# v0.9.0 release audit

Audit date: 2026-07-23
Status: released

## Verdict

v0.9.0 is suitable for release as the graph-semantics and checker-free
correctness version of ProofNet-IR. It is an independently consumable Lean
research library for the documented unit-free, cut-free multiplicative linear
logic certificate model.

The exact public decisions are mathematically complete for that model. The
new unification schedules are separately qualified optimizations: every
successful result is proved sound, while the public exact wrapper retains the
already complete checker-free sequentializer as a fallback. This release does
not claim pure-worklist completeness, Guerrini linearity, arbitrary graph
isomorphism, or support for units, Mix, cuts, additives, or exponentials.

## Mathematical claim boundary

The kernel checks the following graph layer:

- occurrence-aware `Graph.Acyclic`, where stored parallel edge occurrences
  remain distinct and can form a length-two cycle;
- exact reindex transport for directed edge occurrences, walks, simple
  cycles, and acyclicity;
- `Graph.IsTree ↔ Graph.Bounded ∧ Graph.Connected ∧ Graph.Acyclic`;
- a sound and complete executable exact-cycle oracle and
  `Graph.isTreeViaAcyclic = Graph.isTree`.

For structurally well-formed MLL certificates, the kernel checks:

```text
CuspAcyclic ↔ every occurrence-order switching is Acyclic

check = true ↔
  StructurallyWellFormed ∧
  CuspAcyclic ∧
  ReferenceSwitchingConnected
```

Consequently `Certificate.compactCheck = Certificate.check`. The current
colored-cycle decision inside `compactCheck` is exhaustive, so that equality
is an exact alternative specification and not a scalability claim.

The supplied-derivation verifier checks formula inference,
desequentialization, and exact intrinsic `ProofNetEquivalent` identity without
running the input certificate's switchings. Successful automatic
`reconstructDerivation?` results have the same proof-bearing contract. Lean
proves that this automatic path succeeds for every reference-accepted
certificate and that:

```text
Certificate.reconstructsDerivation = Certificate.check
```

The unification layer implements Guerrini's axiom/start, par/forward, and
tensor/unify rules. Both the eager and event-driven worklist candidates pass
the independent derivation verifier, and every successful result is therefore
accepted and sound. The exact wrappers satisfy:

```text
Certificate.unificationWorklistCheck = Certificate.check
Certificate.unificationCheck = Certificate.check
```

Those equalities use the complete checker-free recursive sequentializer after
a fast-path miss. The pure worklist's fuel sufficiency and completeness have
not been proved.

## Complexity and resource boundary

Lean proves the eager schedule performs no more than `|links|` full passes and
exactly `passes * |links|` link-list visits, hence at most `|links|²` such
visits. This deliberately excludes frontier search, representative traversal,
derivation verification, and fallback work.

The worklist result carries a proof that link attempts do not exceed
`n(n+4)+1` for `n` links. That theorem proves termination under the executable
cap; it does not prove that the cap finds every correct net. The implementation
still eagerly starts all axioms and uses a flat waiting-par set, rather than
Guerrini's Figures 7--8 `NEXTAXIOM`/token-age sequential stack. No whole-program
linear or polynomial bound is claimed.

The complete automatic reconstruction fallback can backtrack over inverse
rules and enumerate formula-compatible repeated-label boundary orders.
`reconstructDerivationWithinLimits` is the fail-closed public alternative:
it checks explicit 128-formula/96-link/24-conclusion default ceilings and
never constructs the exhaustive formula-order fallback. A bounded failure is
inconclusive rather than a logical rejection.

## Literature correspondence

The pre-existing local reading ledger accounts for all 948 physical pages
(approximately 780 unique after the exact 168-page Pfenning duplication) in
the seven original local PDFs, plus the complete Rowling chat. The page
matrices distinguish ordered text reading, rendered-page inspection, relevance,
and duplication rather than treating file discovery as reading.
The release audit re-inventoried the parent workspace and recomputed all seven
SHA-256 hashes; every file still matches the frozen reading ledger, and no new
project-literature PDF is present beyond the supplemental Guerrini copy.

For the new algorithm, the separate Guerrini audit covers all ten pages and
all eight figures of the 1999 LICS primary paper. Figure 5 supports the current
logical token rules. Proposition 15 and Theorem 16 do not transfer their linear
bound to this implementation, because that bound depends on the sequential
strategy, `NEXTAXIOM`, ready/waiting organization, and specialized
union-find invariants not yet formalized here.

The literature establishes correspondence with the intended standard
unit-free MLL criterion. It does not replace Lean proofs, independent
differential tests, or downstream package execution.

## Validation receipts

- v0.9 worklist implementation commit:
  `fc43b926432088be537b525c6f87c1da0736fc2d`;
- full Ubuntu CI for that commit passed in run `30028691571`;
- clean v0.9 release-candidate consumer commit:
  `ba137023b2286e421d5b4181a4d60bd639173c53`;
- release-candidate consumer pins the implementation commit above, clones it
  from GitHub, compiles public graph, reconstruction, worklist, exact-check,
  and intrinsic-key APIs, and executes successfully on Windows;
- release-candidate Ubuntu CI passed the complete workflow in run
  `30029142932`, including the commit-pinned v0.9 consumer;
- release commit:
  `9b7dc3d104af8f57ea9123aab2e61b42e05d2216`;
- annotated tag object:
  `e31c9409ac3545208b577cd9da124e6a72f5cfb8`;
- `v0.9.0^{}` resolves to the release commit above;
- automatic tag-push CI passed the complete workflow in run `30030229438`;
- explicit `release_ref=v0.9.0` CI verified exact checkout equality and passed
  the complete workflow in run `30030226127`;
- the post-release consumer resolves public tag `v0.9.0` to the release commit
  above and passes locally on Windows;
- post-release Ubuntu main CI passed the complete workflow, including that
  exact tag-pinned consumer, in run `30030915421`;
- the exact trust audit covers 88 public MLL theorems with no dependency beyond
  `[propext, Classical.choice, Quot.sound]`; six are axiom-free, with narrower
  dependency subsets separately locked where applicable;
- the build uses `warningAsError`, generated API documentation is drift
  checked, and no Lean source contains `sorry` or `admit`;
- the 1,500-case unification differential gate records 750 accepted
  positives, 750 rejected mutations, no fast-path false positive, and no
  observed eager/worklist positive miss;
- the adversarial positive search checks 6,000 cases generated from 1,000
  derivations across six storage orders, through 111 formula occurrences and
  79 links, with no observed eager/worklist miss;
- the 18-case adversarial reconstruction suite reaches 126 formula
  occurrences and 22 conclusions under its 45-second CI budget;
- the committed deterministic 1,000-task matched experiment and held-out
  180-task model experiment remain artifact-hash and Lean-verification gated.

## Remaining macro goal

The persistent macro goal remains open after v0.9. The next research line is
to prove pure worklist completeness and fuel sufficiency, replace eager axiom
starts and flat waiting requeues with the sequential `NEXTAXIOM`/token-age
stack, and prove the cost of every implemented operation before making a
Guerrini-linear claim.

Broader proof-net scope remains separate work: units, cuts and cut
elimination, Mix, additives, exponentials/boxes, arbitrary graph-isomorphism
identity, broader Lean/mathlib integration, and a tactic/tooling layer.

## Publication receipt

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

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