# v0.8.0 release audit

Audit date: 2026-07-23

## Verdict

v0.8.0 is suitable for release as the non-factorial exact proof-identity
version of ProofNet-IR. It is a usable research library for the documented
unit-free, cut-free MLL certificate model. It is not yet a mature
general-purpose Lean or proof-net library.

The release removes the v0.7 canonical wire's factorial link-order enumeration
and seven-link generation ceiling. It does not change the meaning of
`ProofNetEquivalent`, weaken the ordered logical boundary, optimize the
all-switchings checker, or add unsupported logical fragments.

## Mathematical claim boundary

`ProofNetEquivalent` is generated by bounded vertex renaming and literal
link-list permutation. It preserves:

- ordered conclusions;
- tensor and par premise order;
- formula labels and polarity;
- axiom endpoint orientation.

On structurally well-formed certificates Lean proves:

- the ordered-conclusion occurrence forest contains every formula-array vertex
  exactly once;
- orientation-sensitive owner emission contains every submitted link exactly
  once and is a permutation of the input links;
- `intrinsicCanonicalize` is `ProofNetEquivalent` to its input;
- equivalent inputs have equal intrinsic canonical forms;
- intrinsic canonical-form, framed-code, and typed-key equality are each
  equivalent to exactly `ProofNetEquivalent`.

Checker acceptance supplies the structural premises. Two structurally
validated local certificates safely matching the same wire-admissible parsed
intrinsic key are therefore proved equivalent.

These statements are not arbitrary graph-isomorphism results. Reordering
conclusions, swapping connective premises, or reversing an axiom's stored
orientation can change the key by design.

## 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.

The literature audit is evidence that the formal scope matches the intended
standard criterion; it does not replace the Lean proofs, independent
differential audits, or downstream execution.

## Algorithm and resource boundary

The intrinsic construction follows unique tensor/par producers from the
ordered conclusion forest in left/right premise order. Axioms are owned by
their stored left endpoint; tensor/par links are owned by their conclusion.
Existing first-occurrence relabeling then removes submitted vertex numbers.

The direct list implementation has a conservative `O(VL + V^2)` bound for
`V` formula occurrences and `L` links, excluding emitted formula-token volume.
It never enumerates link permutations. The new
`proofnet-canonical-key-0.2` /
`proofnet-equivalent-intrinsic-v1` wire still fails closed above 100,000 tokens
or 1,000,000 aggregate token characters. A checked v0.3 certificate can be
migrated by semantic recomputation; a bare v0.1 key cannot be converted without
its source certificate.

The reference all-switchings checker remains exponential in the number of par
links, and executable sequentialization remains depth-sensitive. v0.8 does not
claim otherwise.

## Validation receipts

- release commit:
  `09a21c328070d53e9fe26b09ed13d2650ab756db`;
- annotated tag object:
  `cca54261eecf8ed6f9d01ca7e841e25fd32f8903`;
- `v0.8.0^{}` resolves to the release commit above;
- release-candidate Ubuntu CI passed the complete workflow in run
  `30002198711`;
- the automatic tag-push workflow passed the same complete suite in run
  `30002543465`;
- explicit `release_ref=v0.8.0` CI verified exact checkout equality and passed
  the complete workflow in run `30002560604`;
- the trust audit locks 45 public MLL boundary theorems to exactly
  `[propext, Classical.choice, Quot.sound]`;
- no Lean source contains `sorry` or `admit`;
- 1,000 deterministic positive/negative cases agree with the v0.7 factorial
  oracle, and 1,000 additional mixed derivation-generated accepted nets retain
  equal, round-tripping, safely matching keys after link-list reversal;
- 5,000 deterministic malformed intrinsic-key strings pass the native parser
  fuzz gate;
- Ubuntu measured four intrinsic cases through 145 links in 82 ms aggregate,
  below the separate five-second budget; the complete representative workload
  took 5,375 ms below its 45-second budget;
- the clean commit-pinned consumer passed inside all three release workflows;
  the post-release consumer resolves public tag `v0.8.0` to the release commit
  and passes locally.

## Publication receipt

The non-draft, non-prerelease GitHub release was published on
2026-07-23 at 11:17:02 UTC:

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

## Remaining macro goal

The persistent project goal remains open. Major remaining work includes an
optimized correctness checker, stronger sequentialization performance and
resource controls, public acyclicity ergonomics, units and cuts/cut
elimination, additives and exponentials, broader Lean integration, and a
tactic/tooling layer. The current intrinsic key is exact only for the explicitly
documented relation and retains a finite output-size envelope.