Every update begins in everyday language and assumes no mathematics background. Open its technical details only when you want the exact Lean scope, theorem pins, and limits.
Use an RSS or Atom reader
Your reader checks this address for new milestones. No email address or PNP Labs account is needed.
This is an editorial planning estimate, updated at each milestone. It is not a probability that the project is correct, a confidence score, or a mathematical claim. It may go down when new work is discovered.
· earned milestone 109
Lean now embeds finite PkgC cancellation into an ambient BN4 ledger
For an arbitrary finite explicit BN4 cell ledger, Lean now accepts a proof-bearing exact multiset embedding of the generated PkgC opposite-sign cancellation cells. The embedding preserves every duplicate and proves that the ambient ledger is exactly the generated balanced subledger followed by an explicit remainder.
At every complete BN4 key, positive and negative mass split across the generated cells and remainder, so both ambient signed mass and the executable residual signed contribution equal the remainder. A successful candidate-derived BN4 kernel also ties every generated cell to its canonical request-atom space, and complete bindings plus exact absence of every computed bridge imply V54 singletonization. The ambient ledger, typed restorer, exact permutation certificate or canonical serialization, and successful kernel remain proof-bearing inputs. Lean has not derived those inputs from a terminal candidate, proved global PkgC route silence or the full historical PkgC theorem, completed global routing, BN6 or Packet selector-realizer completeness, polynomial runtime, ZeroSlack, or PCCMin, put SAT in P, removed a project assumption, or proved P = NP. The 94% figure is a revisable editorial estimate of known reconstruction work, separate from the 109 of 111 scoped formal-publication rows and not a probability that the claim is correct.
Verified scope: For arbitrary finite explicit BN4 cell ledgers, Lean proves that a proof-bearing exact multiset embedding identifies the generated PkgC opposite-sign cancellation ledger with an ambient subledger and preserves every duplicate. Positive and negative mass decompose at every complete key; removing the balanced generated subledger leaves the ambient signed mass and executable residual signed contribution exactly equal to an explicit remainder. A successful candidate-derived BN4 kernel additionally proves every embedded generated cell uses its canonical request-atom space, and complete bindings plus exact absence of every computed bridge imply V54 singletonization.
Boundary: The ambient ledger, typed restoration operation, exact permutation certificate or canonical serialization, and successful candidate-derived BN4 kernel remain explicit proof-bearing inputs. This milestone does not derive the ambient ledger or restorer from a terminal candidate, prove the restorer's semantic adequacy, embed local cancellation or Hall outcomes into the complete global route system, prove global PkgC route silence or the full historical PkgC theorem, establish full BN6 or Packet selector-realizer completeness, polynomial generation or runtime, ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 12
Core source: commit 63f38f39881dd8293e139b1687bf09688acb8e5d, tree af26f9121bd2b6e7d2df11e1d7f3152a0af6914a, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-12-133.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 108
Lean now verifies same-key cancellation for typed PkgC restorations
For every atom of the canonical first disjoint nonsingleton pair, Lean now constructs one positive unit cell for the quotient atom and one negative unit cell for its typed restored candidate. Exact preservation of the complete BN5 coordinate proves that each pair has the same nested BN4 key.
Lean proves the exact cell count, equal positive and negative multiplicity at every BN4 key, an empty computed residual, and zero signed mass. Its total classifier returns either V54 singletonization or a proof-bearing cancellation realization, and exact absence of every cancellation realization forces singletonization. The typed restorer and coordinate maps remain explicit, and the generated cells are not yet identified with a terminal candidate's ambient BN4 ledger. Lean has not completed global route integration or silence, the full historical PkgC result, BN6 or Packet selector-realizer completeness, polynomial runtime, ZeroSlack, or PCCMin, put SAT in P, removed a project assumption, or proved P = NP. The 93% figure is a revisable editorial estimate of known reconstruction work, separate from the 108 of 110 scoped formal-publication rows and not a probability that the claim is correct.
Verified scope: For an arbitrary finite explicit minimal-consumer antichain and typed exact-BN5-coordinate restoration operation, Lean mechanically pairs every quotient atom with its restored full candidate as opposite-sign unit cells, proves the complete BN5 coordinate gives the same nested BN4 key, proves exact cell count and positive/negative multiplicity equality at every BN4 key, computes an empty canonical residual and zero signed mass at every key, and derives V54 singletonization from exact absence of every such proof-bearing cancellation outcome.
Boundary: The typed restoration operation and its complete coordinate maps remain explicit inputs, and the generated opposite-sign cells are not yet proved to be the cells of the terminal candidate's ambient BN4 ledger. This milestone does not construct semantic restorations from a terminal candidate, embed cancellation or Hall outcomes into the complete global route system, prove global route silence or the full historical PkgC theorem, establish full BN6 or Packet selector-realizer completeness, polynomial generation or runtime, ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 11
Core source: commit a46bc46175186748592af32661641fc232dae109, tree caddf0db1c54ee534653a1435047b796aac8025f, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-12-132.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 107
Lean now materializes finite typed PkgC restorations
For an arbitrary finite explicitly supplied minimal-consumer antichain and an explicitly supplied typed coordinate-preserving restoration operation, Lean now materializes one full-restoration candidate for every atom of the canonical first disjoint nonsingleton pair. It proves the exact candidate count and that every position keeps the source atom's complete coordinate.
The resulting equality-fibre graph has exact full and shadow multiplicities, gives complete coverage, and cannot satisfy a strict Hall deficit; when no nonsingleton pair exists, the classifier instead proves the V54 singletonization premise. The typed restoration operation remains caller-supplied, and Lean has not constructed it from a terminal candidate, proved its full semantic adequacy, connected restoration coverage to a BN4 or BN5 contradiction, completed PkgC route silence or global routing, established polynomial runtime, ZeroSlack, or PCCMin, put SAT in P, removed a project assumption, or proved P = NP. The 92% figure is a revisable editorial estimate of known reconstruction work, separate from the 107 of 109 scoped formal-publication rows and not a probability that the claim is correct.
Verified scope: For an arbitrary finite explicit minimal-consumer antichain and a typed coordinate-preserving restoration operation, Lean materializes typed full-restoration candidates for every atom of the canonical first disjoint nonsingleton pair, proves exact candidate count and positional coordinate preservation, derives complete equality-fibre multiplicity coverage, excludes a strict Hall deficit for that graph, and otherwise proves V54 singletonization.
Boundary: The typed restoration operation remains explicit caller data. This milestone does not construct it from a terminal candidate or prove its full semantic adequacy. It does not connect complete restoration to a BN4 or BN5 contradiction, embed local routes into the complete global outcome system, prove global PkgC route silence or the full historical PkgC theorem, establish full BN6 or Packet selector-realizer completeness, polynomial generation or runtime, ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 9
Core source: commit fe2c8ceb024d0a1afcb2a79a21015eb2969c37bd, tree 31e942af36667a728849744f7512fd690bbd3194, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-12-131.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 106
Lean now classifies finite PkgC separating consumers into singletonization or restoration
For an arbitrary finite explicitly supplied minimal-consumer antichain, Lean now scans in a deterministic order for the first disjoint pair that is not singleton-singleton. If no such pair exists, it proves exactly the singletonization premise used by the V54 normal form. If a pair is found, Lean canonically indexes its atoms as exact-coordinate quotient units and compares them with an explicit finite full-restoration universe.
The classifier returns complete multiplicity coverage or a strict Hall deficit with a deterministic local Q route, and every restoration edge preserves the full coordinate. The consumer antichain and restoration universe remain explicit inputs. Lean has not derived them from terminal candidates, connected complete coverage back to a BN4 or BN5 contradiction, embedded the local route into the complete global outcome system, proved global route silence or the full historical PkgC result, completed BN6 or Packet selectors and realizers, established polynomial runtime, ZeroSlack, or PCCMin, put SAT in P, removed a project assumption, or proved P = NP. The 91% figure is a revisable editorial estimate of known reconstruction work, separate from the 106 of 108 scoped formal-publication rows and not a probability that the claim is correct.
Verified scope: For an arbitrary finite explicit minimal-consumer antichain, Lean canonically scans for the first disjoint pair that is not singleton-singleton. Absence proves exactly V54's singletonization premise. A found pair's atoms are canonically indexed into exact-coordinate quotient units and an explicit full-restoration universe is classified into complete multiplicity coverage or a strict Hall deficit with a deterministic local Q route.
Boundary: The restoration coordinate universe remains explicit. This theorem does not derive consumers or restorations from a terminal candidate, connect complete coverage back to a BN4 or BN5 contradiction, embed the Hall route into the complete global outcome system, prove global route silence, or establish the full historical PkgC theorem. It does not prove full BN6 or Packet selector-realizer completeness, polynomial generation or runtime, ZeroSlack or PCCMin, SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 9
Core source: commit 49c463eb734ad7c11ece63177948c9df0af8f52a, tree 4622cebf0bf937b0f4d9c9decb62383aefe9b416, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-12-130.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 105
Lean now connects grouped V54 survivors to a finite BN6 packet classification
For an arbitrary finite set of anchors and an explicitly supplied, already-grouped family of positive survivor cells carrying payloads, Lean now converts their V54 cut activation into the exact V53 hypergraph cut sum. Given one common positive value on every nonempty proper cut, it returns the two-anchor pair case, the three-anchor mixed balanced-triple or full-span case, or the four-or-more-anchor full-span case, together with witnesses back to the original payloads.
The survivor family, grouping, payloads, PkgC singletonization proofs, and constant-cut equation remain explicit inputs. Lean has not constructed PkgC, derived or grouped the survivors from terminal candidates, established the full historical BN6 or Packet selector and realizer results, completed global routes, ZeroSlack, PCCMin, or polynomial runtime, put SAT in P, removed a project assumption, or proved P = NP. The 90% figure is a revisable editorial estimate of known reconstruction work, separate from the 105 of 107 scoped formal-publication rows and not a probability that the claim is correct.
Verified scope: For an arbitrary finite duplicate-free anchor carrier and explicit already-grouped family of positive payload-bearing survivor cells, V54 activation is transported exactly into the constructed V53 hypergraph cut sum. A positive BCEL constant-cut premise then yields the complete pair, mixed three-anchor balanced-triple/full-span, or four-or-more-anchor full-span classification with original payload witnesses.
Boundary: This finite bridge consumes explicit exact footprint grouping, PkgC singletonization proofs, positive atom ledgers, payload data, and the BCEL constant-cut equation. It does not construct PkgC, derive or group survivors from a terminal candidate, establish full historical BN6 or Packet selector/realizer completeness, complete global routes, prove polynomial generation or runtime, ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 8
Core source: commit d77a5faf194b86fd1175065a0930fd485e16ace5, tree 34344e42d12991af68f7ed81ca575cff0307f69a, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-11-129.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 104
Lean now proves finite V53 constant-cut hypergraph rigidity
For an arbitrary finite duplicate-free carrier and an explicitly supplied sparse positive weighted hypergraph, Lean now classifies every case in which all nonempty proper cuts have the same positive value. With two anchors the full-span weight is that value. With three anchors all pair weights agree and the full-span weight plus twice the common pair weight is that value. With four or more anchors every proper footprint has zero weight and the full-span weight is that value.
The hypergraph and constant-cut proof remain explicit inputs. Lean has not constructed PkgC, derived the hypergraph from terminal candidates or the V54 consumer system, built BN6 cells or payloads, completed global routes, ZeroSlack, PCCMin, or polynomial runtime, put SAT in P, removed a project assumption, or proved P = NP. The 89% figure is a revisable editorial estimate of known reconstruction work, separate from the 104 of 106 scoped formal-publication rows and not a probability that the claim is correct.
Verified scope: For an arbitrary finite duplicate-free carrier and sparse nonnegative weighted hypergraph with positive listed cells, exact equality of every nonempty proper cut proves the complete V53 q=2, q=3, and q>=4 classification: full-span weight D; one common pair weight p with w_A + 2p = D; or zero weight on every proper footprint with full-span weight D.
Boundary: This theorem consumes an explicit sparse positive hypergraph and an explicit proof that every nonempty proper cut has the same positive value. It does not construct PkgC, derive the hypergraph from a terminal candidate or the V54 consumer system, build BN6 cells or payloads, complete global routes, selectors, or realizers, establish polynomial generation or runtime, prove ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 10
Core source: commit 8e38de05d9e1b3066484c9fc5555813997076d02, tree 1aca9eafba5ac7a0aaf6d2fe63774a479ac24126, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-11-128.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 103
Lean now proves one finite V54 consumer-antichain normal form
For an arbitrary finite carrier and an explicitly supplied antichain of minimal consumers, Lean now proves that requests are monotone, the empty request is inactive, and two-sided cut activation is nonzero exactly when two consumers are disjoint. If every disjoint consumer pair is singletonized, the exact premise required by the manuscript's PkgC stage, Lean proves literal equality with the cut indicator of the singleton footprint.
The minimal-consumer antichain and singletonization proof remain explicit inputs. Lean has not constructed PkgC or route silence, derived these inputs from terminal candidates, completed V53 or BN6, established complete global routes, ZeroSlack, PCCMin, or polynomial runtime, put SAT in P, removed a project assumption, or proved P = NP. The 88% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For an arbitrary finite carrier and its explicit minimal-consumer antichain, Lean proves monotonicity and empty-request inactivity, proves that nonzero two-sided cut activation is equivalent to the existence of a disjoint consumer pair, and under the exact singletonized-disjoint-pair premise proves literal equality with the corresponding footprint cut indicator.
Boundary: This finite kernel starts from an explicit minimal-consumer antichain and an explicit proof that every disjoint consumer pair is singletonized. It does not construct PkgC, derive that singletonization premise, or connect the footprint back to the full BN6 proof. It does not construct complete global routes, selectors, or realizers; establish polynomial generation or runtime, ZeroSlack, or PCCMin; put SAT in P; remove a project assumption; or prove P = NP.
Reviewed theorem pins: 7
Core source: commit dd7b9be6ad6d05d516da2baf48813ae608c4e46d, tree d755c0b1ab7e407e11ce03428e7f1e68a03ca645, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-11-127.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 102
Lean now checks one finite BN5 full-shadow localization
Starting from one verified negative BN4 cancellation result, Lean now expands its mass into explicit unit records and compares those records with an explicit finite list of quotient-shadow coordinates. It checks whether the chosen cut is silent. When it is active, the classifier either returns complete multiplicity coverage or proves a strict Hall deficit: a specific group of full records has fewer distinct shadow neighbours, and the resulting local route cannot disappear silently.
The payloads, cut, and shadow universe remain explicit inputs rather than constructions from the four-corner bases. Complete matching is not yet connected back to a BN4 contradiction, and the full historical BN5 diagnosis, later package and BN6 stages, complete global routing, polynomial runtime, ZeroSlack, PCCMin, SAT in P, removal of a project assumption, and P = NP remain unproved. The 87% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every explicit finite negative-unit refinement and quotient-shadow ledger, Lean preserves the complete exact-coordinate data, validates the negative mass refinement, computes whether the cut is silent, and otherwise returns either complete multiplicity coverage or a strict Hall deficit with a literal smaller shadow-neighbor fibre, complete-coordinate preservation, and a proof-bearing local X1 route that prevents active unmatched units from disappearing silently.
Boundary: This kernel starts from explicit finite inputs: one complete BN4 key, a negative cancellation result, a payload list, a cut, and a quotient-shadow coordinate list. It does not derive payloads or shadows from four-corner bases, connect complete matching back to a BN4 contradiction, or prove the full CritC/Q/E/L/X2/X3/X4 diagnosis, so it is not the full historical BN5 theorem. It does not construct PkgC or BN6; complete global routes, selectors, or realizers; establish polynomial generation or runtime, ZeroSlack, or PCCMin; put SAT in P; remove a project assumption; or prove P = NP.
Reviewed theorem pins: 12
Core source: commit b829e62744c3e645726f7cba9875fe6926a6b207, tree dc1e76c188b26b9311b2a65f8a8376f497cdd69d, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-11-126.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 101
Lean now checks one finite BN4 cancellation ledger
After the existing finite request-envelope classifier succeeds, Lean now gives each request identity one exact singleton activation code and compares complete typed cancellation keys without enumerating cuts. For an explicit ledger of positive and negative cells, it totals mass only at the same complete key, returns a canonical balanced, positive, or negative residual, and proves exact integer mass conservation, preserved key identity, positive residual mass, and absence of opposite-sign residual pairs.
The ledger, semantic signatures, and transport types are supplied explicitly rather than derived from the four-corner bases, so this is a finite cancellation kernel rather than the full historical BN4 theorem. It has no polynomial construction or size bound and does not construct BN5, PkgC, or BN6; complete global routes, selectors, or realizers; ZeroSlack or PCCMin; SAT in P; removal of a project assumption; or P = NP. The 86% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: After a successful computed finite BN3 envelope, Lean gives every request atom a canonical singleton activation code; proves activation-code equality exactly equivalent to equality of activation functions without enumerating cuts; checks equality of a complete typed key containing the atom, explicit semantic signature, and explicit transport type; totals positive and negative natural mass only at that same complete key; classifies a canonical balanced, positive, or negative residual; proves exact integer mass conservation, complete-key preservation, positive residual mass, and absence of opposite-sign residual pairs; computes duplicate-free ledger keys; and preserves all upstream failure branches while rejecting foreign request atoms.
Boundary: This is a finite cancellation kernel over an explicit typed cell ledger. It does not derive cells, semantic signatures, or transport types from four-corner bases and is not the full historical BN4 theorem. It supplies no polynomial construction or size bound; does not construct PkgC or BN6; does not complete global routes, selectors, or realizers; does not establish ZeroSlack or PCCMin; does not put SAT in P; does not remove a project assumption; and does not prove P = NP.
Reviewed theorem pins: 13
Core source: commit ef94583b39f7050953a78a7a6e0ad431cd2eb459, tree b82aecb1817c83a2b3ec840680aa0f9a9f31870b, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-11-125.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 100
Lean now constructs one finite BN3 request envelope
After the existing finite anchor classifier succeeds, Lean now constructs one canonical duplicate-free list of request identities across every proper cut. It proves that executable request membership is exact, monotone, and stable, computes exact singleton minimal consumers, accounts for each active incidence once, and selects one shared full-or-quotient side-tight basis family for all cuts while preserving every earlier proof-bearing failure.
This is an exact finite reference construction, but it checks every subset of the anchor family and can therefore take exponential time. It does not construct the later BN4 through BN6 stages, prove complete selector or realizer coverage, establish global ZeroSlack or polynomial PCCMin, put SAT in P, remove a project assumption, or prove P = NP. The 85% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: From every successful computed finite BCEL anchor nucleus, Lean uses one canonical duplicate-free primitive-record identity list across every proper cut; gives exact executable monotone request membership stable under extensional transport and exact singleton minimal consumers; accounts active incidences without duplicates; selects one canonical full or quotient side-tight coherent basis for every proper cut; and preserves all upstream proof-bearing classifier failures in a total outcome.
Boundary: This establishes one exact candidate-derived finite BN3 envelope only after the existing computed BCEL anchor-nucleus classifier succeeds. Proper cuts are enumerated through all subsets, so the construction is exponential reference computation rather than a polynomial algorithm. It does not derive the terminal dependency system, map local routes into the manuscript's complete global outcome system, construct BN4-BN6, prove selector or realizer completeness, establish global ZeroSlack or PCCMin, prove SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 11
Core source: commit 85c72816225bc6feab4ffc60499475419645dd73, tree 773d96dae8e14038cc35893dc85402a25bf1b655, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-11-124.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 99
Lean now publishes the concrete locked-NAND threshold reduction
Lean now proves one uniform polynomial-time transformation from encoded CNF satisfiability instances to the concrete locked-NAND threshold language. The witness is the fixed parser, circuit compiler, and locked-NAND emitter pipeline, and the theorem applies to every input bitstring with fail-closed malformed-input behavior.
The theorem depends only on standard Lean logical principles, not on the legacy project assumption with a similar name. It does not put the target language in P, prove concrete CNF-SAT NP-hardness, discharge residual-band minimization, ZeroSlack or PCCMin, establish polynomial certificate checking for the final route, remove the remaining project assumptions, or prove P = NP. The 84% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: A uniform encoded polynomial-time SAT instance builder and the report-level locked-NAND threshold theorem linked to that builder.
Boundary: This closes the uniform all-bitstring CNFSAT-to-concrete-locked-threshold builder and report-facing linkage in the finite charged-pipeline model. It does not put the concrete locked threshold language in P, discharge residual-band minimization, ZeroSlack or PCCMin, prove concrete CNFSAT NP-hardness, activate the legacy string-handle bridge, or prove P = NP.
Reviewed theorem pins: 1
Core source: commit 7445d2afa7af75375d20751b4a0aa7b87e8b8dfc, tree 7376c3d35ebfd9a80e38abb86964e60df6d4f4b3, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-11-123.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 98
Lean now fixes the residual terminal rank and proves it well-founded
Lean now defines the manuscript's residual terminal rank as exactly ten natural-number coordinates in the stated priority order. It proves that the executable Boolean comparison agrees with the lexicographic proposition, supplies a proof for each of the ten possible first-decreasing coordinates, packages proof-bearing descent, and proves accessibility, induction, and kernel-checked well-foundedness for the fixed rank.
This establishes the rank domain and RankWF only. It does not map the current finite terminal routes into the manuscript's complete global outcome system, prove that any current route strictly decreases the rank, establish route completeness or Package E, remove the explicit positive premise from the finite composition, establish manuscript-wide SaturatePositive or BCELReady, prove ZeroSlack or PCCMin, establish polynomial runtime, put SAT in P, remove a project assumption, or prove P = NP. The 83% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For the fixed manuscript residual rank of exactly ten natural coordinates in the stated witness-type, span-type, mode, frontier-defect, projection-defect, saturation-defect, anchor-count, charge-size, profile-size, canonical-code priority order, Lean provides the exact lexicographic proposition, an equivalent executable comparison, all ten priority witnesses, proof-bearing descent, accessibility, induction, and kernel-checked well-foundedness.
Boundary: This establishes the fixed residual rank domain and RankWF only. It does not map the current finite terminal routes into the manuscript's complete global outcome system, prove that any existing route strictly decreases the rank, establish route completeness or Package E, remove the explicit positive premise from the finite composition, establish full manuscript-wide SaturatePositive or BCELReady, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 18
Core source: commit dd69b94a762eb830a3b91503faffde3984cce84f, tree d06833216d204b8eca0510267654263e79752e51, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-10-121.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 97
Lean now composes the finite terminal positive-saturation route
For every finite direct-wire candidate, executable observer, forgetful projection, and proof-bearing terminal anchor problem whose normalized starting point has positive full slack, Lean now checks the candidate-derived origin, kernel, and obligation closures in both gate and profile orientations. It verifies that each safe step is cost transparent, discharges its closure obligation, preserves the forgotten profile, and preserves positive full slack through the complete safe prefix into either the checked-lift or BCEL firewall. Otherwise it returns the exact first local route or nontransparent event together with that complete safe prefix.
This composes the five reconstructed finite terminal obligations only for an explicit proof-bearing problem and closes the finite local form of originKernelObligationClosureRouted. A returned local route is not a complete global outcome, full Package E acceptance, verified gain, or proof of global route completeness, and the initial positive full-slack premise remains explicit. Lean has not established manuscript-wide SaturatePositive, BCELReady or RankWF, proved ZeroSlack or PCCMin, established polynomial runtime, put SAT in P, removed a project assumption, or proved P = NP. The 82% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, executable ambient observer, forgetful projection, and proof-bearing candidate BCEL anchor problem whose normalized seed has positive full slack, Lean recognizes exact candidate-derived origin, kernel, and obligation closures in both gate/profile orientations; checks cost transparency, obligation discharge, and forgotten-profile stability; preserves positive full slack across an all-safe trace into the checked-lift or BCEL firewall; or returns the exact first interface, closure, or other fail-closed nontransparent route with its complete safe prefix.
Boundary: This closes the finite local form of originKernelObligationClosureRouted and composes the five reconstructed terminal sub-obligations only for an explicit proof-bearing problem. A local route is not a complete global outcome, Package E VerifyDW acceptance, verified gain, or global route-completeness result. The positive initial full-slack premise remains explicit. It does not establish manuscript-wide SaturatePositive, BCELReady, RankWF, ZeroSlack, PCCMin, polynomial runtime, SAT in P; remove a project assumption; or prove P = NP.
Reviewed theorem pins: 9
Core source: commit 3f4352d190b44d34866500e672c2ef2af89e08de, tree 2133ae4be763f61dda2c6f8fcc6e194ba777feb2, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-10-120.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 96
Lean now routes finite terminal interface exposure
For every finite direct-wire candidate, executable ambient observer, forgetful projection, and finite terminal seed, Lean now recognizes only an exact interface-consumer edge derived from that candidate. Each recognized event is either proved transparently cost-balanced or turned into a proof-bearing local E-route. Across a saturation trace, Lean records the exact first interface-exposure event and the complete transparent prefix.
This closes only the finite local form of interfaceExposureRoutesToE. The local E-route identifies an exposure obligation; it is not a full Package E acceptance, verified global gain, or proof that every global route has been found. The observer and projection remain explicit inputs, and Lean has not discharged originKernelObligationClosureRouted, established full SaturatePositive, Package E or BCELReady, proved ZeroSlack or PCCMin, established polynomial runtime, put SAT in P, removed a project assumption, or proved P = NP. The 81% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, executable ambient observer, forgetful projection, and finite terminal seed, Lean recognizes only an exact candidate-derived interface-consumer edge. Each recognized event is transparently cost-balanced or produces a proof-bearing local E-route; the production trace result records the exact first nontransparent event and complete transparent prefix, while non-interface first failures remain fail-closed.
Boundary: This closes only the finite local form of interfaceExposureRoutesToE. The proof-bearing local E-route is an exposure-obligation coordinate, not a full Package E VerifyDW acceptance, a verified global gain, or global route completeness. The executable observer and forgetful projection remain explicit model inputs. It does not discharge originKernelObligationClosureRouted; establish full SaturatePositive, Package E, BCELReady or later BCEL/BN2-BN6 conclusions; prove ZeroSlack, PCCMin, polynomial runtime, SAT in P; remove a project assumption; or prove P = NP.
Reviewed theorem pins: 10
Core source: commit 19f43501ad87d4c5611ba109d53157fd0bd1dfdb, tree 574fa83fd6dd1b0d124770d1f577bf3f0147aaa4, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-10-119.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 95
Lean now derives and checks terminal saturation cost balance
For every finite direct-wire candidate, executable ambient observer, forgetful projection, and finite terminal seed, Lean now derives the physical and context-sensitive dependency system from the candidate itself and computes a deterministic rule-labelled saturation trace. If every event is transparent, Lean proves exact support and full-circuit cost balance while preserving full slack, positivity, and a nondecreasing projection defect across the linked history.
If an event is not transparent, Lean records the exact first event, its typed reason, and the complete transparent prefix instead of silently continuing. This closes only the finite terminal forms of transparentSaturationCostBalanced and firstNontransparentStepRecorded. The observer and projection remain explicit inputs, and Lean has not routed a nontransparent event, discharged interfaceExposureRoutesToE or originKernelObligationClosureRouted, established full SaturatePositive, Package E or BCELReady, proved ZeroSlack or PCCMin, established polynomial runtime, put SAT in P, removed a project assumption, or proved P = NP. The 80% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, executable ambient observer, forgetful projection, and finite terminal seed, Lean computes the candidate-derived dependency system and deterministic rule-labelled saturation trace, then returns proof that every event is exactly cost-balanced with preserved full slack and nondecreasing projection defect, or records the exact first nontransparent event and complete transparent prefix.
Boundary: This closes only the finite terminal forms of transparentSaturationCostBalanced and firstNontransparentStepRecorded. The executable observer and forgetful projection remain explicit model inputs, and a nontransparent event is recorded rather than routed. It does not discharge interfaceExposureRoutesToE or originKernelObligationClosureRouted; establish full SaturatePositive, Package E, BCELReady or later BCEL/BN2-BN6 conclusions; prove ZeroSlack, PCCMin, polynomial runtime, SAT in P; remove a project assumption; or prove P = NP.
Reviewed theorem pins: 17
Core source: commit ead67f4864902e667e5fd436eea21c61de2f871e, tree 072fe73440ac21f5daa7a9a3a79b51deb459aeb6, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-09-118.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 94
Lean now computes whether terminal projection positivity is lost
For an explicit finite direct-wire candidate, terminal dependency system, already computed governed proper-positive support, forgetful projection, and executable observer, Lean now computes the whole-support projection defect and handles both possible cases. If the defect is zero, it returns an attained reduced minimum together with a checked full lift. If the defect is positive, it delegates exactly to the existing fail-closed BCEL anchor-nucleus classifier.
This closes only the named projectionPositivityNotLostSilently obligation in the current finite terminal model. It does not derive the dependency system or support, discharge the other four SaturatePositive obligations, establish full SaturatePositive, Package E or BCELReady, prove ZeroSlack or PCCMin, establish polynomial runtime, put SAT in P, or prove P = NP. The 79% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, explicit terminal dependency system, computed governed proper-positive support, forgetful projection, and executable ambient observer, Lean computes the whole-support defect: zero projection defect returns an attained quotient minimum with a checked full lift, while positive defect delegates exactly to the existing fail-closed BCEL anchor-nucleus classifier.
Boundary: This closes only projectionPositivityNotLostSilently in the current finite terminal model. It assumes an explicit terminal dependency system and an already computed governed proper-positive support. It does not discharge transparentSaturationCostBalanced, interfaceExposureRoutesToE, originKernelObligationClosureRouted, or firstNontransparentStepRecorded; establish full SaturatePositive, Package E, BCELReady or later BCEL/BN2-BN6 conclusions; prove ZeroSlack, PCCMin, polynomial runtime, SAT in P; remove a project assumption; or prove P = NP.
Reviewed theorem pins: 12
Core source: commit e6fcbad711f1bdfcc67d8e4c748f2a65d192b8a5, tree 1a326290d19798563b9ed4680228ff595b620248, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-09-117.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 93
Lean now computes the canonical positive anchor nucleus and checks every proper cut
For an explicit finite direct-wire candidate, terminal dependency system, governed proper-positive support, forgetful projection, and executable observer, Lean now enumerates every candidate anchor subfamily and selects the unique canonical minimum-cardinality one with positive projection defect. It then checks the anchor algebra and every proper cut in a deterministic order.
The classifier is fail-closed: it returns an insufficient nucleus, the exact first anchor-algebra mismatch, the exact first proper-cut defect mismatch, the first proof-bearing full-before-reduced local route, or exact constant-cut and local BN2 conclusions for every proper cut. This milestone assumes both the terminal dependency system and a positive whole-support projection defect. It does not derive either premise, identify the manuscript's activation or charge classes, connect every local failure to the complete global route system, or establish SaturatePositive, Package E, BCELReady, ZeroSlack, PCCMin, polynomial runtime, SAT in P, or P = NP. The 78% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, explicit terminal dependency system, computed governed proper-positive support, forgetful projection, executable ambient observer, and positive whole-support projection defect, Lean computes the canonical minimum-cardinality positive anchor nucleus and returns either an insufficient nucleus, the exact first anchor-algebra mismatch, the exact first proper-cut defect mismatch, the proof-bearing first full-before-quotient local route, or exact constant-cut and local BN2 conclusions for every proper cut.
Boundary: This milestone assumes a positive whole-support projection defect and an explicit terminal dependency system. It does not derive either premise, identify manuscript activation or charge equivalence classes absent from the terminal model, connect a local failure to the complete global no-outcome route system, establish SaturatePositive, Package E, BCELReady or later BCEL/BN2-BN6 conclusions, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 36
Core source: commit f0bad8053fa334d4d996abd8ee5b796138526ec8, tree 2e5ee34ffcea47219605756ef3041246996c734c, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-09-116.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 92
Lean now constructs and checks the complete computed four-view square
Given two finite seed lists and one explicit set of terminal dependency rules, Lean now computes the four related terminal-support views, completes the governed frontier at every corner, and proves that the frontier and its reduced projection form the exact compatible square required by this local model. It also keeps the full and reduced minimum quantities on one checked carrier, so the comparison does not silently change what is being measured.
The final checker is fail-closed: when the exact local route queries are silent, Lean returns the complete local square conclusion; otherwise it returns the first full-then-reduced mismatch together with a proof that the route is real. This is computed BN2 square legitimacy for the explicit finite data, not the manuscript's unrestricted conclusion. Lean has not derived the dependency rules from an arbitrary circuit, proved universal route silence, connected every local failure to the complete global no-outcome route system, identified a BCEL anchor square, or completed SaturatePositive, ZeroSlack, PCCMin, polynomial runtime, SAT in P, or P = NP. The 77% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite computed terminal support square built from two finite seeds under one explicit terminal dependency system, direct-wire candidate, observer, and forgetful projection, Lean constructs the exact compatible governed frontier and projection square, keeps full and quotient minimum quantities on the same carrier, and returns either the complete local conclusion under exact local route silence or the deterministic full-then-quotient proof-bearing first coherence route.
Boundary: This milestone packages computed structural legitimacy and the exact local no-route conclusion. It does not derive the terminal dependency system from an arbitrary circuit, prove universal route silence, connect a local failure to the complete global no-outcome route system, identify a BCEL anchor square, establish SaturatePositive, Package E, BCELReady or later BCEL/BN2-BN6 conclusions, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 20
Core source: commit ca60f66498eaa4a6242e15c86fa86a2fe62e78f9, tree 86a19d87f564dd644f78ceea604c18a30ad223ca, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-09-115.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 91
Lean now checks every smallest four-view combination and takes the exact largest result
A computer circuit is a network of simple yes-or-no operations. This part of the proposed proof compares four related views of one circuit. Each view can have several different designs tied for the smallest size. Lean now lists every smallest design for all four views, tries every possible four-way combination, and keeps exactly the combinations that agree where the views overlap.
When the existing local mismatch check finds no problem, Lean proves that at least one matching combination remains and that every retained combination gives the same signed number. It therefore calculates the exact largest value without incorrectly replacing a negative answer with zero. This works in both the full and reduced comparison modes. Lean has not proved that every square passes the local check, established the manuscript's BN2 square-legitimacy theorem, or completed SaturatePositive, ZeroSlack, PCCMin, polynomial runtime, SAT in P, or P = NP. The 76% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite computed terminal support square, every explicit observer, and either full or quotient mode, Lean enumerates the complete finite tight-basis family, retains every exact profile-constrained minimum implementation at each corner, filters the full Cartesian product with the arbitrary-family coherence query, and proves under exact local route silence that the signed maximum equals the selected delta.
Boundary: This milestone closes the remaining local BN2 tight-basis maximum under computed local route silence. It does not prove universal route silence, connect a local obstruction to the complete global no-outcome route system, prove BN2 square legitimacy, derive the terminal dependency system, establish SaturatePositive, Package E, BCELReady or BCEL/BN2-BN6, complete obstruction routing, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 28
Core source: commit fc47845928f2cafb4f7ebbafed38e5e7a8a6c25a, tree fa466d44f3d5cd15ebcd6fabe0a961582cb66c25, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-08-114.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 90
Lean now completes the four-view check when no local mismatch appears
This section of the proposed proof compares four related smallest circuit views. The previous update gave Lean a fixed checklist for finding the first local mismatch between them. Lean can now finish the other side of that checklist: when the relevant checks report no mismatch, it constructs one verified package showing that the four selected views fit together in the chosen comparison mode and reach the exact required size balance.
This result applies to every finite square covered by the formal model and keeps the full and reduced comparison modes separate. It is conditional on the local checklist finding no problem. Lean has not proved that this happens for every square, connected every local problem to the manuscript's complete obstruction route, or proved the manuscript's BN2 square-legitimacy theorem. Later SaturatePositive, ZeroSlack, PCCMin, polynomial runtime, SAT in P, and P = NP obligations remain open. The 75% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite computed terminal support square, every explicit observer, and either full or quotient coherence mode, the exact first local coherence query returns a proof-bearing sound route or, under computed local route silence, Lean supplies the complete checked side-tight coherent optimum tuple with exact minimum incidence value while retaining the separate quotient-promotion firewall.
Boundary: This milestone closes only the local completion edge under computed local route silence. It does not prove universal route silence, connect a local obstruction to the complete global no-outcome route system, prove BN2 square legitimacy, derive the terminal dependency system, enumerate or maximize the complete tight-basis family, establish SaturatePositive, Package E, BCELReady or BCEL/BN2-BN6, complete obstruction routing, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 20
Core source: commit 78c8862e74f251622cdd2eed65e44fd3d0586301, tree 763dcc3b89004639f93e483e4464b3faf7ac4bf7, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-08-113.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 89
Lean can now check whether four smallest circuit views fit together
This part of the proposed proof compares four related views of a computer circuit, each represented by a smallest known circuit for that view. Lean can now check whether those four choices agree where the views overlap. It checks the four connections in a fixed order, so the result does not depend on guesswork or on which comparison happens to be tried first.
If every check passes, Lean returns one package showing exactly how the four choices fit together and retains the size and boundary facts needed by later work. If a check fails, Lean identifies the first exact reason, such as a missing connection, a changed output, a mismatched bookkeeping pattern, or use of the wrong comparison mode. This works for every finite square covered by the model. It does not prove that every square passes, complete the manuscript's square-legitimacy step, or establish P = NP. The 74% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite computed terminal support square, every explicit observer, every terminal projection, and either full or quotient coherence mode, Lean checks the four square legs in a deterministic order and returns either one coherent canonical optimum tuple with exact transport, side-tight, and incidence facts or the exact deterministic first failure.
Boundary: This milestone classifies coherent transport or its exact first failure. It does not prove that every square is coherent, construct the later no-outcome route, prove sideTightCompletionExists or BN2 square legitimacy, establish SaturatePositive, Package E, BCELReady or BCEL/BN2-BN6, complete obstruction routing, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, removal of a project assumption, or P = NP.
Reviewed theorem pins: 19
Core source: commit 34713d47d7e00298aeb532dc9d5c69e57d11f296, tree 8f141b6aa8a7300309c15430e54bf093aceead14, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-08-112.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 88
Lean can now compare four independently smallest circuit views on one common map
This part of the proposed proof compares four related views of a computer circuit. For each view, earlier checked work identifies a circuit with the fewest gates. Those four smallest circuits could originally use different maps of their positions, which made a direct comparison unsafe. Lean now places all four on one finite common map without changing what any circuit does or how many gates it has.
Lean also proves that every real position can be translated to the common map and back exactly, while a missing position is rejected instead of being invented. This works for every finite computed square covered by the model and uses one shared way of observing all four circuit views. It still does not prove that the four smallest circuits fit together consistently along the square's sides, establish the manuscript's square-legitimacy step, or complete the later ZeroSlack, PCCMin, efficient-runtime, SAT-in-P, or P = NP obligations. The 73% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite computed saturated terminal support square and every explicit observer, Lean embeds all four exact corner candidates into one common ambient carrier, proves reversible semantic and gate-count preservation, proves exact ambient and corner reference minima agree, and localizes canonical full and quotient optima from one shared observer and projection without changing their exact minimum counts.
Boundary: This milestone compares independently attained full and quotient optima on one reversible common carrier. It does not prove coherent transport along the square legs, construct a coherent four-corner optimum, prove sideTightCompletionExists or BN2 square legitimacy, derive the terminal dependency system, establish SaturatePositive, Package E, BCELReady or BCEL/BN2-BN6, complete obstruction routing, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, removal of a project assumption, or P = NP.
Reviewed theorem pins: 30
Core source: commit df4f4d830f6a0fd44af51edb0be178652d1b9417, tree db7e1089cbeed18e98a48bbb5000f0985608f1c9, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-08-111.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 87
Lean can now keep the same circuit positions aligned across four related views
This part of the proposed proof compares four related views of a computer circuit: the part two alternatives share, each alternative on its own, and the result of combining them. Lean now gives those views one common map of positions. It proves that every boundary and connection is listed exactly and that no position is accidentally counted twice, so the same wire or bookkeeping item keeps the same identity in all four views.
Lean also checks every position that appears on either side. It proves that the position either remains visible after the sides are combined or becomes internal for a verified reason, and its lookup rejects positions that are not actually present. This works for every finite computed square covered by the model, not one selected example. It still does not construct four compatible optimum circuits, one coherent four-corner minimum, or the manuscript's square-legitimacy result. Later minimization, efficient runtime, ZeroSlack, PCCMin, and P = NP remain open. The 72% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite computed saturated terminal support square, direct-wire candidate, and forgetful terminal projection, Lean derives all four exact governed and extracted endpoints in common ambient coordinates, proves duplicate-free boundary, interface, and profile lists, transports meet and join profiles exactly, and classifies each present side physical coordinate as identically retained or constructively internalized through fail-closed queries.
Boundary: This milestone supplies a checked common ambient carrier for the computed square. It does not transport four optimum realizers, prove the full four-corner optimum carrier-compatibility obligation, construct a coherent four-corner optimum, prove side-tight completion or BN2 square legitimacy, establish SaturatePositive, Package E, BCELReady or BCEL/BN2-BN6, complete obstruction routing, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, removal of a project assumption, or P = NP.
Reviewed theorem pins: 27
Core source: commit 45e828437ed335a62dbc4e9889e65ee383c53139, tree 89d37dd773ec1369ee22d97f8ee0cb3c9da41c9b, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-07-110.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 86
The proof now checks when four related circuit comparisons reach their exact minima
A later part of the proposed proof compares four related views of a computer circuit: the part they share, two alternatives, and their combination. Each view has a smallest possible size under the formal rules. Lean can now check whether all four sizes are exactly minimal and, when they are, calculate their combined difference without losing track of any excess size.
The result applies to every finite four-view family covered by this model, not one chosen circuit. The checker fails closed if even one corner is not exactly minimal. An important limitation remains: the four minima may come from four different constructions, so Lean has not yet built one coherent four-corner object that reaches all of them together. Square legitimacy, efficient runtime, ZeroSlack, PCCMin, and P = NP remain open. The 72% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite terminal projection four-corner family and every independently attained typed full or quotient basis, Lean proves componentwise minimum bounds and the exact signed four-slack identity. A fail-closed Boolean and Option gate returns the corresponding existing delta only when meet, left, right, and join all attain their exact minima; both canonical independently attained minimum bases pass.
Boundary: The canonical corner minima are independently attained. This milestone proves numerical arithmetic and fail-closed exactness, not construction of one coherent four-corner basis, coherent completion, maximization over a finite tight family, BN2 square legitimacy, SaturatePositive, Package E, BCELReady or BCEL/BN2-BN6, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, removal of a project assumption, or P = NP.
Reviewed theorem pins: 24
Core source: commit 4aad02a158f05e18809748e8a6234ea568b76bfc, tree 0781b85b3960a177bd421aff73aa88c07370af0a, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-07-109.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 85
The proof now keeps its structure when extra bookkeeping is hidden
A computer circuit can be split into overlapping parts. The previous milestone proved that Lean could combine the descriptions of two completed parts. This milestone adds a controlled way to hide selected bookkeeping details and proves that the visible result still has the same physical boundary and shared information.
It does this for every finite circuit covered by the formal model and every allowed choice of details to hide, rather than for a fixed example. Combining first and hiding later gives the same visible structure as hiding each side first and then combining them. The dependency rulebook is still supplied, and important mathematical and efficiency steps remain open. This does not prove that P equals NP. The 71% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, explicit terminal dependency system, computed saturated support square, and every forgetful terminal projection, Lean retains the exact physical frontier, filters all ten role profiles exactly, proves projected meet is the shared side overlap, and proves projected join is the side-only projected pushout without reading the join corner.
Boundary: The terminal dependency system remains explicit input rather than a profile frontier derived from the circuit. This milestone proves structural projection commutation for computed saturated support squares, not side-tight four-corner minima, BN2 square legitimacy, SaturatePositive, Package E, BCEL/BN2-BN6, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, removal of a project assumption, or P = NP.
Reviewed theorem pins: 23
Core source: commit 23abd2eaf8913ea91dc1cf379878f278b9ee3d10, tree 5d2486bd4233650eb4a4186ababb9db99ac57f17, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-06-108.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 84
The proof can now combine the boundaries of two completed circuit parts
A circuit is a collection of simple yes-or-no operations connected by wires. Lean could already complete two chosen parts and describe each one's boundary. It can now combine those two descriptions to build the boundary of everything covered by either part, while keeping exactly the information the parts share.
Lean proves that this combined description matches a separate calculation made from the completed whole. Each item at either side's boundary is accounted for: it remains exposed or becomes internal to the combined part. The dependency rulebook is still supplied rather than derived from the circuit. The required projection-compatible square, obstruction routing, efficient runtime, ZeroSlack, PCCMin, and P = NP remain open. The 70% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, explicit terminal dependency system, and computed saturated support square, Lean constructs the governed boundary, interface, and role-preserving profile pushout from the two side completions alone. The independently completed join frontier equals that gluing, the meet profile is the exact shared overlap, and every side physical coordinate is either retained externally or witnessed as internalized.
Boundary: The terminal dependency system remains explicit input rather than a profile frontier derived from the circuit. This milestone proves exact frontier gluing for computed saturated support squares, not projection compatibility, side-tight four-corner minima, BN2 square legitimacy, SaturatePositive, Package E, BCEL/BN2-BN6, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, removal of a project assumption, or P = NP.
Reviewed theorem pins: 28
Core source: commit 31937a36ecc21413e334e5e7f7f27058f0dfecc7, tree 795ca7177f7a99e301b19e4dca7c3abac914d1ef, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-06-107.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 83
The proof can now organise each completed circuit part into one consistent boundary
A circuit is a collection of simple yes-or-no operations connected by wires. Lean can now take any finite chosen part that has been completed under a supplied dependency rulebook, identify exactly which wires enter and leave it, and sort its selected bookkeeping positions into ten distinct roles. The result is calculated by the formal construction rather than supplied as a separate certificate.
Lean proves that every selected record is covered, no profile position is duplicated or assigned to two roles, every required dependency remains present, and the completed part is physically compatible. The same guarantees now apply to all four related parts from the previous milestone. The dependency rulebook is still supplied rather than derived from the circuit, and obstruction routing, the required projection square, efficient runtime, ZeroSlack, PCCMin, and P = NP remain open. The 69% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, explicit terminal dependency system, finite seed list, and computed saturated support-square corner, Lean computes the exact physical boundary, ordered interface, and partition of selected profile coordinates among all ten terminal profile roles. It proves exact membership, no duplicates, pairwise disjointness, record coverage, dependency closure, physical compatibility, and retention of each exact corner.
Boundary: The terminal dependency system remains explicit input rather than a profile frontier derived from the circuit. This milestone computes a governed finite completion of each saturated support-square corner, not the manuscript's obstruction routing, frontier pushout, projection-compatible square, side-tight four-corner minima, BN2 square legitimacy, SaturatePositive, Package E, BCEL/BN2-BN6, complete residual routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, removal of a project assumption, or P = NP.
Reviewed theorem pins: 26
Core source: commit c225e91eeb469cd87f0c52c9731074e8b66fc573, tree 9616b6c150124561a7f88672aa20a34bba1a4aae, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-06-106.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 82
The proof can now combine two completed circuit parts without losing their shared structure
A circuit is a collection of simple yes-or-no operations connected by wires. Some later proof steps need to compare two chosen parts at once. Lean can now start from any two finite lists under a supplied dependency rulebook, complete both lists, and calculate four related parts: what they share, the completed left and right parts, and everything covered by either side.
Lean proves all four parts obey every supplied dependency, the shared part is the largest one contained in both sides, and the combined part is the smallest one containing both. It also rebuilds each part as an induced circuit with the expected inputs and outputs. The rulebook is still supplied rather than derived automatically, and the harder manuscript requirements for a projection-compatible square, routing obstructions, efficient runtime, ZeroSlack, PCCMin, and the final P versus NP theorem remain open. The 68% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, every explicit terminal dependency system, and every pair of finite terminal seeds, Lean computes saturated left and right corners, their canonical closed meet, and their closed saturated-union join. It proves the exact greatest-lower-bound and least-upper-bound laws, seed extensionality, computed physical compatibility, exact gate count, open-support semantics, and induced whole-circuit recovery for all four corners.
Boundary: The terminal dependency system remains explicit input rather than a profile frontier derived from the circuit. This milestone proves finite closed-corner algebra and computed physical extraction, not the manuscript's obstruction routing, frontier pushout, projection-compatible square, side-tight four-corner minima, BN2 square legitimacy, SaturatePositive, Package E, BCEL/BN2-BN6, complete residual routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, removal of a project assumption, or P = NP.
Reviewed theorem pins: 23
Core source: commit 7e4f3a683f87f0009c2c6010678ff022638bc8b8, tree ee1727221b3600193b9f622dc1cc060c3b2c8833, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-06-105.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 81
The proof can now search for a genuinely smaller useful part of a circuit
A circuit is a list of simple yes-or-no operations connected by wires. Lean can now examine every possible starting selection from a supplied finite dependency system, complete all recorded dependencies, and test whether the resulting part is nonempty, genuinely smaller than the whole circuit, and improves the exact size comparison.
Lean proves that this finite search finds a qualifying part whenever one exists in that governed search space, and that the extracted smaller circuit preserves the intended boundary behaviour. The dependency system is still supplied rather than derived from the circuit, and the search is exhaustive rather than efficient. It does not complete the manuscript's full support or square arguments, finish ZeroSlack or PCCMin, provide a polynomial-time algorithm, or prove P = NP. The 67% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate and explicit terminal dependency system, Lean enumerates the complete canonical finite universe of primitive-record seeds, saturates and physically completes each seed, extracts its exact open support, and computes exact local gain from the exhaustive semantic reference minimum. The search returns a proof-bearing nonempty proper support with positive gain whenever one exists in that canonical seed universe, and its none result is equivalent to the absence of such a seed.
Boundary: The terminal dependency system remains explicit input rather than a profile frontier derived from the circuit, and the search is exhaustive reference computation rather than a polynomial algorithm. This milestone does not prove global gain completeness, full manuscript support completion or square legitimacy, instantiate a projection-compatible square, prove SaturatePositive or BCELReady, discharge Package E or BCEL/BN2-BN6, generate a complete residual route, prove ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 22
Core source: commit bdbbabc67f20b5d4f673e11098ba86a9d10a1cf1, tree c26d7b20ab7d5241ad4fc7f214ac06b9477e78c6, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-05-104.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 80
The proof can now rebuild any chosen part of a circuit
A circuit is a collection of simple yes-or-no operations connected by wires. Lean can now select any collection of operations, including a scattered collection, and turn that selection into a smaller circuit of its own. It identifies every value entering the selection, rebuilds the selected operations in their original order, and exposes every selected result that the rest of the circuit uses.
Lean proves the rebuilt circuit has exactly the selected number of operations and gives the intended outgoing values for every possible set of incoming values. When those incoming values come from the original whole circuit, the extracted circuit reproduces the original results, including after the dependency checklist is completed. The record list and dependency links are still supplied rather than derived automatically, and this does not construct the manuscript’s proper positive support or required square, finish ZeroSlack or PCCMin, provide a polynomial-time algorithm, or prove P = NP. The 66% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate and finite terminal record list, including noncontiguous selections, the actual program is structurally extracted over its exact canonical incoming boundary and ordered outgoing interface. The extracted candidate equals an independently defined open-support function for every boundary valuation and recovers the original interface values on whole-circuit-induced boundaries; the construction also composes with executable terminal saturation.
Boundary: The record list and terminal dependency system remain explicit inputs rather than the manuscript's derived profile frontier. This milestone does not construct a proper positive support, prove full governed support completion or square legitimacy, instantiate the required projection square, prove SaturatePositive, discharge Package E or BCEL/BN2-BN6, generate a complete residual route, prove ZeroSlack or PCCMin, establish polynomial runtime, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 21
Core source: commit 5bc35c370e0d8987c69bd51f7f31e29070f7c162, tree 9f28a98946ada047b8a3beb50158239d66ecf5d9, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-05-103.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 79
The proof can now account for every wire crossing a chosen part of a circuit
A circuit is a collection of simple yes-or-no operations connected by wires. Lean can now take any chosen group of operations in any finite circuit, finish its recorded dependency checklist, and identify every wire that brings a value into the group or carries a result out. The result is put in one consistent order, even if the starting checklist was duplicated or scrambled.
Lean proves that no crossing wire is missed and no unrelated wire is added: constants stay inside, wires between chosen operations stay internal, and wires connecting to the rest of the circuit appear on the correct side. This still does not complete the extra bookkeeping records required by the manuscript, construct the positive witness, prove the required four-part square, finish ZeroSlack or PCCMin, provide a polynomial-time algorithm, or prove P = NP. The 65% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire candidate, explicit terminal dependency system, and finite seed list, a deterministic finite work list computes exactly the inductive saturation, then the actual program computes canonically ordered incoming boundary and outgoing interface wires. Lean proves no crossing wire is omitted or added and the composed physical support is compatible.
Boundary: The terminal dependency system remains explicit data rather than an extracted profile frontier. This milestone does not construct proper positive support, prove support completion in the manuscript's full sense or square legitimacy, instantiate the required projection square, prove SaturatePositive, discharge Package E or BCEL/BN2-BN6, generate a complete residual route, prove ZeroSlack or PCCMin, establish polynomial runtime, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 14
Core source: commit 9a01a9aee903b0d76132e80d40eed9004dc4eae1, tree 10972cee78cd0c70926b2ea13fbe073e6202a43d, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-05-102.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 78
The proof can now complete a finite checklist under every recorded dependency
A later part of the proposed proof needs to start with a set of facts about a circuit and repeatedly add every other fact those facts depend on. Lean now defines that process for any finite checklist and any explicitly supplied dependency links. It proves the process includes everything initially selected and continues until no recorded dependency is missing.
Lean also proves this completed checklist is the smallest one with those properties: starting with more facts cannot produce fewer, running the process again changes nothing, and a checklist is unchanged exactly when it was already complete. This does not yet create the correct dependency links from an arbitrary circuit or build the manuscript’s required support square. It does not complete ZeroSlack or PCCMin, provide a polynomial-time algorithm, or prove P = NP. The 64% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite terminal primitive-record universe and every explicit Boolean dependency system tagged by the manuscript's ten closure mechanisms, the generated reflexive transitive closure contains the seed, is dependency-closed, is least among closed supersets, is monotone and idempotent, and has exactly the closed supports as fixed points.
Boundary: This closure theorem does not derive the dependency relation from an arbitrary circuit, construct proper support, prove support completion or square legitimacy, instantiate a projection-compatible square, prove SaturatePositive or BCELReady, discharge Package E or BCEL/BN2-BN6, generate a complete residual route, prove ZeroSlack or PCCMin, establish polynomial runtime, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 7
Core source: commit e355c176bd0e961b5db41dd11fc5b2ccfe6642fb, tree 2ab1d800d697d4f6f0fa360615f4315ff277c022, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-04-101.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 77
The proof now balances four related circuit comparisons
Sometimes this proof compares circuits using a complete checklist of their behaviour, and sometimes it uses a shorter checklist that deliberately ignores selected details. This update considers four related cases: the common part, two alternatives, and their combined case. It proves an exact accounting rule for how the shorter checklist changes the measured size differences. The rule applies only when all four cases use the same checklist and the same way of omitting details.
Under the stated conditions, if no information is lost in the common part or either alternative, but the combined case loses D circuit operations, then the accounting difference is exactly D; if D is greater than zero, the difference is too. Lean checks increases and decreases correctly. It does not construct the four cases, prove that the manuscript’s required support and saturation objects exist, complete ZeroSlack or PCCMin, provide a fast algorithm, or prove P = NP. The 63% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire four-corner terminal-profile family sharing one computed observer and one explicit projection, signed full and quotient minimum deltas obey the exact Section 5.2 transfer identity. The projection excess is the quotient delta minus the full delta; if meet and both side defects are zero while the join defect is D, the excess equals D and is positive whenever D is positive.
Boundary: This is signed arithmetic over four supplied corners. It does not construct or certify a proper governed support square, prove SaturatePositive, discharge Package E or BCEL/BN2-BN6, generate a complete residual route, prove ZeroSlack or PCCMin, establish polynomial runtime, put SAT in P, remove a project assumption, or prove P = NP.
Reviewed theorem pins: 4
Core source: commit aa888e54beeff5be0162415fa962f80b4b18d113, tree d3978744cfd0f86905a6bc934b012a7468e1e49f, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-04-100.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 76
The proof now measures exactly what is lost when a circuit comparison ignores details
A circuit is a finite collection of simple yes-or-no operations. Two circuits can be compared using either a full checklist of their behaviour or a shorter checklist that deliberately ignores some details. Lean now exhaustively finds the smallest matching circuit under each checklist, proves that a circuit of each reported size really exists, and proves that no matching circuit can be smaller.
Ignoring details can never make the smallest matching circuit larger. Lean now measures the exact size gap between the two comparisons and proves that the gap is zero exactly when a smallest partial match also passes every omitted check. This exhaustive reference search is not an efficient algorithm and does not complete the remaining support, saturation, ZeroSlack, PCCMin, or complexity-theory work, so it does not prove P = NP. The 62% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire implementation, computed finite terminal-profile observer, and explicit forgetful projection, complete enumeration through the current gate count computes an attained full-profile minimum and an attained quotient-profile minimum. Both minima universally lower-bound every matching realization, forgetting coordinates cannot increase the minimum, the full minimum decomposes as the quotient minimum plus a nonnegative projection defect, and that defect is zero exactly when an attained quotient minimum has a checked full lift.
Boundary: These are exhaustive finite reference minima through the supplied implementation size. This milestone proves no polynomial runtime, proper or governed support construction, arbitrary manuscript quotient carrier, SaturatePositive, Package E, BCEL/BN2-BN6, complete residual routing, ZeroSlack certificate, PCCMin exactness, SAT-in-P result, discharged project assumption, or proof that P = NP.
Reviewed theorem pins: 14
Core source: commit accf07e45123837661307a37a02d2119ecd7aacc, tree 79f2ab904d9c90db6aa2d10ba2931c11a036b747, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-04-99.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 75
The proof now separates partial and complete circuit comparisons
A circuit is a finite collection of simple yes-or-no operations. Some proof steps compare only a selected checklist of facts about two circuits, while later steps need every relevant fact to match. Lean now records exactly which facts were kept, preserves the circuit, its number of operations, and all input-and-output behaviour, and prevents a partial comparison from being treated as a complete one without the missing checks.
A partial comparison can now be lifted to a complete comparison exactly when every omitted fact also agrees; keeping the full checklist makes that lift immediate. This is a safety boundary for future minimisation work, not a method for finding smaller circuits, completing the remaining support and saturation arguments, running the final algorithm efficiently, or proving P = NP. The 61% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Editorial progress estimate at publication: 61%.
Technical detailsShowHide⌄
Milestone:residual-terminal-mode-firewall
Classification: formalized-terminal-mode-firewall
Verified scope: For every finite direct-wire implementation, a computed finite profile observer records the ten terminal carrier roles and an explicit forgetful projection selects the quotient coordinates. Projection retains the exact implementation, gate count, and complete multi-output Boolean semantics. A quotient comparison has a checked full lift exactly when every forgotten profile coordinate agrees, lossless projections lift directly, and obligation discharge transports across a checked lift.
Boundary: This is a terminal comparison/lifting firewall only. It supplies no proper or governed supports, arbitrary quotient construction, support or projection-defect minimum, saturation, Package E, BCEL/BN2-BN6, packet or selector completeness, global residual route, ZeroSlack certificate, PCCMin exactness or polynomial runtime, SAT-in-P result, discharged project assumption, or proof that P = NP.
Reviewed theorem pins: 12
Core source: commit 1c9732052c9fbb05b7bea33887cfefea535a1c01, tree 88b8b18e0adc1e62d78d2b6b37bdfcb9d2a95332, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-04-98.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 74
The proof now compares a complete circuit at once
A circuit is a collection of simple yes-or-no operations. Lean now checks the full comparison for any finite circuit: another circuit counts as equivalent only when it gives the same answer for every possible input and every output. The wrapper used for that comparison also preserves the circuit and its exact number of operations.
Lean also checks that any cheaper complete equivalent circuit is genuine progress toward the smallest one, and that no such circuit exists exactly when the remaining size gap is zero. It does not provide an efficient way to find that circuit or finish the manuscript’s remaining minimisation and complexity-theory steps, and it does not prove P = NP. The 60% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite direct-wire implementation, terminalization preserves the exact whole implementation, gate count, and semantics at every input/output coordinate. An independently stated terminal minimum is attained, universally lower-bounds every complete terminal realization, and equals the exhaustive semantic reference minimum. Positive residual slack is equivalent to a cheaper whole-span full realization, every such realization gives strict residual descent, and zero slack is equivalent to absence of one.
Boundary: This is the direct-wire terminal full-mode specialization of the manuscript bridge. It does not formalize the quotient carrier or quotient-to-full firewall, proper or governed supports, SaturatePositive, BCEL/BN2-BN6, packet or selector completeness, route generation, the ZeroSlack certificate, PCCMin, polynomial minimum search or checking, SAT in P, discharge a project assumption, or prove P = NP.
Reviewed theorem pins: 13
Core source: commit 1361ec17b033acc591d0bd91a7a6e7ec552a449b, tree 3fd4f4bf9d41fbc7f1a56daf28b1060766df006a, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-03-97.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 73
A globally complete stop now certifies a smallest circuit
A circuit is a finite list of simple yes-or-no operations. Two circuits are equivalent when they give exactly the same outputs for every possible input. Lean now proves an exact rule for when an equivalent circuit cannot be made smaller: there is no smaller equivalent circuit anywhere exactly when the current circuit is already as small as possible.
This lets a previously checked shrinking sequence end with an exact minimum result, but only when a separate proof rules out every smaller equivalent circuit, not merely the circuits in a searched list. The milestone does not supply that global proof, an efficient search, the manuscript’s remaining ZeroSlack/PCCMin construction, or P = NP. The 59% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Editorial progress estimate at publication: 59%.
Technical detailsShowHide⌄
Milestone:residual-gain-stopping-specification
Classification: formalized-semantic-stopping-only
Verified scope: For every finite direct-wire implementation, positive exhaustive-reference residual slack is equivalent to the existence of some strictly smaller semantically equivalent implementation; zero slack and semantic minimality are each equivalent to global absence of such an implementation. A verified chain endpoint with separately proved global no-gain evidence therefore has zero slack and packages an exact minimum result.
Boundary: This is a semantic stopping criterion, not a stopping algorithm. It uses the exhaustive reference minimum as a mathematical witness and requires a proof quantifying over every finite implementation at the endpoint. It does not derive global absence from a finite scan, generate a route, prove candidate-list or route completeness, construct the manuscript's ZeroSlack certificate, establish polynomial checking or PCCMin runtime, put SAT in P, discharge a project assumption, or prove P = NP.
Reviewed theorem pins: 10
Core source: commit 1b5c1bc1f563d39c58b735c7163be661042c1356, tree 2daff0f133177f30a79e4d1ce01d44f721954124, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-03-96.
A circuit is a collection of simple yes-or-no operations. Sometimes one circuit can be replaced by a smaller circuit that gives exactly the same answers. Lean now checks a general rule for any finite sequence of these replacements: when every step is independently checked to keep all answers the same and to use fewer operations, the sequence cannot continue for longer than the starting gap between the current circuit and the smallest equivalent circuit.
For the locked comparison circuits already constructed in this project, that starting gap is at most four, so any such verified shrinking sequence has at most four steps. This rules out endless repetition, but it does not find the next smaller circuit, prove that every possible improvement will be found, or show that stopping early means the smallest circuit has been reached. Those search, completeness, runtime, and final P = NP steps remain open. The 58% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Editorial progress estimate at publication: 58%.
Technical detailsShowHide⌄
Milestone:residual-gain-chain-bound
Classification: formalized-iteration-bound-only
Verified scope: Every finite proof-bearing or executably verified chain of adjacent strict equivalent gains preserves semantics and the exhaustive reference minimum, while its endpoint residual slack plus its length is at most its starting residual slack. For the complete locked-NAND candidate, the existing residual-slack-at-most-four theorem specializes this to at most four verified gain steps.
Boundary: This milestone bounds only a disclosed, independently verified sequence. It does not find the next gain, prove route or candidate-list completeness, justify stopping after fewer than the bound, construct ZeroSlack, compute an exact minimizer, establish polynomial checker or PCCMin runtime, put SAT in P, discharge a project assumption, or prove P = NP.
Reviewed theorem pins: 14
Core source: commit 3894e5e2dd3f34c2fe19f6eb0b9e39119ad05403, tree 83f4874213a6c2be7c182d9e33d61a0e1b250acb, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-08-03-95.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 71
The CNF-to-NAND translation now runs as a checked efficient process
The previous update proved that a CNF formula and its NAND translation have the same yes-or-no answer. This update adds one fixed, inspectable machine that performs that translation for every possible input. Lean checks that valid formulas produce exactly the intended circuit, while malformed inputs stop safely and produce no result.
Lean also proves that the work grows at a polynomial rate with the input size, which is the standard efficiency requirement for this kind of translation. The checked machine is now packaged as a formal reduction from CNF satisfiability to NAND-circuit satisfiability and then connected to the existing locked-circuit conversion. It still does not decide CNF satisfiability efficiently, remove the remaining locked-circuit assumption, or prove P = NP. The 57% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: One fixed 135,070-rule three-node parser/carrier/controller work graph halts on every bitstring, rejects malformed CNF words with empty output, emits exactly compileEncodedCNFToNAND on every valid source, has one external encoded-input polynomial, compiles to a non-timeout PolynomialTimeFunction, retains literal RawRefinement, packages a direct PolynomialReduction from CNFSAT to EncodedNANDSAT, and composes it with the strict locked-NAND reduction to EncodedLockedNANDThreshold.
Boundary: This syntax-directed compiler does not itself decide CNF-SAT, put CNFSAT in deterministic polynomial time, establish SAT NP-hardness or CNFSAT NP-completeness, connect the concrete locked-NAND target to the abstract report-level threshold theorem, complete residual minimization or ZeroSlack/PCCMin, discharge any project assumption, or prove P = NP.
Reviewed theorem pins: 28
Core source: commit 3e60a7b270d4695da137a60d6a4a9ca59d3886f8, tree 04dbf61379eb4d24f1adc8419bf6e9d2dd636346, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-31-94.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 70
A general CNF formula can now be translated into NAND
A CNF formula is a list of yes-or-no requirements, while a NAND circuit is a network built from one simple universal logic operation. Lean now checks a general translation between these two forms and proves that a solution exists before the translation exactly when one exists afterward.
The proof covers empty formulas, empty clauses, invalid encodings, out-of-range variables, the exact number of added gates, and a polynomial limit on the output size. This is a semantic and size result, not yet the finite-machine polynomial-time reduction needed for the full complexity-theory bridge, and it does not prove P = NP. The 56% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Editorial progress estimate at publication: 56%.
Technical detailsShowHide⌄
Milestone:concrete-cnf-to-nand-semantic-compiler
Classification: formalized-semantic-boundary
Verified scope: A total answer-independent compiler transforms every strict canonical CNF formula into an intrinsically topological well-formed NAND circuit, preserves satisfiability exactly, proves the exact gate count and a quadratic serialized-output bound, fails closed on every malformed bitstring, and composes semantically with the concrete locked-NAND threshold builder.
Boundary: This milestone is the pure semantic and size-bound layer; the subsequent all-input milestone supplies the finite-machine, PolynomialTimeFunction, RawRefinement, and PolynomialReduction interfaces. Neither layer decides CNF-SAT, proves CNFSAT is in deterministic polynomial time, discharges the abstract report-level locked-NAND premise, completes ZeroSlack/PCCMin, or proves P = NP.
Reviewed theorem pins: 18
Core source: commit 95773a6583ca3d41f7b0c82090f000d9c6eb72da, tree 9890af1d8b919dd432ec00707eb5555d720000d1, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-31-93.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 69
The checked conversion is now a formal efficient reduction
A reduction is a reliable translation from one yes-or-no problem into another. The project already had checked machines that validate a circuit description and build the corresponding comparison object. Lean now packages those machines as one formal translation and proves, for every possible input, that the original circuit has a successful input exactly when the translated comparison passes its threshold.
Lean also records that this translation runs within an explicit polynomial limit, so the construction does not hide an impractical exhaustive search. This is an important complexity-theory bridge, but it does not yet connect ordinary CNF-SAT to this exact source format, prove that the target comparison can be solved efficiently, discharge the remaining assumptions, or prove P = NP. The 55% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: The existing strict parser/emitter composition is packaged as a concrete polynomial many-one reduction from EncodedNANDSAT to EncodedLockedNANDThreshold, with exact function identity, exact output, all-bitstring language equivalence, a ReducesTo witness, and recursive raw-machine refinement.
Boundary: The downstream all-input CNF compiler now identifies CNFSAT with this concrete source language through a fixed finite machine and a direct polynomial reduction, then composes with this reduction. This milestone does not discharge the abstract target-language assumption, prove the report-level locked-NAND threshold theorem, put CNFSAT in P, complete residual minimization or ZeroSlack, or prove P = NP.
Reviewed theorem pins: 5
Core source: commit 03f62a5465c1eacd399671121123a3891d8b3e67, tree 9ac174c23560579e75091fefda81f81e986b6cc1, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-30-92.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 68
A checked machine can now build the comparison circuit
A circuit description is a list of simple yes-or-no operations. The previous milestone added a machine that checks this description before it is used. This milestone adds a second fixed, inspectable machine that turns an accepted description into the larger comparison circuit required by the mathematical argument. Lean proves that every output bit matches the construction already defined in the formal development.
Malformed or invalid descriptions are rejected without leaving a result. Lean also proves that the running time and output size are bounded by explicit formulas based only on the input length, and that the checker and builder can be joined into one verified path. The remaining work includes packaging that path as the formal reduction needed by complexity theory and closing the still-open threshold, hardness, and final P = NP steps. The 54% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Editorial progress estimate at publication: 54%.
Technical detailsShowHide⌄
Milestone:concrete-locked-nand-target-emitter
Classification: formalized-foundation-only
Verified scope: One literal 1,387,921-rule grammar-only controller emits the exact direct locked-NAND target on every grammar-decoded circuit, rejects malformed grammar with empty output, cannot time out within an explicit all-input polynomial, has an explicit quadratic output-size bound, and supplies compiled polynomial-time machine/function witnesses, exact leaf RawRefinement, and strict parser/emitter composition computing buildLockedNANDInstance.
Boundary: The standalone emitter intentionally accepts every grammar-decoded raw circuit, including intrinsically invalid references; strict fail-closed semantics come from parser composition. The standalone emitter does not itself package the language equivalence as PolynomialReduction; the downstream concrete reduction milestone now does. The abstract locked-NAND threshold assumption, CNFSAT-in-P result, NP-hardness transport, and P = NP remain absent.
Reviewed theorem pins: 22
Core source: commit 23f53b6efccee3ff50987cf55338b8b01ddad343, tree 1549519b1c971a062b5315c8146272786a407648, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-29-91.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 67
Every circuit description now gets checked before use
A circuit description is a string of zeros and ones that tells a computer which simple yes-or-no steps to perform. Lean now proves that a fixed, inspectable machine checks every possible description from beginning to end. It verifies the format version, the stated counts, each operation, every reference to earlier data, all closing markers, and the exact end of the input.
Valid descriptions are accepted and returned unchanged. Anything malformed, including a reference to something that has not been defined yet, is rejected and produces no output. Lean also proves that this check always finishes within a stated size-based limit. This completes the input-checking half of the planned conversion; it does not yet build the comparison object, complete the full conversion, or prove P = NP. The 53% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Editorial progress estimate at publication: 53%.
Technical detailsShowHide⌄
Milestone:concrete-locked-nand-source-parser
Classification: formalized-foundation-only
Verified scope: One literal nine-symbol finite work machine validates every strict version-zero source bitstring: it accepts exactly ValidEncodedCircuit, preserves valid bytes, clears invalid bytes, cannot time out within the proved compiled cubic bound, and supplies polynomial-time machine/function witnesses plus the validator's exact leaf RawRefinement.
Boundary: This source parser alone does not emit the locked-NAND target or establish the source-to-target PolynomialReduction. The downstream emitter now supplies its own runtime/output bounds and strict composition, but the abstract locked-NAND threshold assumption, CNFSAT-in-P result, NP-hardness or NP-completeness transport, and P = NP remain absent.
Reviewed theorem pins: 20
Core source: commit a20c99f035eeb6bc3cafc7184bec6c40f9cbda22, tree 6114efcd6cf47f1e960eaf22bedc66e73ebb2f72, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-29-90.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 66
The circuit comparison now has an exact data format
A circuit is a list of very simple yes-or-no operations. To turn a mathematical construction into a real algorithm, its input and output need one exact bit format. Lean now fixes a strict version-zero format for the source circuit and the complete comparison object, proves that valid data can be encoded and decoded without changing its meaning, and normalizes outputs that were only an input or a constant.
The resulting pure transformation preserves the yes-or-no comparison: for valid encoded circuits, the constructed bytes cross the target size threshold exactly when the original circuit has a solution, while malformed inputs are rejected. This is a strategic bridge from the mathematical circuit theorem toward an algorithm, but it is not yet a bounded parser or emitter machine, a polynomial-time reduction, CNF-SAT in P, or P = NP. The 52% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: A strict version-zero bit grammar round-trips normalized NAND circuits and complete locked-NAND candidates; the pure all-bitstring transformation is fail-closed and preserves source satisfiability at the exact target threshold.
Boundary: This is not a parser/validator machine, emitter machine, RawRefinement, PolynomialReduction, construction-runtime or output-size bound, abstract locked-NAND threshold discharge, CNFSAT-in-P result, or P = NP.
Reviewed theorem pins: 11
Core source: commit fdd4e10c36155f079edc72f44fd59f0e8767dad6, tree 34313d90e30ff0940ce4624d6d590b0b65df7b7d, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-28-89.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 65
The proof now separates circuits with and without a solution
A circuit is a sequence of simple yes-or-no steps. Earlier work proved what happens when no successful input exists. Lean now also proves the other direction: when a successful input does exist, the enlarged circuit cannot shrink back to the established baseline size. Its smallest equivalent form must use at least one extra step, while the construction adds no more than four.
Together, these results give an exact yes-or-no comparison at the mathematical circuit level: the minimum size rises above the baseline exactly when the original circuit has a solution. The efficient encoded procedure needed to turn arbitrary inputs into these circuits is still missing, as are the remaining reduction, CNF-SAT in P, and P = NP. The 51% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Editorial progress estimate at publication: 51%.
Technical detailsShowHide⌄
Milestone:locked-nand-global-semantic-threshold
Classification: formalized
Verified scope: For every finite topologically ordered NAND circuit, one answer-independent full candidate instantiates all six semantic premises, has residual slack at most four, and crosses the exact source-derived minimum threshold exactly when the source circuit is satisfiable.
Boundary: This typed semantic theorem does not construct or compile the report's encoded polynomial-time SAT-to-locked-NAND builder, establish CNFSAT in P, prove NP-hardness transport, discharge the abstract locked-NAND threshold axiom, or prove P = NP.
Reviewed theorem pins: 8
Core source: commit 4cdfd0e3d263f473177bbef9e9b26d7756810bdf, tree f33a5857d25a510d1fc1f6db4e8221dd387bdade, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-28-88.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 64
The final check now stays off whenever no solution exists
A circuit is a sequence of simple yes-or-no steps. This project adds a final check that can turn on only when the original circuit has a successful input and all of the recorded intermediate work agrees. Lean now proves that if no successful input exists, that final check stays off for every possible filling of the workspace, including deliberately inconsistent ones.
Lean also proves that, in this no-solution case, the smallest equivalent implementation has exactly the established baseline size. This closes only the no-solution half of the comparison. The successful-solution separation argument, complete size threshold, uniform polynomial-time builder, CNF-SAT in P, and P = NP remain unproved. The 50% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: For every finite topologically ordered NAND circuit, unsatisfiability makes the full final coordinate identically false on the whole carrier and fixes the exhaustive reference minimum at B.
Boundary: This does not prove satisfiable FinalLockSeparation, instantiate the complete threshold package, establish the global locked-NAND threshold or residual-slack bound, or construct the uniform polynomial builder.
Reviewed theorem pins: 2
Core source: commit 764c4ccc3795a32b183c6ee4fa1e347720562483, tree 71b50f3bc11bad65e04372505aa747ba03356e92, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-27-87.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 63
The proof now shows every baseline output does a different job
The previous milestone assembled a baseline circuit with one exposed output for every gate. That head count alone did not show every gate was necessary: an output might have been fixed, might merely copy an input, or might duplicate another output. This milestone proves none of those shortcuts occurs, for every finite circuit in the family.
That makes the baseline's exact minimum size match its stated size and completes another required part of the later threshold argument. Two final-output laws and the uniform polynomial-time construction are still missing, so the locked-circuit threshold, CNF-SAT in P, and P = NP remain unproved. The 49% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Editorial progress estimate at publication: 49%.
Technical detailsShowHide⌄
Milestone:locked-nand-global-baseline-distinct
Classification: formalized
Verified scope: All exposed baseline outputs are nonconstant, nonprojections, pairwise semantically distinct, and have exact exhaustive reference minimum B for arbitrary finite topological NAND circuits.
Boundary: BaselineDistinct does not prove either whole-carrier final-output branch law, instantiate the complete threshold premise package, establish the locked-NAND threshold or global residual-slack bound, or construct the uniform polynomial bitstring builder.
Reviewed theorem pins: 5
Core source: commit aed2c360982d1e356b462b9e27d976b23a2305a4, tree eee584b56ab70409e756362a58adf1ccf562265b, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-27-86.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 62
The proof now assembles the two circuit families used in the next comparison
The previous milestone established a reliable way to represent and check the step-by-step behaviour of any finite circuit built from simple logic gates. This milestone uses that representation to assemble the two complete circuit families required by the next stage: a baseline whose number of inputs matches its number of gates, and a slightly larger version with four additional gates. It proves the exact size of each construction and that every original output is preserved.
The construction also avoids hidden fixed values inside the circuits and shows that changing the new final control input cannot alter any original output. This turns an abstract outline into a concrete family that works for circuits of any finite size. Important comparison and threshold arguments are still missing, as is the uniform polynomial-time procedure that would generate the construction from encoded input. The 48% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Editorial progress estimate at publication: 48%.
Technical detailsShowHide⌄
Milestone:locked-nand-global-candidate-assembly
Classification: formalized
Verified scope: Exact source-derived B/B baseline and B+4/B+1 extension for arbitrary finite topological NAND circuits.
Boundary: Candidate assembly alone does not prove global BaselineDistinct, either conditional final-output branch law, the locked-NAND threshold, residual slack at most four, or a uniform polynomial bitstring builder.
Reviewed theorem pins: 11
Core source: commit a8916280a02c3d2357f5b81917baa17926e51047, tree 73c43c480fe556651edd2fa3ccbd491fa810ec2f, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-26-85.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 61
The proof now gives every finite NAND circuit one checkable trace
A computer circuit can be pictured as a row of small logic gates. Each gate reads two earlier values and produces a new value. This milestone gives every finite circuit arranged in that order a fixed set of labelled spaces for its inputs, connections, intermediate results, and final check. It proves that filling those spaces consistently is exactly the same as evaluating the circuit gate by gate.
This is a rule for circuits of any finite size, not just another fixed-size example. It still does not build the complete locked circuit family, prove the required size threshold, supply the full polynomial-time construction, or prove P = NP. The 47% figure is a revisable estimate of known reconstruction work, not a probability that the claim is correct.
Verified scope: Exact X/T/O/R/L/z carrier separation and both trace-equivalence directions for arbitrary finite topological NAND circuits.
Boundary: Carrier/trace equivalence does not assemble the complete exposed candidates, prove cross-instance BaselineDistinct or final-output laws, construct the uniform polynomial builder, or establish the locked-NAND threshold.
Reviewed theorem pins: 8
Core source: commit f1ebb93c5683592eaa70e0b77ed1969a1def6180, tree 6fc22902a94f4a720ccb771ef5df30c22cae8bd2, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-25-84.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 60
The machine starts writing the following item’s number
The machine is building a long checklist one position at a time. In wider layouts it has already written the opening mark for the following item. At the next position, the smallest supported layout still has intentional empty spacing, so it moves past without writing. In wider layouts, it writes the first mark of that item’s number. In both cases, it stops at the exact following position.
Only this one position is handled. The machine does not write the remaining number marks or closing mark, finish the second block, or finish the full checklist. The 46% figure is a revisable planning estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete sixth padding-or-opening-unary-opportunity predecessor with the represented-width unary evaluator, the reviewed 93-rule finite optional-appender table, and the retained-coordinate unary evaluator through three total nine-symbol WorkChain bridges. The global table has exactly 6124 plus the thirty-two inherited/generated unary-evaluator rule counts. Every raw input follows exact predecessor, width-evaluator, width-one skip or wider-width first-unary-index-T appender, retained-coordinate, bridge, suffix, and combined traces. At tapeWidth one it consumes padding and emits no token; at every wider width it appends exactly the first unary-index T of the following literal. The output equals encodedFormula.take (2 * (FormulaWidth + 43 + if tapeWidth = 1 then 0 else 7)) and the retained coordinate is FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 14. Direct lookup and the specification cursor prove the following slot is padding at width one and the second unary-index T of the following literal at wider widths. The external compiled bound evaluates to BuilderSecondConstraintSixthPaddingOrOpeningUnaryOpportunityStep.rawTimeBound + 684 + 24 * n + 12 * FormulaWidth + 12 * width + 12 * widthRootPrefixLength + 6 * widthWorkSteps + 6 * targetWorkSteps. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, predecessor-unlaunched-endpoint, and one-step-short results are proved while component malformed-workspace behavior remains fail-closed. The measured audit covers all 66 new public declarations, fourteen reused optional-appender interfaces, and two strengthened schedule lemmas: 37 closures are empty, 12 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone consumes exactly one additional width-selected schedule opportunity after the second scheduled constraint following literal opening: padding with no emitted token at width one or the first unary-index T of the following literal at wider widths. It observes but does not consume the following padding opportunity at width one or second unary-index T at wider widths, does not complete the following literal or traverse the remainder of the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 655d767f486a8ef64ee841b24ba853c4e0414658, tree a177eac640ef51557208b131b313ec0ff1c703d7, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-25-83.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 59
The machine starts the following item when one exists
The machine is building a long checklist one position at a time. It has reached the position where another item would begin. In the smallest supported layout there is no item here, so it leaves the position blank. In wider layouts it writes the opening mark for the following item. In both cases it stops at the exact next position.
Only this one position is handled. The machine does not write the following item's number or closing mark, finish the second block, or finish the full checklist. The 45% figure is a revisable planning estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete fifth padding-or-terminator-opportunity predecessor with the represented-width unary evaluator, the reviewed 93-rule finite optional-appender table, and the retained-coordinate unary evaluator through three total nine-symbol WorkChain bridges. The global table has exactly 6004 plus the thirty inherited/generated unary-evaluator rule counts. Every raw input follows exact predecessor, width-evaluator, width-one skip or wider-width opening-T appender, retained-coordinate, bridge, suffix, and combined traces. At tapeWidth one it consumes padding and emits no token; at every wider width it appends exactly the opening positive T of the following literal. The output equals encodedFormula.take (2 * (FormulaWidth + 43 + if tapeWidth = 1 then 0 else 6)) and the retained coordinate is FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 13. Direct lookup and the specification cursor prove the following slot is padding at width one and the first unary-index T of the following literal at wider widths. The external compiled bound evaluates to BuilderSecondConstraintFifthPaddingOrTerminatorOpportunityStep.rawTimeBound + 672 + 24 * n + 12 * FormulaWidth + 12 * width + 12 * widthRootPrefixLength + 6 * widthWorkSteps + 6 * targetWorkSteps. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, predecessor-unlaunched-endpoint, and one-step-short results are proved while component malformed-workspace behavior remains fail-closed. The measured audit covers all 66 new public declarations, fourteen reused optional-appender interfaces, and two strengthened schedule lemmas: 37 closures are empty, 12 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone consumes exactly one additional width-selected schedule opportunity after the second scheduled constraint second literal: padding with no emitted token at width one or the opening positive T of the following literal at wider widths. It observes but does not consume the following padding opportunity at width one or first unary-index T at wider widths, does not complete the following literal or traverse the remainder of the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 59d89b6b07ae16e649cda19dfeb3c78b335397ea, tree f62c8553fc98e4cb0aba8174193264da027c1d55, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-24-82.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 58
The machine checks whether the next item ends here
The machine is building a long checklist one position at a time. It has now reached the next reserved position. In the smallest supported layout, there is no extra item here, so the position stays blank. In wider layouts, the machine writes the closing mark that finishes the next item. In both cases, it stops at the exact following position.
Only this one position is handled. The machine does not write the first mark of whatever comes next, finish the second block, or finish the full checklist. The 44% figure is a revisable planning estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete fourth padding-or-unary-opportunity predecessor with the represented-width unary evaluator, a new reviewed 93-rule finite optional-terminator table over the audited token-appender rules, and the retained-coordinate unary evaluator through three total nine-symbol WorkChain bridges. The global table has exactly 5884 plus the twenty-eight inherited/generated unary-evaluator rule counts. Every raw input follows exact predecessor, width-evaluator, width-one skip or wider-width F-appender, retained-coordinate, bridge, suffix, and combined traces. At tapeWidth one it consumes padding and emits no token; at every wider width it appends exactly the terminating F of the second literal. The output equals encodedFormula.take (2 * (FormulaWidth + 43 + if tapeWidth = 1 then 0 else 5)) and the retained coordinate is FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 12. Direct lookup and the specification cursor prove the following slot is padding at width one and the opening unary T of the following literal at wider widths. The external compiled bound evaluates to BuilderSecondConstraintFourthPaddingOrUnaryOpportunityStep.rawTimeBound + 660 + 24 * n + 12 * FormulaWidth + 12 * width + 12 * widthRootPrefixLength + 6 * widthWorkSteps + 6 * targetWorkSteps. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, predecessor-unlaunched-endpoint, and one-step-short results are proved while component malformed-workspace behavior remains fail-closed. The measured audit covers all 66 new public outer declarations, fourteen new optional-terminator interfaces, and two strengthened schedule lemmas: 37 closures are empty, 12 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone consumes exactly one additional width-selected schedule opportunity after the second scheduled constraint first literal: padding with no emitted token at width one or the terminating F of the second literal at wider widths. It observes but does not consume the following padding opportunity at width one or opening unary T at wider widths, does not complete the following literal or traverse the remainder of the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 650dbecaa067ff71b996d26d13315da9dd2cdcc9, tree 94cb12d3bddb453b9e78d9ea8bfa2583c39643a0, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-24-81.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 57
The machine checks a fourth reserved position
The machine is building a long checklist one position at a time. It has now reached a fourth reserved position after a completed item. In the smallest supported layout, that position is still intentional empty spacing, so the machine moves past it without writing. In wider layouts, it writes the fourth and final number mark of the next item. In both cases, it stops at the exact following position.
Only this one additional position is handled. The machine does not write the following closing mark, complete the next item, finish the second block, or finish the full checklist. The 43% figure is a revisable planning estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete third padding-or-unary-opportunity predecessor with the represented-width unary evaluator, the same reviewed 93-rule finite optional-appender table, and the retained-coordinate unary evaluator through three total nine-symbol WorkChain bridges. The global table has exactly 5764 plus the twenty-six inherited/generated unary-evaluator rule counts. Every raw input follows exact predecessor, width-evaluator, width-one skip or wider-width T-appender, retained-coordinate, bridge, suffix, and combined traces. At tapeWidth one it consumes padding and emits no token; at every wider width it appends exactly the fourth unary T of the second literal. The output equals encodedFormula.take (2 * (FormulaWidth + 43 + if tapeWidth = 1 then 0 else 4)) and the retained coordinate is FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 11. Direct lookup and the specification cursor prove the following slot is padding at width one and the terminating F at wider widths. The external compiled bound evaluates to BuilderSecondConstraintThirdPaddingOrUnaryOpportunityStep.rawTimeBound + 648 + 24 * n + 12 * FormulaWidth + 12 * width + 12 * widthRootPrefixLength + 6 * widthWorkSteps + 6 * targetWorkSteps. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, predecessor-unlaunched-endpoint, and one-step-short results are proved while component malformed-workspace behavior remains fail-closed. All 66 new public declarations, fourteen reused optional-appender interfaces, and two strengthened schedule lemmas are axiom-audited: 37 have empty closure, 12 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone consumes exactly one additional width-selected schedule opportunity after the second scheduled constraint first literal: padding with no emitted token at width one or the fourth unary T of the second literal at wider widths. It observes but does not consume the following padding opportunity at width one or terminating F at wider widths, does not complete the second literal or traverse the remainder of the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit fdc5e2f7e58e11dd0cd834378e05a9be0492573c, tree c13f132f69af662f9e867be611ae381050c36086, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-24-80.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 56
The machine checks a third reserved position
The machine is building a long checklist one position at a time. It has now reached a third reserved position after a completed item. In the smallest supported layout, that position is still intentional empty spacing, so the machine moves past it without writing. In wider layouts, it writes the third mark of the next numbered item. In both cases, it stops at the exact following position.
Only this one additional position is handled. The machine does not write the following mark, complete the next item, finish the second block, or finish the full checklist. The 42% figure is a revisable planning estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second padding-or-unary-opportunity predecessor with the represented-width unary evaluator, the same reviewed 93-rule finite optional-appender table, and the retained-coordinate unary evaluator through three total nine-symbol WorkChain bridges. The global table has exactly 5644 plus the twenty-four inherited/generated unary-evaluator rule counts. Every raw input follows exact predecessor, width-evaluator, width-one skip or wider-width T-appender, retained-coordinate, bridge, suffix, and combined traces. At tapeWidth one it consumes padding and emits no token; at every wider width it appends exactly the third unary T of the second literal. The output equals encodedFormula.take (2 * (FormulaWidth + 43 + if tapeWidth = 1 then 0 else 3)) and the retained coordinate is FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 10. Direct lookup and the specification cursor prove the following slot is again padding at width one and the fourth unary T at wider widths. The external compiled bound evaluates to BuilderSecondConstraintSecondPaddingOrUnaryOpportunityStep.rawTimeBound + 636 + 24 * n + 12 * FormulaWidth + 12 * width + 12 * widthRootPrefixLength + 6 * widthWorkSteps + 6 * targetWorkSteps. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, predecessor-unlaunched-endpoint, and one-step-short results are proved while component malformed-workspace behavior remains fail-closed. All 66 new public declarations, fourteen reused optional-appender interfaces, and two strengthened schedule lemmas are axiom-audited: 37 have empty closure, 12 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone consumes exactly one additional width-selected schedule opportunity after the second scheduled constraint first literal: padding with no emitted token at width one or the third unary T of the second literal at wider widths. It observes but does not consume the following padding opportunity at width one or fourth unary T at wider widths, does not complete the second literal or traverse the remainder of the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit cf0220e7e73b13b5b2639c3b6b0ec1b170090ecf, tree 371c1e78025328a752e1f146bddd7ad52e370f7a, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-24-79.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 55
The machine handles one more position in the next item
The machine is building a long checklist one position at a time. It had already handled the first reserved position after a completed item. At the next position, the smallest supported layout still needs intentional empty spacing, so the machine moves past it without writing. In wider layouts, it writes the second mark of the next numbered item. In both cases, it stops at the exact following position.
Only this one additional position is handled. The machine does not write the following mark, complete the next item, finish the second block, or finish the full checklist. The 41% figure is a revisable planning estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete first padding-or-unary-opportunity predecessor with the represented-width unary evaluator, the same reviewed 93-rule finite optional-appender table, and the retained-coordinate unary evaluator through three total nine-symbol WorkChain bridges. The global table has exactly 5524 plus the twenty-two inherited/generated unary-evaluator rule counts. Every raw input follows exact predecessor, width-evaluator, width-one skip or wider-width T-appender, retained-coordinate, bridge, suffix, and combined traces. At tapeWidth one it consumes padding and emits no token; at every wider width it appends exactly the second unary T of the second literal. The output equals encodedFormula.take (2 * (FormulaWidth + 43 + if tapeWidth = 1 then 0 else 2)) and the retained coordinate is FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 9. Direct lookup and the specification cursor prove the following slot is again padding at width one and the third unary T at wider widths. The external compiled bound evaluates to BuilderSecondConstraintPaddingOrUnaryOpportunityStep.rawTimeBound + 624 + 24 * n + 12 * FormulaWidth + 12 * width + 12 * widthRootPrefixLength + 6 * widthWorkSteps + 6 * targetWorkSteps. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, predecessor-unlaunched-endpoint, and one-step-short results are proved while component malformed-workspace behavior remains fail-closed. All 66 new public declarations, fourteen reused optional-appender interfaces, and two strengthened schedule lemmas are axiom-audited: 37 have empty closure, 12 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone consumes exactly one additional width-selected schedule opportunity after the second scheduled constraint first literal: padding with no emitted token at width one or the second unary T of the second literal at wider widths. It observes but does not consume the following padding opportunity at width one or third unary T at wider widths, does not complete the second literal or traverse the remainder of the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 9d2bff977cfc3ad5dbea9da60d46448276eea2cd, tree a48617d1fe7298677563b063d5a36184fb33d952, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-23-78.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 54
The machine handles the next position after its choice
The machine has finished one numbered item in a long checklist and has already chosen the mark that follows it. This milestone verifies what happens at the very next reserved position. In the smallest supported layout, that position is intentional empty spacing, so the machine moves past it without writing. In wider layouts, it writes the first mark of the next numbered item. In both cases, it finishes at the exact following position.
Only this one position is handled. The machine does not write the next mark, complete the next item, finish the second block, or finish the full checklist. The 40% figure is a revisable planning estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second-constraint first-literal successor-token predecessor with the represented-width unary evaluator, one 93-rule finite optional-appender table, and the retained-coordinate unary evaluator through three total nine-symbol WorkChain bridges. The global table has exactly 5404 plus the twenty inherited/generated unary-evaluator rule counts. Every raw input follows exact predecessor, width-evaluator, width-one skip or wider-width T-appender, retained-coordinate, bridge, suffix, and combined traces. At tapeWidth one it consumes padding and emits no token; at every wider width it appends exactly the first unary T of the second literal. The output equals encodedFormula.take (2 * (FormulaWidth + 43 + if tapeWidth = 1 then 0 else 1)) and the retained coordinate is FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 8. Direct lookup and the specification cursor prove the following slot is again padding at width one and the second unary T at wider widths. The external compiled bound evaluates to BuilderSecondConstraintFirstLiteralSuccessorTokenStep.rawTimeBound + 612 + 24 * n + 12 * FormulaWidth + 12 * width + 12 * widthRootPrefixLength + 6 * widthWorkSteps + 6 * targetWorkSteps. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, predecessor-unlaunched-endpoint, and one-step-short results are proved while component malformed-workspace behavior remains fail-closed. All 80 new public declarations plus two strengthened schedule lemmas are axiom-audited: 37 have empty closure, 12 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone consumes exactly one width-selected schedule opportunity after the second scheduled constraint first literal: padding with no emitted token at width one or the first unary T of the second literal at wider widths. It observes but does not consume the following padding opportunity at width one or second unary T at wider widths, does not complete the second literal or traverse the remainder of the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 5aba133715790bae354e584c0d8606c19bb3ab8b, tree 8f7140c0401973197017b988592256fb3ddeb704, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-23-77.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 53
The machine chooses what comes after the completed item
Imagine the machine has just finished one numbered item in its long checklist. The next mark depends on how wide the checklist is. In the smallest supported layout, it writes an end-of-line mark. In wider layouts, it writes the opening mark for the next item. This milestone verifies that it makes that choice, writes exactly one mark, and moves to the following position.
It does not write the next item's number, finish the second block, or finish the full checklist. The 39% figure is a revisable planning estimate of known reconstruction work, not a probability that the claim is correct. P = NP remains unproved.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second-constraint first-literal terminator with the represented-width unary evaluator, one 93-rule finite width branch that enters a single reused 59-rule token appender at either Finish or T, and the retained-coordinate unary evaluator through three total nine-symbol WorkChain bridges. The global table has exactly 5284 plus the eighteen inherited/generated unary-evaluator rule counts. Every raw input follows exact predecessor, width-evaluator, branch/appender, retained-coordinate, bridge, suffix, and combined traces; emits Finish exactly when tapeWidth is one and T at every wider width; preserves encodedFormula.take (2 * (FormulaWidth + 43)); and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 7. Direct lookup and the specification cursor prove the following opportunity is padding at width one and unary T at wider widths. The external compiled bound evaluates to BuilderSecondConstraintFirstLiteralTerminatorStep.rawTimeBound + 600 + 24 * n + 12 * FormulaWidth + 12 * width + 12 * widthRootPrefixLength + 6 * widthWorkSteps + 6 * targetWorkSteps. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, predecessor-unlaunched-endpoint, and one-step-short results are proved while component malformed-workspace behavior remains fail-closed. All 80 new public declarations plus two strengthened predecessor boundary lemmas are axiom-audited: 37 have empty closure, 12 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly one width-selected token after the terminating F of the second scheduled constraint's first literal: Finish at width one or positive T at wider widths. It observes but does not emit the following padding opportunity at width one or unary T at wider widths, does not emit the remainder of the second constraint or traverse that constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit a632bd845a69a7c442e1e6fcecb00981854b2f1c, tree 9e62eda65361d0714060f8eae9f917768d98d2c9, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-23-76.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 52
The machine closes the first item in its second checklist block
Imagine a machine writing a numbered item in a long checklist, one mark at a time. The marks saying how to use the item and which item it is were already in place. This milestone verifies that the machine adds the single closing mark that completes the first item in the second major block, then moves to the next required position.
Only that closing mark is added. In the smallest supported layout, the next position closes the line; in wider layouts, it begins another item. The machine identifies which case applies but writes neither next mark. It has not finished the second block or the full checklist, and this update does not prove that P equals NP.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second-constraint first-literal third-unary-unit step with the reused selected 59-rule F appender and 45-rule cursor advance through one outer total nine-symbol WorkChain bridge. The global table has exactly 5164 plus the sixteen inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits exactly the terminating F of the second scheduled constraint's first literal; preserves encodedFormula.take (2 * (FormulaWidth + 42)); and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 6. A constructive schedule case split proves the direct next schedule token is Finish when tapeWidth is one and the positive T beginning the next literal at wider widths. The external compiled bound evaluates to BuilderSecondConstraintFirstLiteralThirdUnaryUnitStep.rawTimeBound + 594 + 24 * n + 12 * FormulaWidth + 12 * cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, both unlaunched-endpoint, and one-step-short results are proved. All 48 new public declarations plus eight reviewed reused false-token/cursor and dead-state interfaces are axiom-audited: 14 have empty closure, 11 use only propext, and 31 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly one token: the terminating F of the second scheduled constraint's first literal. It observes but does not emit the following Finish in the width-one case or the following positive T in wider cases, does not emit the remainder of the second constraint or traverse that constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 2869924b3f5b7f4cea1b27d40ccebb91ee36a5ec, tree 91f28c0732fb700be15512313da961b2bcfecaf0, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-23-75.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 51
The machine finishes writing the first item's number
Imagine a machine writing a numbered item in a long checklist, one mark at a time. Two of the three marks needed for the first item's number in the second major block were already in place. This milestone verifies that it writes the third and final number mark, then moves to the closing mark for that item.
Only that final number mark is added. The machine has not written the closing mark, completed the item, finished the second block, or finished the full checklist. This update does not prove that P equals NP.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second-constraint first-literal second-unary-unit step with the reused selected 59-rule T appender and 45-rule cursor advance through one outer total nine-symbol WorkChain bridge. The global table has exactly 5042 plus the sixteen inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits exactly the third and final unary T of the second scheduled constraint's first variable index; preserves encodedFormula.take (2 * (FormulaWidth + 41)); and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 5. A constructive schedule case split proves the selected variable index is exactly three in both the width-one head-variable and wider position-one blank-symbol branches, so the direct next schedule token is the terminating F. The external compiled bound evaluates to BuilderSecondConstraintFirstLiteralSecondUnaryUnitStep.rawTimeBound + 582 + 24 * n + 12 * FormulaWidth + 12 * cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, both unlaunched-endpoint, and one-step-short results are proved. All 48 new public declarations plus eight reviewed reused true-token/cursor interfaces are axiom-audited: 14 have empty closure, 11 use only propext, and 31 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly one token: the third and final unary T of the second scheduled constraint's first variable index. It observes but does not emit the following terminating F, does not complete that literal or traverse the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 170775d279865370c239919326f1f336cf254b70, tree 4e6b53721a57038737be8681146ec7f07d51d888, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-23-74.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 50
The machine writes the next mark of the first item's number
Imagine a machine writing a long checklist, one mark at a time. It had already written the first mark of the first item's number in the second major block. This milestone verifies that it now writes the second mark and moves to the exact place for the third mark.
Only that one additional number mark is added. The machine has not written the third mark, completed the item, finished the second block, or finished the full checklist. This update does not prove that P equals NP.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second-constraint first-literal first-unary-unit step with the reused selected 59-rule T appender and 45-rule cursor advance through one outer total nine-symbol WorkChain bridge. The global table has exactly 4920 plus the sixteen inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits exactly the second unary T of the second scheduled constraint's first variable index; preserves encodedFormula.take (2 * (FormulaWidth + 40)); and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 4. A constructive schedule proof establishes that the index is at least three, so the direct next schedule token is the third unary T. The external compiled bound evaluates to BuilderSecondConstraintFirstLiteralFirstUnaryUnitStep.rawTimeBound + 570 + 24 * n + 12 * FormulaWidth + 12 * cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, both unlaunched-endpoint, and one-step-short results are proved. All 48 new public declarations plus eight reviewed reused true-token/cursor interfaces are axiom-audited: 14 have empty closure, 11 use only propext, and 31 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly one token: the second unary T of the second scheduled constraint's first variable index. It observes but does not emit the following third unary T, does not complete that literal or traverse the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 2079ea0df337d413c2402a3820087aea4aca9efa, tree 60b3b6663d381c5e95029cc20c66ab31928e784c, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-23-73.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 49
The machine starts writing the first item's number
Imagine a machine writing a long checklist, one mark at a time. It had already placed the divider for the second major block and marked that its first item should be used as written. This milestone verifies that it now writes the first mark of that item's number and moves to the next mark.
Only that one number mark is added. The machine has not written the next mark, completed the item, finished the second block, or finished the full checklist. This update does not prove that P equals NP.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second-constraint first-literal sign step with the reused selected 59-rule T appender and 45-rule cursor advance through one outer total nine-symbol WorkChain bridge. The global table has exactly 4798 plus the sixteen inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits exactly the first unary T of the second scheduled constraint's first variable index; preserves encodedFormula.take (2 * (FormulaWidth + 39)); and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 3. A constructive schedule proof establishes that the index is at least three, so the direct next schedule token is the second unary T. The external compiled bound evaluates to BuilderSecondConstraintFirstLiteralSignStep.rawTimeBound + 558 + 24 * n + 12 * FormulaWidth + 12 * cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, both unlaunched-endpoint, and one-step-short results are proved. All 48 new public declarations plus eight reviewed reused true-token/cursor interfaces are axiom-audited: 14 have empty closure, 11 use only propext, and 31 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly one token: the first unary T of the second scheduled constraint's first variable index. It observes but does not emit the following second unary T, does not complete that literal or traverse the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 6b0b51ad3fda5bed69ca765b485b166746da8cfd, tree 0084a05b3daebd42b09ad5afac7e6bf210ba2c1b, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-23-72.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 48
The machine now starts the first item in its second checklist block
Imagine a machine writing a long checklist, one mark at a time. It had already placed the divider that opens the second major block. This milestone verifies that it now writes the single mark saying the first item in that block should be used as written, rather than as its opposite, then moves to the exact place where the item's number begins.
Only that one mark is added. The machine has not written the item's number, completed the item, finished the second block, or finished the full checklist. This update does not prove that P equals NP.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second-constraint separator step with the reused selected 59-rule T appender and 45-rule cursor advance through one outer total nine-symbol WorkChain bridge. The global table has exactly 4676 plus the sixteen inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits exactly the positive sign beginning the second scheduled constraint's first literal; preserves encodedFormula.take (2 * (FormulaWidth + 38)); and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 2, whose direct next schedule token is the first unary T of a nonzero variable index. The external compiled bound evaluates to BuilderSecondConstraintSeparatorStep.rawTimeBound + 546 + 24 * n + 12 * FormulaWidth + 12 * cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, both unlaunched-endpoint, and one-step-short results are proved. All 48 new public declarations plus eight reviewed reused true-token/cursor interfaces are axiom-audited: 14 have empty closure, 11 use only propext, and 31 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly one token: the fixed positive T sign that begins the second scheduled constraint's first literal. It observes but does not emit the following unary T, does not complete that literal or traverse the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 3b4bd1a42175a4a07606f5d5690b2ca8af83940e, tree a5ae0d32a6f55805841ac8d3c3747e571bd16866, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-22-71.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 47
The builder now opens the second major checklist block
Imagine this project as a machine that writes a very long checklist of simple logical conditions. The first major checklist block was already complete. This milestone verifies that the machine writes one divider marking the start of the second block, then moves to the exact position where the next item belongs.
This step adds only that divider. It does not write the next checklist item, finish the second block, complete the full checklist-building machine, or prove that P equals NP.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete first-constraint padding run with the reused selected 59-rule Sep appender and 45-rule cursor advance through one outer total nine-symbol WorkChain bridge. The global table has exactly 4554 plus the sixteen inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits exactly the Sep beginning the second scheduled constraint; preserves encodedFormula.take (2 * (FormulaWidth + 37)); and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 1, whose direct next schedule token is T. The external compiled bound evaluates to BuilderFirstConstraintPaddingRun.rawTimeBound + 534 + 24 * n + 12 * FormulaWidth + 12 * cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, both unlaunched-endpoint, and one-step-short results are proved. All 48 new public declarations plus eight reviewed reused separator/cursor interfaces are axiom-audited: 14 have empty closure, 11 use only propext, and 31 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly one token: the fixed Sep that starts the second scheduled constraint. It observes but does not emit the following T, does not emit the first literal or traverse the second constraint, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 8ac394c0fb19fbaabec883a498a1ad35d730b77f, tree 9dacf36b058e09470f4790536d37b0480916df8c, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-22-70.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 46
The builder now reaches the second major checklist block
This project is checking a step-by-step method that turns a computer task into a long checklist of simple yes-or-no conditions. Each major block has a fixed amount of reserved space. This update confirms that the builder can cross all the unused space left in the first major block without changing the checklist, then stop at the exact marker where the second block begins.
Think of completing the first section of a very large fixed-size form and moving across every unused box until you reach the next section divider. The divider is seen but not printed by this step, and the next item is not started. The full builder is still incomplete, and this update does not prove that P equals NP.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the fifth-clause padding predecessor with two structurally generated unary evaluators, the reused 25-rule PaddingCountdown machine, and three total nine-symbol WorkChain bridges. Its table has exactly 4432 plus sixteen inherited/generated unary-evaluator rule counts. For every raw bitstring it traverses exactly (FormulaVariableSlotBound - 2) * (FormulaVariableSlotBound + 2) * FormulaTokensPerClause = (FormulaClauseSlotsPerConstraint - 5) * FormulaTokensPerClause remaining empty token opportunities of the first scheduled constraint without emitting a token, preserves encodedFormula.take (2 * (FormulaWidth + 36)), and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause. Direct schedule lookup and the specification cursor prove that every traversed opportunity is padding and the endpoint is the Sep beginning the second scheduled constraint. The external compiled bound is BuilderFifthClausePaddingRun.rawTimeBound + 18 + six times the count-evaluator work, countdown bound, and target-evaluator work. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-countdown, unlaunched-predecessor, and one-step-short results are proved. All 65 new public declarations and three reused countdown interfaces are axiom-audited: 26 have empty closure, 9 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone traverses only the remaining empty clause rectangles of the first scheduled constraint and retains the Sep beginning the second scheduled constraint. It observes but does not emit that separator, does not emit the next constraint's first literal, implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, emit the remaining formula body, construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 39
Core source: commit 5a2cf2b0bea9568d7361336fa5f8f197246a2f9c, tree 2871fea51d6f6fc0d150a71d67e5eb99458ba26e, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-22-69.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 45
The builder now crosses a whole intentionally empty section
This project is building, and checking, a step-by-step method that turns a computer task into a long list of simple yes-or-no checks. Some places in that list are deliberately left empty so every section has a predictable size. This update confirms that the builder can cross one whole empty section without changing the list and stop at the next exact boundary.
Think of a form with fixed-size boxes: the machine can now move across one unused box and arrive at the next unused box without writing anything. This is a small construction milestone. It does not reach the next meaningful check, finish the builder, or prove that P equals NP.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the fourth-clause padding predecessor with two structurally generated unary evaluators, the reused 25-rule PaddingCountdown machine, and three total nine-symbol WorkChain bridges. Its table has exactly 4380 plus fourteen inherited/generated unary-evaluator rule counts. For every raw bitstring it traverses exactly FormulaTokensPerClause padding opportunities in the intentionally empty fifth fixed-width clause rectangle without emitting a token, preserves encodedFormula.take (2 * (FormulaWidth + 36)), and retains coordinate FormulaVariableSlotBound + 1 + 5 * FormulaTokensPerClause. Direct schedule lookup and the specification cursor prove that every traversed fifth-slot opportunity and the first opportunity in the intentionally empty sixth slot are padding. The external compiled bound is BuilderFourthClausePaddingRun.rawTimeBound + 18 + six times the count-evaluator work, countdown bound, and target-evaluator work. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-countdown, unlaunched-predecessor, and one-step-short results are proved. All 65 new public declarations and three reused countdown interfaces are axiom-audited: 28 have empty closure, 9 use only propext, and 31 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone traverses only the intentionally empty fifth clause rectangle and retains the first opportunity in the intentionally empty sixth clause rectangle. It does not traverse that sixth rectangle, reach the next constraint, emit another token, implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, emit the remaining formula body, construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 39
Core source: commit ad98889b806c4726e3d61c1ab58adf589782a971, tree 87dc990e9d04ec050c93260d5d78aea5a5853ef8, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-22-68.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 44
The builder now clears the unused space after section four
To check a computer program with mathematics, this project turns the program and its input into a long checklist of yes-or-no conditions. The fourth checklist section was already complete. This milestone verifies that the builder can move across every blank position reserved after it without writing anything, stop at the exact boundary of the next reserved block, and fail safely if its workspace is damaged.
Think of a document template with fixed-size boxes: the builder has crossed the unused part of the fourth box and landed at the next box, which is also intentionally blank. It has not started the next meaningful checklist section, finished the full builder, or established the project’s P-versus-NP claim.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete fourth-clause prefix with two structurally generated unary evaluators, the reused 25-rule PaddingCountdown machine, and three total nine-symbol WorkChain bridges. Its table has exactly 4328 plus twelve inherited/generated unary-evaluator rule counts. For every raw bitstring it traverses exactly FormulaTokensPerClause - 9 padding opportunities without emitting a token, preserves encodedFormula.take (2 * (FormulaWidth + 36)), and retains coordinate FormulaVariableSlotBound + 1 + 4 * FormulaTokensPerClause. Direct schedule lookup and the specification cursor both prove that this first opportunity in the intentionally empty fifth fixed-width clause slot is padding. The external compiled bound is BuilderFourthClausePrefix.rawTimeBound + 18 + six times the count-evaluator work, countdown bound, and target-evaluator work. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-countdown, unlaunched-predecessor, and one-step-short results are proved. All 65 new public declarations and three reused countdown interfaces are axiom-audited: 26 have empty closure, 9 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone traverses only the remaining padding in clause four and retains the first opportunity in the intentionally empty fifth clause rectangle. It does not traverse that empty rectangle, reach the next constraint, emit another token, implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, emit the remaining formula body, construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 39
Core source: commit 5377b99658a756f60a8b36d19896be579761d8cd, tree 8218321ed58d3e617a472db560c9c0bfc6dd111c, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-21-67.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 43
The fourth checklist section is now complete
To check a computer program with mathematics, this project turns the program and its input into a long checklist of yes-or-no conditions. This milestone verifies that the checklist builder can add the closing marker to the fourth section, move to the first unused space after it, and stop safely if its workspace is damaged.
Think of a document generator: the fourth section now has its heading, both required lines, and its closing mark. The larger document is still far from finished. This update does not complete the full checklist builder or establish the project’s P-versus-NP claim.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the fourth-clause second-literal prefix with a selected 59-rule Finish appender, one existing 45-rule cursor advance, and two total nine-symbol WorkChain bridges. The selected suffix has exactly 113 rules and the global table has exactly 4276 plus the ten inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits the Finish that completes clause four; preserves encodedFormula.take (2 * (FormulaWidth + 36)); and retains coordinate FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause + 9, whose direct next schedule token is padding. The external compiled bound evaluates to BuilderFourthClauseSecondLiteralPrefix.rawTimeBound + 618 + 24 * n + 12 * FormulaWidth + 12 * BuilderFourthClauseSeparatorStep.cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, both unlaunched-endpoint, and one-step-short results are proved. All 55 new public declarations and two cursor dead-state facts are axiom-audited: 14 have empty closure, 10 use only propext, and 33 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly the fixed Finish terminator that completes clause four and advances to its first padding coordinate. It does not traverse clause-four padding, implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, emit the remaining formula body, construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 41
Core source: commit c9f4b9b684b18b5fed4a4256133bcfdb83f3ad75, tree e69c76ac4a05c7895cde0ba70d6e1af22e5b7512, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-21-66.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 42
The fourth section now contains its second complete item
To check a computer program with mathematics, this project turns the program and its input into a long checklist of yes-or-no conditions. This milestone verifies that the checklist builder can add the second complete item in the fourth section, move to the exact place where the section-ending marker belongs, and fail safely if its workspace is damaged.
Think of a document generator: the fourth section now has two checked lines, but its closing marker has not yet been written. This is one small verified construction step. The fourth section and the full checklist are still unfinished, and the project’s much larger claim about P versus NP is not established.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete fourth-clause first-literal prefix with the reused 479-rule F/T/T/F appender/cursor suffix through one outer total nine-symbol WorkChain bridge. The global table has exactly 4154 plus the ten inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits the complete second negative literal on variable two in clause four; preserves encodedFormula.take (2 * (FormulaWidth + 35)); and retains coordinate FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause + 8, whose direct next schedule token is Finish. The external compiled bound evaluates to BuilderFourthClauseFirstLiteralPrefix.rawTimeBound + 2232 + 96 * n + 48 * FormulaWidth + 48 * BuilderFourthClauseSeparatorStep.cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, all eight unlaunched-endpoint, and one-step-short results are proved. All 124 new public declarations, 21 reviewed reused suffix interfaces, and two cursor dead-state facts are axiom-audited: 46 have empty closure, 32 use only propext, and 69 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly the fixed second negative literal on variable two in clause four. It observes but does not emit the following Finish, does not complete clause four, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 92
Core source: commit 3a56b27add47f7991b670e6e0fb9bb302d78cd04, tree b17cdd6861c91234de106474b7e5fa03277cb37f, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-21-65.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 41
The fourth section now contains its first complete item
To check a computer program with mathematics, this project turns the program and its input into a long checklist of yes-or-no conditions. This milestone verifies that the checklist builder can place the first complete item in the fourth section, stop exactly where the next item should begin, and fail safely if its workspace is damaged.
Think of a document generator: the fourth section heading was already in place, and this update checks the first full line beneath it. This is one small verified construction step. The fourth section and the full checklist are still unfinished, and the project’s much larger claim about P versus NP is not established.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete fourth-clause separator prefix with the reused 357-rule F/T/F appender/cursor suffix through one outer total nine-symbol WorkChain bridge. The global table has exactly 3666 plus the ten inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits the complete first negative literal on variable one in clause four; preserves encodedFormula.take (2 * (FormulaWidth + 31)); and retains coordinate FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause + 4, whose direct next schedule token is F. The external compiled bound evaluates to BuilderFourthClauseSeparatorStep.rawTimeBound + 1422 + 72 * n + 36 * FormulaWidth + 36 * cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, all six unlaunched-endpoint, and one-step-short results are proved. All 97 new public declarations, 16 reviewed reused suffix interfaces, and two cursor dead-state facts are axiom-audited: 33 have empty closure, 25 use only propext, and 57 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly the fixed first negative literal on variable one in clause four. It observes but does not emit the following second-literal F, does not complete clause four, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 75
Core source: commit 3112ca90d74d58116dc53ea5300082d0caa63c0e, tree 00affbe8d76a9c28b3d6aa98384d43e23aacd71f, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-21-64.
Site release and live deployment identity are verified separately by the release seal and deployment provenance record.
These coordinates and hashes establish artefact identity only; they do not establish theorem correctness.
· earned milestone 40
The generated checklist now reaches its fourth section
This project turns a computer program and its input into a long checklist of logical conditions. The work is being verified one small construction step at a time. This milestone confirms that the builder can add the marker that starts the fourth section of that checklist and then move to the correct place for the next symbol.
In everyday terms, it is like checking that a document generator placed the next section break in exactly the right spot. It is useful progress, but it does not complete the fourth section, finish the full generator, or establish the project’s overall mathematical claim.
Verified scope: For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete third-clause padding run with the reused selected 59-rule Sep appender and 45-rule cursor advance through one outer total nine-symbol WorkChain bridge. The global table has exactly 3300 plus the ten inherited/generated unary-evaluator rule counts. Every raw input follows exact prefix, appender, cursor, bridge, suffix, and combined traces; emits exactly the fourth-clause Sep; preserves encodedFormula.take (2 * (FormulaWidth + 28)); and retains coordinate FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause + 1, whose direct next schedule token is F. The external compiled bound evaluates to BuilderThirdClausePaddingRun.rawTimeBound + 426 + 24 * n + 12 * FormulaWidth + 12 * cursorWord.length. Compiled exact, bounded, blank-equivalent, accepting, non-timeout, malformed-workspace, both unlaunched-endpoint, and one-step-short results are proved. All 48 new public declarations plus eight reviewed reused separator/cursor interfaces are axiom-audited: 14 have empty closure, 11 use only propext, and 31 use only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This milestone emits exactly one token: the fixed Sep that starts clause four. It observes but does not emit the following F, does not complete clause four, does not implement a general dynamic formula cursor or raw decoder for arbitrary schedule coordinates, does not emit the remaining formula body, and does not construct a complete formula builder or FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNFSAT NP-hardness or NP-completeness, establish CNFSAT in P, or prove P = NP.
Reviewed theorem pins: 40
Core source: commit 522c8da0f4add7b310659dd28c3dd3bd492d5337, tree 43ab837054ffd8dfb3d2bf34fa8458779c4ee4b0, status PNP-FORMAL-RECONSTRUCTION-STATUS-2026-07-20-63.
