Compiled declaration inventory
27,794 exported public declarations from 250 modules, including 14,454 theorem-kind declarations and 7,347 assumption-free theorem-kind declarations. Exactly 15,008 private compiler auxiliaries are excluded.
See how Lean source becomes a public status report.
The source is compiled, declarations and axiom closures are inventoried, reviewed milestone pins are checked, and the public report is generated. Missing or inconsistent evidence fails closed.
Layer map
Current publication layers.
Each layer must match the exact reviewed coordinate. Missing, stale, malformed, digest-mismatched, or internally inconsistent data fails closed.
Reviewed evidence pins
2,589 milestone candidates carry reviewed kernel-type fingerprints; the publication map itself is digest-pinned.
Whole-source closure
Every Lean source plus toolchain, Lake configuration, manifest, and inventory probe is bound to one reviewed source-closure digest.
Scoped milestone classifier
One hundred and nine earned rows require theorem presence, theorem kind, approved axiom closure with no project axiom, exact type pins, and source-closure agreement. The newest row publishes an exact finite ambient-BN4-ledger embedding for generated balanced PkgC cancellation cells. Duplicate multiplicities and per-key mass decompose through an explicit remainder, while a candidate-derived kernel retains canonical request atoms. The ambient ledger, restorer, exact certificate or serialization, and successful kernel remain explicit inputs. The result does not establish full PkgC route integration or silence, global ZeroSlack, polynomial PCCMin, or the root theorem.
Concrete publication gate
Concrete standard semantics, target/root fingerprints, axiom closure, and source closure form a strict conjunction. Null is never a match.
Generated public surfaces
Status, theorem-emission fields, TeX, PDF, and site copy derive from the gate and inventory; historical checker records cannot override them.
Historical package ledger
Unformalized vocabulary from the 57-page manuscript.
These names are review leads, not inventory-derived theorem evidence and not current publication inputs.
| Package family | Audit question | Expected evidence |
|---|---|---|
| E / N / FT / X | Do local transformations compile to full-mode verified direct-wire gains? | Frontier exactness, obligation lifecycle, finite coverage, route priority, and gain compilation. |
| BC / UN / HN / BUD | Are governed structures routed, solved, or sidecar-blocked without circular justification? | Transition audits, BWL exactness, budget dynamic programs, and blocker-indexed sidecars. |
| RW / BN2–BN6 / PkgC | Does positive residual slack force a concrete packet prototype? | BCEL nuclei, side-tight bases, activation antichains, full-shadow localization, and constant-cut hypergraphs. |
| Packet / R / HB / O | Does every packet yield a selector, and every unblocked selector yield a checked gain? | Faithful seeds, typed bots, charge-surplus injections, rank induction, selector silence, and ZeroSlack. |
| G / Final / PACK | Can the proposed package argument be reconstructed as a polynomial SAT decision theorem? | Concrete Lean locked-NAND threshold, framework match, residual minimiser, ZeroSlack, polynomial bounds, root theorem, and axiom audit. |
Trust boundaries
Primary trust boundaries.
Legacy checker boundary
The JavaScript checker validates fields and relations in assertion-bearing records under implemented predicates. It does not prove the mathematical assertions carried by those fields.
Constructive firewall
The new Lean interface makes the terminal case explicit: selected-coordinate equality is not a full-mode replacement until every omitted profile coordinate is checked. Route tokens, sidecar records, and bounds-only evidence likewise cannot stand in for complete replacement records.
Release custody
Source/checker origin is separated from the durable artefact-bearing release, with manifest and checksum records available for review.
Formal invariant
Every mathematical step must become a checked Lean theorem.
Legacy verifier records can identify proposed obligations, but the reconstruction must prove them from concrete definitions and expose every remaining axiom at the root theorem.