# v0.6.0 release audit

Audit date: 2026-07-23

## Verdict

v0.6.0 is suitable for release as a scoped research-library version of the
persistent/linear LeanProp bridge. It is not evidence that ProofNet-IR is a
mature general-purpose Lean library, and it does not broaden the established
unit-free, cut-free MLL certificate semantics.

The release claim is limited to:

- a proposition-indexed two-context derivation with explicit persistent
  weakening/contraction, no linear structural constructors, and ordinary Lean
  proposition rules;
- executable checking and typed elaboration for the separate
  `leanprop-schema-0.1` atoms/conjunction/implication wire fragment;
- proof-term reconstruction, exact linear-use counting, proof-relevant
  exchange completeness, and the documented raw/indexed agreement theorems;
- a noncomputable typed normalizer for the exact local redex
  `persistentContract (persistentWeaken premise)`, recursively under every
  derivation constructor.

It does not claim a runtime raw-schema normalizer, all commuting conversions,
an MLL interpretation of ordinary Lean conjunction/implication, proof-net
semantics for quantifiers, or arbitrary graph-isomorphism canonicalization.

## Source correspondence

The seven original project PDFs and Rowling chat are recorded as completely
read in the reading ledger and source-coverage audit. Their current file hashes
still match the audited corpus:

| Source | SHA-256 |
|---|---|
| Pfenning, *Linear Logic* | `5d5a29d68c13c530243075b60f9ff9e64ea6ac1885a752323c6f4b0beb96fa96` |
| Manin, *A Course in Mathematical Logic for Mathematicians* | `79baf1ed4e817e0b081180e55d17b26765a41a00f5819b8eab5dca58be9351ee` |
| *Proof Nets as Graphical Proof Objects* | `8166b610c3b86f8538835a55e90ff9e653e41acb2bff6b465f94bae0dd2474b8` |
| *ProofNet-IR Research Plan* | `4c934e603f8a21985545340630988b8c74ea5526326efeabb3645a03a06d85aa` |
| Marcolli et al., *Syntax-Semantics Interface* | `ed4daccfdf3ebe31c21204ec5e0c3f3c857e00df93674920902115a6a9935fa9` |
| *Geometry of Neuroscience* | `e7730b0731bb9897e67961554bd2a00a96a0bcd47db342c6460d51c19e7a5602` |
| Park, *Open Book Decompositions with Page a Four-Punctured Sphere* | `7b756a8759e10173d0089d1fa9dad4bb6b8362ff91a08f48797cbcb2d7b29388` |

Pfenning supports the unrestricted/linear distinction and the need for
different structural principles. The project-specific documents motivate the
staging. None of the sources licenses identifying this LeanProp layer with
the existing MLL tensor/par certificates, so the implementation keeps the two
modules separate.

## Kernel and executable evidence

On the public candidate history:

- release metadata commit
  `ca5f825d1c67417ceb1fd22fb821dad142f8e563` changes the package version and
  release documentation after the green code baseline; it does not change a
  Lean declaration, schema, executable, dataset, or experiment artifact;
- the whole Lean project builds with zero `sorry`/`admit` in
  `ProofNetIR/*.lean`;
- the API environment generator resolves the public declarations and rejects
  stale or unsafe entries;
- the exact trust audit reports 25 MLL boundary theorems using only the locked
  set `[propext, Classical.choice, Quot.sound]`; for LeanProp, four audited
  theorems are axiom-free, fifteen use exactly `[propext]`, and four use
  exactly `[propext, Quot.sound]`;
- all 600 positive LeanProp templates pass typed erasure, raw checking,
  elaboration, canonical wire round trip, and universal reconstruction checks;
- all 1,000 malformed templates are rejected with their exact raw and wire
  diagnostics;
- the 1,600-record Lean-emitted corpus matches SHA-256
  `76433392981d2739c71d1478216d5cecc57cb262326587129c13bd6b908c3a91`;
- the deterministic LeanProp parser mutation gate classifies 5,000 cases;
- a clean Lake consumer fetched public commit
  `bda420f42d99235f5a9de17e865f5c16b178d9c0` from GitHub and typechecked the
  checked-wire and normalization APIs;
- annotated tag `v0.6.0` resolves to release commit
  `72cdc292be13b5407b1a172e3b43d7b372f43e84`; after changing the clean
  consumer input revision to `v0.6.0`, Lake resolved that exact commit,
  rebuilt all 65 jobs, and ran the consumer smoke successfully;
- Ubuntu CI for main commit
  `c26a9b5a029bae81e7ef143a691b462a2e813402` passed every build, fuzz,
  schema, corpus, performance, downstream-consumer, experiment-artifact, and
  independent differential-mathematics gate in run
  `29991395630`.
- the release-metadata commit passed the same complete main workflow in run
  `29991853283`;
- post-tag main commit `2d190d05d9621b2ce625795ef5c69dae1a01d347`
  passed the complete workflow in run `29992330129`; its Ubuntu
  `Consume the pinned public v0.6.0 release` step installed and used the
  public tag successfully.
- main commit `0ce15cfc19ee2e8ca0602af01aa0376c441665a2`
  passed the complete push workflow in run `29992857227`;
- because GitHub did not enqueue a separate run for the original tag-push
  event, explicit release-ref run `29992876112` checked out `v0.6.0`, proved
  that its actual HEAD was release commit
  `72cdc292be13b5407b1a172e3b43d7b372f43e84`, and passed the full workflow.

## Mathematical boundary of the normalizer

The indexed return type preserves the persistent context, exact linear
context, and goal by construction. Kernel theorems establish:

- every output is free of an immediate contraction-over-weakening redex;
- every reduced derivation is a fixed point;
- normalization is idempotent;
- persistent weakening/contraction node count does not increase;
- linear-axiom count is unchanged;
- `toProof` is pointwise equal before and after normalization.

The `toProof` equality is proof-irrelevant equality between inhabitants of the
same proposition. It is not a completeness theorem for proof-term identity.
The current normal form also does not commute weakening or contraction across
exchange or logical rules to identify all structurally equivalent derivations.

## Release procedure

The version commit passed the full main CI before the annotated `v0.6.0` tag
was pushed. Because a repository cannot contain a consumer that refers to its
own not-yet-created tag without a circular commit hash, the final external
consumption gate is performed from main after the tag exists: the clean
consumer dependency is `v0.6.0`, and the GitHub release is created only after
that main CI rebuild passes. The workflow also supports explicit manual
dispatch with a `release_ref`: checkout and an explicit commit-equality check
ensure a missing automatic tag-push event can be rerun against the exact tag
contents rather than inferred from a branch checkout.

## Publication receipt

The non-draft, non-prerelease GitHub release was published on
2026-07-23 at 08:56:30 UTC:

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

## Macro library-readiness boundary

This release is genuinely usable within its documented fragments, but the
macro mature-library goal remains open. Important remaining work includes
broader logical fragments, a compact canonical representative for the broader
proof-net equivalence when one is specified, harder performance
qualification, broader property/fuzz coverage, and integration/tactic work.
The negative model-backed experiment remains part of the evidence and is not
reframed as a proof-net performance advantage.