# v0.7.0 release audit

Audit date: 2026-07-23

## Verdict

v0.7.0 is suitable for release as the exact, scoped proof-identity version of
ProofNet-IR. It is a usable research-library release for unit-free, cut-free
MLL certificates, but it is not a mature general-purpose Lean library.

The release establishes a single typed key whose equality is equivalent to the
documented `ProofNetEquivalent` relation on structurally well-formed, hence
checker-accepted, certificates. It also publishes a separate bounded wire
contract. It does not claim arbitrary graph isomorphism, reordered conclusion
boundaries, or scalable canonicalization.

## Mathematical claim boundary

`ProofNetEquivalent` is the equivalence generated by bounded vertex renaming
and semantically irrelevant link-list permutation. It preserves:

- the ordered conclusion boundary;
- tensor and par premise order;
- formula labels and polarity;
- axiom endpoint orientation.

Lean proves:

- injectivity of the length-framed formula, link, and certificate structural
  encoders;
- totality and selected-family membership of `proofNetCanonicalCode?`;
- `ProofNetEquivalent` iff typed canonical-code equality under structural
  well-formedness;
- the same iff theorem with checker acceptance supplying the structural
  premises;
- the corresponding exact theorem for the bounded wire-key generator when
  both inputs satisfy the seven-link ceiling;
- two checker-accepted certificates matching one parsed opaque key are
  `ProofNetEquivalent`.

The older JSON fingerprint remains forward-only because the project does not
assume `Json.compress` injectivity.

## Source correspondence

The reading ledger and source-coverage audit account for every unique page of
all seven original local research PDFs plus the complete Rowling chat. The
project-specific proof-net exposition supports explicit occurrences and the
Danos-Regnier all-switchings tree criterion for unit-free MLL without Mix.
Pfenning supports cut-free linear resource discipline and focused comparison.
The other sources are recorded as conceptual or later-case-study inputs and do
not supply proof-net correctness theorems.

This source audit does not itself prove the implementation correct. The trusted
mathematical boundary is the Lean definitions and theorems, checked against the
standard scoped criterion and tested by the independent audits below.

## Wire and resource boundary

`proofnet-canonical-key-0.1` uses the
`proofnet-equivalent-v1` canonicalization marker and an opaque array of
length-framed structural tokens. The parser enforces:

- exactly the declared fields and marker values;
- a nonempty token array;
- at most 100,000 tokens;
- at most 1,000,000 aggregate token characters.

The typed exact key remains total but materializes a factorial family. Public
wire generation, migration, and parsed-key matching therefore check a hard
seven-link ceiling before evaluation. Above the ceiling they fail closed.
Callers should use `CheckedCertificate.sameProofNet?` for larger pairwise
comparisons.

## Validation receipts

- release commit:
  `dab12d48d1af62daa5c2fe96cc7fdff4b86e16eb`;
- annotated tag object:
  `bd658bf00dee455aa1ecdabc273b5815476ec37b`;
- `v0.7.0^{}` resolves to the release commit above;
- release-commit Ubuntu CI passed every build, test, schema, fuzz, benchmark,
  downstream-consumer, experiment, and independent differential-mathematics
  gate in run `29998286474`;
- explicit `release_ref=v0.7.0` CI verified the checked-out commit equality and
  passed the complete workflow in run `29998511738`;
- the automatic tag-push workflow passed the same complete suite in run
  `29998512286`;
- the trust audit locks 37 public MLL boundary theorems to exactly
  `[propext, Classical.choice, Quot.sound]`;
- 1,000 deterministic canonical-key wire properties and 5,000 malformed-key
  parser mutations pass;
- the 1/4/7-link benchmark materializes 5,065 candidates under a separate
  10-second budget and the full representative workload remains below 45
  seconds;
- a clean Lake consumer resolves the public `v0.7.0` tag to the release commit
  and exercises exact bounded-key equality, safe matching, over-limit failure,
  and executable sequentialization.

## Publication receipt

The non-draft, non-prerelease GitHub release was published on 2026-07-23 at
10:18:01 UTC:

`https://github.com/fushanbobfan/proofnet-ir/releases/tag/v0.7.0`

## Remaining macro goal

The persistent project goal remains open. Major remaining work includes a
proved non-factorial canonical construction, stronger sequentializer
performance, public acyclicity/theory ergonomics, units and cuts, additives
and exponentials, broader Lean integration, and a tactic/tooling layer. No
v0.7 theorem or benchmark establishes those claims.