# v0.10.0 release audit Audit date: 2026-09-21 Status: released ## Verdict v0.10.0 is suitable for release as the sequential-decision version of ProofNet-IR. Its public decision `Certificate.unificationCheck` is the sequential Figures 7–8 executable of Guerrini's algorithm: it is proved equal to the reference all-switchings checker with no eager scan, no worklist tier, and no recursive fallback, and every operation of a run is counted and bounded by a kernel-checked quadratic theorem. The library remains an independently consumable Lean research library for the documented unit-free, cut-free multiplicative linear logic certificate model. This release does not claim Guerrini linearity, completeness of the retained eager or flat-worklist candidates, arbitrary graph isomorphism, or support for units, Mix, cuts, additives, exponentials, or quantifiers. ## Mathematical claim boundary Every v0.9.0 guarantee is retained with its statement unchanged: exact occurrence-aware graph semantics, `check = true ↔ StructurallyWellFormed ∧ CuspAcyclic ∧ ReferenceSwitchingConnected`, `compactCheck = check`, the supplied-derivation verifier, complete checker-free reconstruction with `reconstructsDerivation = check`, and the sound eager and worklist candidates with `unificationWorklistCheck = check`. The [v0.9.0 release audit](v0.9-release-audit.md) states them exactly. New in v0.10.0, the kernel checks the sequential scheduler layer: - a reservation state with the ready-bucket stack, the `sigma` boundary, the waiting cells, immutable raw token ages, and the complete `NEXTAXIOM` tag array; the canonical dispatcher runs `concl`, `nop`, `new`, `wait`, `forward`, and `unifyPayload` in that fixed precedence, and every successful rule preserves the occurrence-exact scheduler invariant; - termination: repeated dispatch stops within `formulas.size + 1` calls (ledger item D4); - progress: a started reachable state of a correct certificate either dispatches or has every occurrence marked (D3), through an order-free region-closure invariant and switching connectedness; - enabledness: reachable `new` guards suffice, and a reachable nonterminal state has a priority witness exactly when it is initialized; the original unconditional form is refuted by the reachable empty scheduler of one axiom (D5, refuted as stated and closed in corrected form); - completeness of the executable and the public decision: ```text Certificate.sequentialFastCheck = Certificate.check Certificate.unificationCheck = Certificate.sequentialFastCheck Certificate.unificationCheck = Certificate.check ``` `sequentialFastCheck` initializes at the first conclusion, runs the dispatcher for the carrier budget, exchanges the final component's frontier into the conclusion order, and accepts only a derivation that `verifyDerivation?` validates, so soundness is by construction; completeness (D1) composes initialization totality, the run's endpoint, the final structure, inference, and proof-net equivalence of the desequentialized final derivation to the input. The verifier now compares intrinsic canonicalizations instead of their string codes; the certificates it accepts are unchanged by theorem. ## Complexity and resource boundary The instrumented twin `sequentialDecisionWithStats` runs the public decision and counts the operations of every phase (structural check, initialization, each dispatcher call by its rule attempts, final extraction, verification); its Boolean is proved equal to `unificationCheck`. The kernel checks: ```text StructurallyWellFormed certificate → sequentialDecisionWithStats.stats.total ≤ 152 * (formulas.size + 1) * (formulas.size + links.length + conclusions.length + 1) sequentialDecisionWithStats.stats.total ≤ 152 * inputSize * inputSize ``` where `inputSize` adds the symbols of every submitted formula, because a malformed input can carry formulas larger than its carrier and the structural check reads them before rejecting. The model charges each list traversal by its length, each array access by one, each formula by its symbols with an atom name as one symbol, and each early-failing rule attempt in full; its charging conventions are stated in `ProofNetIR/Figure7/Cost.lean`, not extracted from compiled code, and wall-clock time is measured, not proved. The bound is quadratic, not linear: the stack is list-based with tail access, buckets are rebuilt by append, and the consumer index is recomputed per rule attempt. Guerrini's Proposition 15 and Theorem 16 therefore still do not transfer to this executable; linearity is recorded as the later goal D6-linear. The eager `|links|²` link-visit bound and the worklist `n(n+4)+1` link-attempt cap of v0.9.0 remain as stated there. Measured on the committed 291-input benchmark corpus on Windows: sequential decision 47 ms, reference all-switchings check 532 ms, exact sequentialization 4,707 ms. On the 7,200-case adversarial positive corpus (up to 447 occurrences and 319 links) every case is accepted, the largest instrumented run used 14.7% of its proved cost bound, and the largest call count, 448 for 447 occurrences, is exactly the termination bound. ## Literature correspondence The frozen reading ledger is unchanged since v0.9.0. A rescan of the parent workspace on 2026-09-21 found the same 16 PDFs; all eight included-PDF SHA-256 values and the Rowling brief hash still match the ledger, and no project-literature source was added, removed, or changed. For Guerrini (LICS 1999), the separate audit covers all ten pages and eight figures. Figures 7 and 8 are now implemented as the public decision and proved complete; the `NEXTAXIOM` search, token ages, and the ready/waiting stack are formalized as the scheduler invariant. Proposition 15 and Theorem 16 do not transfer their linear bound, because the implemented data structures are not constant-time. The literature establishes correspondence with the standard unit-free MLL criterion; it does not replace Lean proofs, differential tests, or downstream package execution. ## Public API changes since v0.9.0 - `Certificate.unificationCheck` moved from `ProofNetIR/Unification.lean` to `ProofNetIR/Figure7/Sequential.lean` and is now the sequential fast path alone; `unificationCheck_eq_check`, `unificationCheck_eq_true_iff_check`, and `unificationCheck_eq_true_iff_declarativelyCorrect` keep their names and statements, and `unificationCheck_eq_sequentialFastCheck` is new. Code that imports only `ProofNetIR.Unification` and names `unificationCheck` must import the umbrella `ProofNetIR` or `ProofNetIR.Figure7.Sequential`; the former eager, worklist, and reconstruction tiers stay public under their own names. - `PriorityEnabled` stores input-only `new` enabledness; the field-type break and its migration are in [compatibility.md](compatibility.md). - 153 new library modules, all reachable through `import ProofNetIR`; the generated [API reference](api-reference.md) and the trust audit cover their registered public declarations, and no module was removed. - Wire formats and schemas are unchanged. ## Validation receipts - D6 checkpoint commit `33ebfd52543b443b52115f940c5e8ec736faa46e`; full Ubuntu CI passed in run `35557157288`; - adversarial-corpus check of the compiled decision, commit `f833e292c03438bf003749ba4fd5a6515c0c677c`; CI run `35601448836`; - release-candidate consumer commit `e1a3805` pins `f833e29`, clones it from GitHub, compiles the public decision, its theorems, the cost bounds, the verifier, and the intrinsic key, and executes successfully on Windows; release-candidate Ubuntu CI passed the complete workflow in run `35603279988`; - the exact trust audit covers 1,191 audited declarations: 889 public MLL theorems depend on exactly `[propext, Classical.choice, Quot.sound]`, 25 are axiom-free, 132 use `propext` only, and 145 use `propext` and `Quot.sound` only; - the build uses `warningAsError`, generated API documentation is drift checked, the convergence gate passes, and no Lean source contains `sorry` or `admit`; - the 1,500-case unification differential gate records the public decision equal to the reference on every case, 750 accepted positives, 750 rejected mutations, and no eager or worklist positive miss or false positive; - the 7,200-case adversarial positive search (1,200 derivations, depths zero through seven, six storage orders) records no eager or worklist miss, and its sequential mode records acceptance by the public decision on every case with the instrumented dispatcher-call and cost bounds holding on all 1,200 original variants; - the 1,000-case reconstruction audit and the 18-case adversarial reconstruction suite pass within their CI budgets; - the finite Figure-7 audits pass: the new-progress replay classifies all visited states with zero incomplete-without-head, incomplete-dispatch-none, cycle, or truncation counters, and the tail-law search reports the region predicate C12 at all 1,217,664 default and 1,071,360 wait-focus reachable states; - the committed deterministic 1,000-task matched experiment and held-out 180-task model experiment remain artifact-hash and Lean-verification gated; - release commit: `f0fd97f8592938165dbffd91656d226b6102adcc`, whose main-branch CI passed the complete workflow in run `35605382703`; - annotated tag object: `c9338bc0c681d49e57ec827747fae0a34ce15722`; - `v0.10.0^{}` resolves to the release commit above; - automatic tag-push CI passed the complete workflow in run `35607492983`; - explicit `release_ref=v0.10.0` CI verified exact checkout equality and passed the complete workflow in run `35607552332`; - the post-release consumer resolves public tag `v0.10.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 `35609911959`. ## Publication receipt The non-draft, non-prerelease GitHub release was published on 2026-09-21 at 14:05:02 UTC: `https://github.com/fushanbobfan/proofnet-ir/releases/tag/v0.10.0` ## Remaining macro goal The persistent macro goal remains open after v0.10. The next research line is a linear whole-program bound (D6-linear): constant-time stack access and bucket merge and a single consumer-index construction, measured by the committed operation counters, before any Guerrini-linear claim. The flat worklist's completeness and linear bound and the history tail law are retired, unproved, in the [goal ledger](goal-ledger.md). Broader proof-net scope remains separate work: units, cuts and cut elimination, Mix, additives, exponentials/boxes, quantifiers, arbitrary graph-isomorphism identity, broader Lean/mathlib integration, and a tactic/tooling layer.