Compiled environment
27,794 public declarations across 250 modules, including 14,454 theorem-kind declarations and 7,347 assumption-free theorem-kind declarations. Exactly 15,008 private compiler auxiliaries are excluded.
Read what has been machine-checked, and what has not.
The current 88-page report is generated from the compiled Lean inventory. It records scoped results, assumptions, and missing work. It does not report an established proof of P = NP.
Publication model
Inventory first, report second
The report is deterministically rendered from the status and publication map that are themselves derived from the compiled Lean environment.
Reviewed milestone pins
2,589 theorem candidates have reviewed kernel-type SHA-256 pins. Earned milestones require every named theorem to be present, theorem-kind, type-matched, bound to the reviewed source closure, and free of project or unapproved axioms.
Concrete gate
Publication requires the strict conjunction of concrete target, root, type/value, axiom-closure, and source-closure checks. Unconfigured null fingerprints never match.
Current result
One hundred and nine scoped milestones; two missing global milestones
The latest result is an exact finite PkgC ambient-BN4-ledger embedding. Given an explicit ambient ledger, typed restorer, exact multiset certificate, and successful candidate-derived kernel, Lean preserves duplicates, decomposes per-key mass, and reduces signed mass and executable residual contribution to an explicit remainder. Those inputs remain explicit and are not derived from a terminal candidate. The result does not prove full PkgC route integration or silence, complete global routing, or polynomial generation and runtime. Scope labels and non-claims are part of every milestone row.
Earned scoped results
Concrete machine/cost semantics and raw-machine compilation; universal concrete CNF-SAT verifier correctness, no-timeout and NP membership; Cook-Levin semantics, size and schedule bounds, and a bounded formula-building prefix; typed locked-NAND semantics, strict codecs, fixed machines, concrete polynomial reductions, and the report-facing all-bitstring locked-NAND reduction theorem; verified residual-gain chains and a semantic stopping criterion; terminal carriers, projection minima, finite support construction, four-corner coherence and tight-basis results; computed BN2 structural square legitimacy; a canonical positive terminal BCEL anchor nucleus; candidate-derived terminal saturation traces and finite routing; the finite terminal positive-saturation composition; the fixed ten-coordinate residual RankWF; the finite candidate-derived BN3 request envelope; the finite BN4 activation-exact same-key cancellation kernel; the finite BN5 full-shadow localization kernel; the finite PkgC separating-consumer restoration dichotomy, typed restoration realization, typed-restoration same-key cancellation, and ambient-BN4-ledger embedding; the finite V54 consumer-antichain normal form; the finite V53 constant-cut hypergraph classification; and the finite BN6 grouped hypergraph-packet bridge with payload witnesses. The BN4 ledger, BN5 payload and shadow universe, PkgC consumer antichain, typed restoration operation and coordinate maps, V54 minimal-consumer antichain and singletonization premise, and BN6 survivor family, grouping, payloads, and constant-cut equation remain explicit inputs. The ambient ledger, typed restorer, exact embedding certificate, and successful candidate kernel are not derived from a terminal candidate. The full historical BN4, BN5, PkgC, and BN6 results, a decreasing complete global route system, selector and realizer completeness, manuscript-wide SaturatePositive, Package E, BCELReady, ZeroSlack, PCCMin, polynomial runtime, and the final theorem remain outside this earned scope.
Not earned
SAT NP-hardness or CNF-SAT NP-completeness, global ZeroSlack, PCCMin, residual minimization and polynomial runtime, a complete Cook-Levin formula builder, CNF-SAT in P, and a concrete standard P-versus-NP target with an eligible root theorem. The legacy abstract string-handle bridge remains quarantined and publication-ineligible. P = NP is not established.
Claim boundary
The abstract bridge is not a publication theorem
The existing PNP.PEqualsNP structure uses string handles for languages and witness code. It is trivially inhabitable and explicitly publication-ineligible. The finite charged-pipeline target PNP.Main.ConcretePEqualsNP and raw-machine linkage are formalized, but reviewed activation fingerprints and compatibility root PNP.Main.p_eq_np remain absent. The gate therefore fails, and all public theorem-emission fields remain false or null.
Verify the report
Check the bytes and their source boundary.
Use the published digest ledger for file identity, then reproduce the compiled inventory and publication generation in the Lean repository. A hash match is not proof of a theorem.
Historical provenance
The old 57-page claim manuscript remains historical only
The historical manuscript is preserved at source tag final-pnp-proof-report-hardened-7072f8d, commit 7072f8d0bda6d44d240f9bb3fad624fd357e1278, with provenance in archive/legacy-v0/ARCHIVE.json. Its checker-mediated claim language is superseded and never controls current theorem status or the canonical download aliases.