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 current 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.
The report is deterministically rendered from the status and publication map that are themselves derived from the compiled Lean environment.
The canonical compiled inventory records the checked declarations, modules, theorem kinds and their axiom closures. Private compiler auxiliaries are excluded. Project-specific axioms remaining: 0. Inventory size is not proof completion.
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.
Publication requires the strict conjunction of concrete target, root, type/value, axiom-closure, and source-closure checks. Unconfigured null fingerprints never match.
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. This row count measures the evidence ledger, not proof completion.
The report includes the concrete machine foundations, complete all-input Cook-Levin polynomial reduction, concrete CNF-SAT NP-completeness and locked-NAND reduction. The computational residual work now connects physical accounting and normalization to source-derived full-field-preserving support replacement.
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.
A deterministic polynomial-time SAT algorithm, unconditional residual minimization and global ZeroSlack, complete exact PCCMin with polynomial construction, runtime, output-size and certificate-size bounds, and the eligible concrete P-versus-NP root theorem. The full manuscript carrier, general obligation calculus and complete global routes remain open. The report-facing compatibility alias and conditional bridge cannot substitute for that missing root. P = NP is not established.
PNP.PEqualsNP now aliases the concrete finite charged-pipeline mutual-inclusion proposition, and PNP.Main.ConcretePEqualsNP names the same inactive target. Neither definition proves the proposition. The reviewed activation fingerprints and exact compatibility root PNP.Main.p_eq_np remain absent, so the gate fails and all public theorem-emission fields remain false or null.
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.
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.
