The project has verified a limit of the implemented circuit search: no fixed cap on the number of gates checked together makes it a complete test for global minimality. For every such cap, a circuit can be made smaller even though the complete bounded search finds no accepted improvement. Every proper selected part, including disconnected selections, is already minimal when its boundary inputs are treated as independent.
The result rules out using this fixed-size local search alone to certify that an entire circuit is minimal. It does not settle P versus NP or rule out growing windows or transformations that use the surrounding circuit. A corrected route must still prove global coverage and polynomial runtime for the complete construction. This correction does not earn a positive milestone or increase the proof-completion estimate.
This correction adds no earned positive publication row or fixed checkpoint credit. Read the verified correction and its limits.
The project has verified a counterexample to an unrestricted reading of the original report's replacement claim. The checked example has a smaller replacement for one part, but inserting it would create a circular dependency; the whole circuit was already minimal.
This does not invalidate the checked replacement results that enforce the necessary restrictions, and it does not settle P versus NP. It identifies a central obligation for the next research: derive the admissible replacements and show that the general method can use them without losing the required saving.
This correction adds no earned positive publication row or fixed checkpoint credit. Read the verified correction and its limits.
Latest earned milestone: M280.
For nested supports that have already been completed by the existing construction, the project now builds the comparison circuits needed to prove cost and positive-saving bounds. The bounds follow from those physical constructions instead of being assumptions.
This establishes the enlargement step for already-completed supports. It does not show that every raw local witness can be completed without losing its saving, and the complete admissibility and global routing arguments remain open.
This is not a globally successful rewrite strategy or a theorem of total polynomial runtime.
M230 and M231 retain the complete Cook-Levin builder and concrete CNF-SAT NP-completeness; a polynomial-time SAT decision algorithm remains open.
Risk-weighted proof completion estimate: 40%, with uncertainty 20% to 40%. Formal artefact coverage: 256 of 258 current scoped publication rows earned. Global gates closed: 0 of 5. Project-specific axioms remaining: 0. The eligible root theorem PNP.Main.p_eq_np remains absent and the publication gate is false.
P = NP is not established.
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.
Each layer must match the exact reviewed coordinate. Missing, stale, malformed, digest-mismatched, or internally inconsistent data fails closed.
The canonical inventory records the actual public declarations, modules, theorem kinds and axiom closures, with private compiler auxiliaries excluded. Reviewed theorem kinds, exact fingerprints, permitted axiom closures and source identity establish the publication boundary. Declaration totals are not proof completion.
Milestone candidates carry reviewed kernel-type fingerprints; the publication map itself is digest-pinned.
Every Lean source plus toolchain, Lake configuration, manifest, and inventory probe is bound to one reviewed source-closure digest.
Formal artefact coverage is 256 of 258 scoped rows, earned only when theorem presence, theorem kind, approved axiom closure with no project axiom, exact type pins and source-closure identity all agree. This evidence-ledger ratio is not proof completion. The separate fixed-weight tracker is 40% and comes from the canonical progress ledger.
For nested supports that have already been completed by the existing construction, the project now builds the comparison circuits needed to prove cost and positive-saving bounds. The bounds follow from those physical constructions instead of being assumptions.
This establishes the enlargement step for already-completed supports. It does not show that every raw local witness can be completed without losing its saving, and the complete admissibility and global routing arguments remain open.
Concrete standard semantics, target/root fingerprints, axiom closure, and source closure form a strict conjunction. Null is never a match.
Status, theorem-emission fields, TeX, PDF, and site copy derive from the gate and inventory; historical checker records cannot override them.
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. |
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.
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.
Source/checker origin is separated from the durable artefact-bearing release, with manifest and checksum records available for review.
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.
