Why a complete local search can still miss a global improvement
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.
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.
Proving cost comparisons for nested completed supports
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.
A machine-checked reconstruction of a proposed route to P = NP.
Current result: P = NP is not established.
P versus NP asks whether problems with answers that can be checked efficiently can also be solved efficiently. Lean is software that checks each stated mathematical step. This project is rebuilding a proposed route in Lean so that completed steps, assumptions, and gaps are explicit.
Proving cost comparisons for nested completed supports
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.
Latest earned step: Computed nested-support cost and positivity transport. For arbitrary finite wire carriers, keep masks and two raw seed lists whose computed completed supports are physically nested, derive the exact gate difference and crossing bindings. Extend the actual full or quotient reference minimum inside the common ambient input domain, preserving the larger padded ordinary interface and exact required computational-field availability, including false values. The derived comparisons prove that either minimum grows by at most the added physical gates, that full slack and support size minus quotient minimum are monotone, and that positive full slack or projection defect remains positive in the completed larger support. Raw-seed inclusion derives the physical inclusion. No cost inequality, field-equality certificate or optimizer is supplied to the final theorem. Remaining boundary: This compares already completed dependency-closed supports in the computational-wire-profile model. It does not prove preservation of an arbitrary raw witness's initial positivity during completion, transparency of every intermediate event, monotonicity of projection defect alone, complete manuscript profile semantics, discovery of a proper positive support, global routing or unconditional SaturatePositive, BCELReady or ZeroSlack. Reference minimization, matching and influence computations remain exhaustive; complete polynomial PCCMin runtime, output-size and certificate bounds are not proved. The eligible root theorem remains absent and P = NP is not proved.
Trust boundary: the current status is bound to the compiled Lean inventory. Hashes identify exact artefact bytes; they do not establish theorem correctness.
Compiled inventory SHA-256:8cffec40ac5786f31bb8538967e79529423316f217bfee319e8423b81cf91bc3. This identifies the exact inventory bytes, not theorem correctness.
Source and release identifiersShowHide⌄
Current inventoryPNP-LEAN-THEOREM-INVENTORY-2026-09-10-230
Coordinates and hashes make the published files identifiable and reproducible. They do not, by themselves, show that a mathematical statement is true.
The question in one minute
What does P versus NP ask?
Here, “efficiently” means the work grows at a manageable polynomial rate as the input gets larger. The question is foundational because it separates finding answers from checking them.
P: problems we can solve efficiently
There is an algorithm that finds an answer within the required polynomial-time limit.
NP: answers we can check efficiently
If someone supplies a proposed answer, an algorithm can verify it within a polynomial-time limit.
The open question
Does efficient checking always mean efficient solving? P = NP says yes. This project has not established that answer.
Choose your depth
Start where the language suits you.
The same status is presented at different levels; technical detail never replaces the plain statement of what is and is not proved.
New to P versus NP
Read short answers about the question, Lean, the current result, and what the percentage means.
Why a complete local search can still miss a global improvement
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.
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.
Proving cost comparisons for nested completed supports
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.
