One hundred and nine scoped milestones are earned. The newest result embeds the generated balanced PkgC cancellation ledger into an arbitrary explicit ambient BN4 ledger by an exact proof-bearing multiset decomposition. Duplicate multiplicities and per-key positive and negative mass decompose exactly, leaving the ambient signed mass and executable residual contribution equal to an explicit remainder. Candidate-derived kernels retain canonical request atoms, and complete bindings with no computed bridge imply V54 singletonization. The ambient ledger, typed restorer, exact certificate or serialization, and successful kernel remain explicit inputs. Full PkgC route integration and silence, complete decreasing global routing, Package E, BCELReady, global ZeroSlack, polynomial PCCMin, five formal blockers, four project axioms, and the final theorem remain unresolved.
These cards are orientation. The compiled inventory and exact theorem records remain the technical authority below.
Scoped Lean results cover the earlier concrete and terminal chain plus PkgC typed restoration, same-key cancellation, and an exact ambient-BN4-ledger embedding with duplicate-preserving mass decomposition, explicit remainders, candidate-derived canonical-atom retention, and a fail-closed singletonization consequence.
The manuscript route still needs the ambient BN4 ledger, typed restorer, exact certificate, and successful candidate kernel derived rather than supplied; the BN5 payload and shadow universe derived from the four-corner bases; matching and cancellation connected to the complete global route system; full PkgC route silence; derived BN6 and Packet selector-realizer data; strict rank decrease and route completeness; Package E; manuscript-wide SaturatePositive and BCELReady; ZeroSlack; PCCMin exactness and polynomial runtime; SAT completeness transport; and the remaining Cook-Levin builder.
A CNF-SAT polynomial-time decider, global ZeroSlack and PCCMin, polynomial runtime and certificate bounds, a discharged root-theorem axiom boundary, and an eligible P = NP root theorem. The legacy abstract string-handle bridge remains quarantined and publication-ineligible.
status = "formal-reconstruction-in-progress" mathematicalTheoremEstablished = false publicTheoremEmissionAllowed = false publicTheoremStatement = null rootLeanTheoremPresent = false projectSpecificAxiomsRemaining = true leanLockedNANDCarrierLayoutFormalized = true leanLockedNANDCarrierTraceAxiomAuditPassed = true leanLockedNANDCarrierTraceAuditedDeclarationCount = 71 leanLockedNANDGlobalCandidateAssemblyFormalized = true leanLockedNANDGlobalCandidateAxiomAuditPassed = true leanLockedNANDGlobalCandidateAuditedDeclarationCount = 71 leanLockedNANDGlobalBaselineDistinctFormalized = true leanLockedNANDGlobalBaselineDistinctAxiomAuditPassed = true leanLockedNANDGlobalBaselineDistinctAuditedDeclarationCount = 5 leanLockedNANDUnsatisfiableFinalZeroFormalized = true leanLockedNANDUnsatisfiableFinalZeroAxiomAuditPassed = true leanLockedNANDUnsatisfiableFinalZeroAuditedDeclarationCount = 2 leanLockedNANDGlobalSemanticThresholdFormalized = true leanLockedNANDGlobalSemanticThresholdAxiomAuditPassed = true leanLockedNANDGlobalSemanticThresholdAuditedDeclarationCount = 8 leanConcreteLockedNANDCanonicalEncodingFormalized = true leanConcreteLockedNANDCompleteCandidateCodecFormalized = true leanConcreteLockedNANDEncodedSemanticReductionFormalized = true leanConcreteLockedNANDEncodedSemanticReductionAxiomAuditPassed = true leanConcreteLockedNANDEncodedSemanticReductionAuditedDeclarationCount = 48 leanConcreteLockedNANDParserMachineFormalized = true leanConcreteLockedNANDParserAxiomAuditPassed = true leanConcreteLockedNANDParserAuditedDeclarationCount = 380 leanConcreteLockedNANDParserAxiomAuditSplit = 247 empty / 58 propext / 75 propext+Quot.sound leanConcreteLockedNANDParserMachineShape = 228 states / 2052 rules / 9 symbols leanConcreteLockedNANDParserAllInputExactFormalized = true leanConcreteLockedNANDParserExactOutputFormalized = true leanConcreteLockedNANDParserCompiledNonTimeoutFormalized = true leanConcreteLockedNANDParserPolynomialTimeMachineFormalized = true leanConcreteLockedNANDParserPolynomialTimeFunctionFormalized = true leanConcreteLockedNANDParserRawRefinementFormalized = true leanConcreteLockedNANDParserWorkBound = 4096 * (n + 1)^3 leanConcreteLockedNANDParserCompiledRawTimeBound = 6 * 4096 * (n + 1)^3 leanConcreteLockedNANDEmitterMachineFormalized = true leanConcreteLockedNANDEmitterAxiomAuditPassed = true leanConcreteLockedNANDEmitterAuditedDeclarationCount = 3295 leanConcreteLockedNANDEmitterAxiomAuditSplit = 2224 empty / 429 propext / 642 propext+Quot.sound leanConcreteLockedNANDEmitterMachineShape = 1387921 rules / 9 symbols leanConcreteLockedNANDEmitterAllInputExactFormalized = true leanConcreteLockedNANDEmitterExactTargetBytesFormalized = true leanConcreteLockedNANDEmitterCompiledNonTimeoutFormalized = true leanConcreteLockedNANDEmitterPolynomialTimeMachineFormalized = true leanConcreteLockedNANDEmitterPolynomialTimeFunctionFormalized = true leanConcreteLockedNANDEmitterRawRefinementFormalized = true leanConcreteLockedNANDEmitterStrictParserCompositionFormalized = true leanConcreteLockedNANDEmitterOutputSizeBoundFormalized = true leanConcreteLockedNANDPolynomialReductionFormalized = true leanConcreteCNFToNANDSemanticCompilerFormalized = true leanConcreteCNFToNANDSemanticCompilerAxiomAuditPassed = true leanConcreteCNFToNANDSemanticCompilerAuditedDeclarationCount = 68 leanConcreteCNFToNANDExactSemanticsFormalized = true leanConcreteCNFToNANDExactGateCountFormalized = true leanConcreteCNFToNANDPolynomialOutputSizeBoundFormalized = true leanConcreteCNFToNANDAllBitstringFailClosedFormalized = true leanConcreteCNFToNANDLockedThresholdCompositionFormalized = true leanConcreteCNFToNANDFiniteMachineFormalized = true leanConcreteCNFToNANDPolynomialTimeFunctionFormalized = true leanConcreteCNFToNANDPolynomialReductionFormalized = true leanConcreteCNFToNANDPolynomialReductionAxiomAuditPassed = true leanConcreteCNFToNANDPolynomialReductionAuditedDeclarationCount = 1316 leanConcreteCNFToNANDAllInputExactFormalized = true leanConcreteCNFToNANDExactMachineOutputFormalized = true leanConcreteCNFToNANDCompiledNonTimeoutFormalized = true leanConcreteCNFToNANDRawRefinementFormalized = true leanConcreteCNFToNANDDirectReductionFormalized = true leanConcreteCNFToNANDLockedReductionCompositionFormalized = true leanResidualGainChainVerifierFormalized = true leanResidualGainChainAxiomAuditPassed = true leanResidualGainChainSemanticInvariantFormalized = true leanResidualGainChainSlackIterationBoundFormalized = true leanLockedNANDGainIterationsAtMostFourFormalized = true leanResidualGainChainPolynomialRuntimeFormalized = false leanResidualGainStoppingSpecificationFormalized = true leanResidualGainStoppingAxiomAuditPassed = true leanResidualGainZeroIffGlobalNoStrictGainFormalized = true leanResidualGainSemanticMinimumIffGlobalNoStrictGainFormalized = true leanResidualGainChainGlobalStoppingConsequenceFormalized = true leanResidualTerminalFullBridgeFormalized = true leanResidualTerminalFullBridgeAxiomAuditPassed = true leanResidualTerminalizationExactFormalized = true leanResidualTerminalFullMinimumSpecificationFormalized = true leanResidualTerminalMuBridgeFormalized = true leanResidualWholeSpanPositiveWitnessIffFormalized = true leanResidualWholeSpanStrictDescentFormalized = true leanResidualWholeSpanZeroAbsenceIffFormalized = true leanResidualTerminalQuotientCarrierFormalized = true leanResidualTerminalModeFirewallFormalized = true leanResidualTerminalModeFirewallAxiomAuditPassed = true leanResidualTerminalProfileProjectionExactFormalized = true leanResidualTerminalCheckedFullLiftFormalized = true leanResidualTerminalQuotientEqualityNotConstructiveFormalized = true leanResidualTerminalObligationDischargePreservedFormalized = true leanResidualProjectionTransferFormalized = true leanResidualProjectionTransferAxiomAuditPassed = true leanResidualProjectionTransferSignedDeltasFormalized = true leanResidualProjectionTransferIdentityFormalized = true leanResidualProjectionTransferConstantCutFormalized = true leanResidualTerminalProperSupportFormalized = true leanResidualTerminalProperSupportSearchCompleteFormalized = true leanResidualTerminalProperSupportExactLocalGainFormalized = true leanResidualTerminalProperSupportAxiomAuditPassed = true leanResidualTerminalProperSupportScope = "all-finite-direct-wire-candidates-explicit-terminal-dependency-systems-and-canonical-primitive-record-seeds-with-exhaustive-reference-minimum-local-gain" leanResidualTerminalSaturationFormalized = true leanResidualTerminalSaturationAxiomAuditPassed = true leanResidualTerminalPrimitiveUniverseFormalized = true leanResidualTerminalSaturationExtensiveFormalized = true leanResidualTerminalSaturationLeastFormalized = true leanResidualTerminalSaturationMonotoneFormalized = true leanResidualTerminalSaturationIdempotentFormalized = true leanResidualTerminalExecutableSaturationFormalized = true leanResidualTerminalPhysicalSupportCompletionFormalized = true leanResidualTerminalPhysicalBoundaryFormalized = true leanResidualTerminalPhysicalInterfaceFormalized = true leanResidualTerminalPhysicalCompatibilityFormalized = true leanResidualTerminalPhysicalSupportCompletionAxiomAuditPassed = true leanResidualTerminalSupportExtractionFormalized = true leanResidualTerminalOpenSemanticsFormalized = true leanResidualTerminalInducedRecoveryFormalized = true leanResidualTerminalSupportExtractionAxiomAuditPassed = true leanResidualTerminalSupportExtractionScope = "all-finite-direct-wire-candidates-terminal-record-lists-boundary-valuations-and-interface-coordinates" leanResidualTerminalProperSupportFormalized = true leanResidualTerminalProperSupportSearchCompleteFormalized = true leanResidualTerminalProperSupportExactLocalGainFormalized = true leanResidualTerminalProperSupportAxiomAuditPassed = true leanResidualTerminalSupportSquareClosureFormalized = true leanResidualTerminalSupportSquareMeetJoinExactFormalized = true leanResidualTerminalSupportSquarePhysicalCompatibilityFormalized = true leanResidualTerminalSupportSquareSemanticExtractionFormalized = true leanResidualTerminalSupportSquareClosureAxiomAuditPassed = true leanResidualTerminalSupportCompletionFormalized = true leanResidualTerminalGovernedSupportCompletionFormalized = true leanResidualTerminalGovernedProfilePartitionFormalized = true leanResidualTerminalGovernedSupportCompletionAxiomAuditPassed = true leanResidualTerminalFrontierPushoutFormalized = true leanResidualTerminalFrontierBoundaryGlueExactFormalized = true leanResidualTerminalFrontierInterfaceGlueExactFormalized = true leanResidualTerminalFrontierProfileGlueExactFormalized = true leanResidualTerminalFrontierInternalizationFormalized = true leanResidualTerminalFrontierPushoutAxiomAuditPassed = true leanResidualTerminalProjectionSquareFormalized = true leanResidualTerminalProjectionPhysicalInvariantFormalized = true leanResidualTerminalProjectionProfileExactFormalized = true leanResidualTerminalProjectionMeetJoinCommuteFormalized = true leanResidualTerminalProjectionPushoutCommuteFormalized = true leanResidualTerminalProjectionSquareAxiomAuditPassed = true leanResidualTerminalProjectionSquareScope = "all-finite-direct-wire-candidates-explicit-terminal-dependency-systems-computed-saturated-support-squares-and-forgetful-terminal-projections" leanResidualTerminalSideTightMinimumArithmeticFormalized = true leanResidualTerminalSideTightSignedSlackIdentityFormalized = true leanResidualTerminalSideTightFailClosedGateFormalized = true leanResidualTerminalSideTightCanonicalFullBasisFormalized = true leanResidualTerminalSideTightCanonicalQuotientBasisFormalized = true leanResidualTerminalSideTightMinimumAxiomAuditPassed = true leanResidualTerminalSideTightMinimumScope = "all-finite-terminal-projection-four-corner-families-and-independently-attained-full-and-quotient-minimum-bases" leanResidualTerminalFourCornerCarrierTransportFormalized = true leanResidualTerminalFourCornerCarrierExactEndpointsFormalized = true leanResidualTerminalFourCornerCarrierInjectiveCoordinatesFormalized = true leanResidualTerminalFourCornerCarrierProfileTransportFormalized = true leanResidualTerminalFourCornerCarrierFailClosedPhysicalTransportFormalized = true leanResidualTerminalFourCornerCarrierAxiomAuditPassed = true leanResidualTerminalFourCornerCarrierScope = "all-finite-computed-saturated-terminal-support-squares-and-canonical-physical-profile-transport-coordinates" leanResidualTerminalFourCornerOptimaCarrierCompatibleFormalized = true leanResidualTerminalFourCornerOptimaFaithfulAmbientizationFormalized = true leanResidualTerminalFourCornerOptimaReferenceMinimumPreservedFormalized = true leanResidualTerminalFourCornerOptimaLocalizedMinimaFormalized = true leanResidualTerminalFourCornerOptimaSharedObserverProjectionFormalized = true leanResidualTerminalFourCornerOptimaAxiomAuditPassed = true leanResidualTerminalFourCornerOptimaCarrierScope = "all-finite-computed-saturated-terminal-support-squares-one-reversible-ambient-carrier-and-shared-observer-projection" leanResidualTerminalFourCornerOptimumCoherenceClassifierFormalized = true leanResidualTerminalFourCornerOptimumFirstFailureFormalized = true leanResidualTerminalFourCornerOptimumRetainedSemanticsFormalized = true leanResidualTerminalFourCornerOptimumProfileTransportFormalized = true leanResidualTerminalFourCornerOptimumModeFirewallFormalized = true leanResidualTerminalFourCornerOptimumSideTightTupleFactsFormalized = true leanResidualTerminalFourCornerOptimumCoherenceAxiomAuditPassed = true leanResidualTerminalFourCornerOptimumCoherenceScope = "all-finite-computed-terminal-support-squares-observers-projections-and-full-or-quotient-modes-coherent-tuple-or-deterministic-first-failure" leanResidualTerminalFourCornerOptimumLocalRouteClassifierFormalized = true leanResidualTerminalFourCornerOptimumRouteSoundnessFormalized = true leanResidualTerminalFourCornerOptimumRouteSilenceFormalized = true leanResidualTerminalFourCornerOptimumSideTightCompletionUnderRouteSilenceFormalized = true leanResidualTerminalFourCornerOptimumExactCompletionValuesFormalized = true leanResidualTerminalFourCornerOptimumPromotionFirewallRetained = true leanResidualTerminalFourCornerSideTightCompletionAxiomAuditPassed = true leanResidualTerminalFourCornerSideTightCompletionScope = "all-finite-computed-terminal-support-squares-observers-and-full-or-quotient-modes-side-tight-coherent-completion-under-exact-local-route-silence" leanResidualTerminalFourCornerArbitraryFamilyCoherenceFormalized = true leanResidualTerminalFourCornerExactMinimumFamilyEnumerated = true leanResidualTerminalFourCornerTightBasisFamilyComplete = true leanResidualTerminalFourCornerSignedTightBasisMaximumFormalized = true leanResidualTerminalFourCornerTightBasisMaximumEqualsDeltaFormalized = true leanResidualTerminalFourCornerTightBasisMaximumAxiomAuditPassed = true leanResidualTerminalFourCornerTightBasisMaximumScope = "all-finite-computed-terminal-support-squares-observers-and-full-or-quotient-modes-complete-tight-basis-family-and-signed-maximum-under-exact-local-route-silence" leanResidualTerminalCoherentFourCornerBasisFormalized = true leanResidualTerminalCoherentFourCornerBasisScope = "conditional-on-exact-mode-appropriate-local-route-silence-not-universal-bn2-square-legitimacy" leanResidualTerminalSquareLegitimacyFormalized = true leanResidualTerminalSquareStructuralCompatibilityFormalized = true leanResidualTerminalSquareFrontierPushoutFormalized = true leanResidualTerminalSquareSharedQuantityCarrierFormalized = true leanResidualTerminalSquareLocalConclusionUnderRouteSilenceFormalized = true leanResidualTerminalSquareFailClosedRouteDichotomyFormalized = true leanResidualTerminalSquareLegitimacyAxiomAuditPassed = true leanResidualTerminalSquareLegitimacyScope = "all-finite-computed-terminal-support-squares-explicit-terminal-dependency-systems-direct-wire-candidates-observers-and-forgetful-projections-with-local-route-silence-or-proof-bearing-first-failure" leanResidualTerminalComputedBCELAnchorNucleusFormalized = true leanResidualTerminalBCELMinimumPositiveNucleusFormalized = true leanResidualTerminalBCELAnchorAlgebraFormalized = true leanResidualTerminalBCELCutDefectFirewallFormalized = true leanResidualTerminalBCELCutRouteDichotomyFormalized = true leanResidualTerminalBCELConstantCutConclusionFormalized = true leanResidualTerminalBCELAnchorNucleusAxiomAuditPassed = true leanResidualTerminalBCELAnchorNucleusScope = "all-finite-direct-wire-candidates-explicit-terminal-dependency-systems-computed-governed-proper-positive-supports-forgetful-projections-executable-ambient-observers-and-positive-whole-support-projection-defect" leanResidualTerminalSaturationPositivityFirewallFormalized = true leanResidualTerminalSaturationPositivityFirewallAxiomAuditPassed = true leanResidualTerminalSaturationPositivityFirewallScope = "all-finite-direct-wire-candidates-explicit-terminal-dependency-systems-computed-governed-proper-positive-supports-forgetful-projections-and-executable-ambient-observers-total-zero-or-positive-whole-support-projection-defect-classification" leanResidualTerminalCandidateSaturationFormalized = true leanResidualTerminalSaturationCostBalanceFormalized = true leanResidualTerminalFirstNontransparentStepFormalized = true leanResidualTerminalSaturationCostBalanceAxiomAuditPassed = true leanResidualTerminalSaturationCostBalanceScope = "all-finite-direct-wire-candidates-executable-observers-forgetful-projections-candidate-derived-dependency-system-rule-labelled-exact-cost-balance-or-first-nontransparent-step" leanResidualTerminalInterfaceExposureRoutingFormalized = true leanResidualTerminalFiniteInterfaceExposureRoutesToEFormalized = true leanResidualTerminalInterfaceExposureZeroCostRetractFormalized = true leanResidualTerminalFirstInterfaceExposureRouteFormalized = true leanResidualTerminalInterfaceExposureRoutingAxiomAuditPassed = true leanResidualTerminalInterfaceExposureRoutingScope = "all-finite-direct-wire-candidates-executable-observers-forgetful-projections-candidate-derived-interface-consumer-transparent-or-local-e-route-with-exact-first-failure" leanResidualTerminalOriginKernelObligationRoutingFormalized = true leanResidualTerminalFiniteOriginKernelObligationClosureRoutedFormalized = true leanResidualTerminalFirstOriginKernelObligationRouteFormalized = true leanResidualTerminalOriginKernelObligationRoutingAxiomAuditPassed = true leanResidualTerminalOriginKernelObligationRoutingScope = "all-finite-direct-wire-candidates-executable-observers-forgetful-projections-candidate-derived-origin-kernel-obligation-closures-with-exact-safety-or-first-route" leanResidualTerminalFiniteSaturatePositiveCompositionFormalized = true leanResidualTerminalFiniteSaturatePositiveCompositionAxiomAuditPassed = true leanResidualTerminalFiniteSaturatePositiveCompositionScope = "all-finite-direct-wire-candidates-executable-observers-forgetful-projections-proof-bearing-positive-full-slack-candidate-bcel-anchor-problems-total-finite-saturate-positive-composition" leanResidualTerminalRankWFFormalized = true leanResidualTerminalRankWFAxiomAuditPassed = true leanResidualTerminalRankWFScope = "fixed-ten-coordinate-natural-lexicographic-order-executable-comparison-accessibility-induction-and-kernel-well-foundedness" leanResidualTerminalBN3RequestEnvelopeFormalized = true leanResidualTerminalBN3RequestEnvelopeAxiomAuditPassed = true leanResidualTerminalBN3RequestEnvelopeScope = "successful-computed-finite-bcel-anchor-nuclei-canonical-stable-request-identities-exact-singleton-minimal-consumers-duplicate-free-incidence-and-jointly-side-tight-full-or-quotient-basis-family" leanResidualTerminalBN4ActivationCancellationFormalized = true leanResidualTerminalBN4ActivationCancellationAxiomAuditPassed = true leanResidualTerminalBN4ActivationCancellationScope = "successful-computed-finite-bn3-envelope-explicit-typed-cell-ledgers-activation-exact-complete-key-same-key-cancellation-and-exact-integer-mass-residuals" leanResidualTerminalBN5FullShadowLocalizationFormalized = true leanResidualTerminalBN5FullShadowLocalizationAxiomAuditPassed = true leanResidualTerminalBN5FullShadowLocalizationScope = "all-finite-exact-coordinate-negative-unit-refinements-computed-cut-silence-complete-multiplicity-coverage-or-strict-hall-deficit-with-local-x1-nonsilence" leanResidualTerminalPkgCSeparatingConsumersFormalized = true leanResidualTerminalPkgCSeparatingConsumersAxiomAuditPassed = true leanResidualTerminalPkgCSeparatingConsumersScope = "all-finite-explicit-minimal-consumer-antichains-pkgc-separating-consumer-first-pair-canonical-atoms-exact-coordinate-restoration-or-strict-hall-local-q" leanResidualTerminalPkgCTypedRestorationFormalized = true leanResidualTerminalPkgCTypedRestorationAxiomAuditPassed = true leanResidualTerminalPkgCTypedRestorationScope = "all-finite-explicit-minimal-consumer-antichains-typed-full-restoration-candidates-coordinate-preserving-exact-multiplicity-coverage-no-hall-or-singletonized" leanResidualTerminalPkgCSameKeyCancellationFormalized = true leanResidualTerminalPkgCSameKeyCancellationAxiomAuditPassed = true leanResidualTerminalPkgCSameKeyCancellationScope = "all-finite-explicit-minimal-consumer-antichains-typed-exact-coordinate-restoration-canonical-opposite-sign-bn4-ledger-every-key-balanced-empty-residual-or-singletonized-under-cancellation-silence" leanResidualTerminalPkgCAmbientBN4LedgerFormalized = true leanResidualTerminalPkgCAmbientBN4LedgerAxiomAuditPassed = true leanResidualTerminalPkgCAmbientBN4LedgerScope = "all-finite-explicit-ambient-bn4-ledgers-exact-multiset-embedding-balanced-generated-subledger-removal-preserves-remainder-signed-mass-and-candidate-derived-canonical-atom-linkage" leanResidualTerminalConsumerAntichainNormalFormFormalized = true leanResidualTerminalConsumerAntichainNormalFormAxiomAuditPassed = true leanResidualTerminalConsumerAntichainNormalFormScope = "all-finite-minimal-consumer-antichains-monotone-empty-false-nonzero-iff-disjoint-and-pkgc-singletonized-exact-v54-consumer-antichain-cut-indicator" leanResidualTerminalConstantCutHypergraphRigidityFormalized = true leanResidualTerminalConstantCutHypergraphRigidityAxiomAuditPassed = true leanResidualTerminalConstantCutHypergraphRigidityScope = "all-finite-nonnegative-weighted-hypergraphs-constant-cut-hypergraph-rigidity-v53-q2-q3-q4-classification" leanResidualTerminalBN6HypergraphPacketFormalized = true leanResidualTerminalBN6HypergraphPacketAxiomAuditPassed = true leanResidualTerminalBN6HypergraphPacketScope = "all-finite-explicit-grouped-v54-activation-to-v53-grouped-hypergraph-packet-bn6-pair-mixed-triple-fullspan-with-payload-witnesses" leanSaturatePositiveFormalized = false leanBCELReadyFormalized = false leanResidualRoutesGlobalGainCompletenessFormalized = false leanZeroSlackCompletenessFormalized = false leanConcreteCookLevinFormulaBuilderFormalized = false concretePublicationGate.passed = false
Static fail-closed boundary: missing, malformed, stale, or digest-mismatched data never enables theorem publication.
Coordinate PNP-LEAN-THEOREM-INVENTORY-2026-08-12-133; SHA-256 696c76220a092e5a84e7caa804fd1c57889f193968d1285b520c408f8237f5c1. Coordinate alone is not authority; the release also pins commit, tree, and artifact hashes.
27,794 public declarations; 14,454 theorem-kind declarations; 7,347 assumption-free theorem-kind declarations; 15,008 private compiler auxiliaries excluded; 250 modules; 4 project axioms.
The inventory is emitted from Lean environment constants and axiom collection. It is not inferred from source text, JSON claims, checker acceptance, or report prose.
The static rows below are conservative fallback copy. When validation succeeds, JavaScript replaces them from the exact status payload.
Every proof-bearing function or decision program tree compiles recursively into one literal finite raw machine. Sequential composition preserves verdict, machineOutput, acceptance, no-timeout, and stuck-first timeout with Rseq(m) = PipelineRaw(p)(m) + 6 + PipelineRaw(q)(m + p(m) + 1).
Boundary: This closes the concrete complexity machine-link blocker only; it does not provide a polynomial-time CNF-SAT decider or NP-completeness reduction.
Finite charged decision, verifier, and function pipelines grounded in concrete machine leaves, with polynomial certificate, runtime, output, and recursively compiled exact raw-machine refinement bounds.
Boundary: Concrete CNF-SAT in P, NP-completeness, and the root theorem remain absent.
An explicit paired finite-machine verifier with formula and assignment decoders, exact accept/reject semantics, no timeout at a polynomial fuel bound, and CNFSAT ∈ NP via PNP.Concrete.FinalUniversalDesign.cnfSATInNP.
Boundary: This does not prove CNF-SAT in P, NP-completeness, or P = NP.
Executable time, tape, state, and certificate dimensions with proved disjoint in-range Boolean-variable blocks.
Boundary: This layout alone is not a CNF reduction.
The canonical bounded raw trace is exactly characterized by intrinsic transition validity and agrees with boundedDecide.
Boundary: This fixed-certificate semantics alone does not emit CNF.
Language membership is equivalent to an existential bounded accepting tableau under one answer-independent raw fuel bound.
Boundary: No complete Boolean encoding or reduction polynomial follows from this milestone alone.
Finite local constraints compile to well-scoped clauses with exact satisfaction and clause-count theorems.
Boundary: This does not yet enumerate the whole verifier tableau.
An answer-independent, finite, well-scoped formula encodes initialization, first-match transitions, preservation, and final acceptance.
Boundary: Syntax and local reflection alone are not the final semantic or complexity proof.
Formula satisfiability is exactly equivalent to an intrinsic finite accepting tableau. The reviewed theorem closures use only permitted Lean standard axioms and no project axiom.
Boundary: The following raw-tape bridge supplies the concrete execution connection.
encodedFormula_mem_CNFSAT_iff_language connects the generated CNF exactly to ordinary raw Tape execution and the verifier language.
Boundary: This is semantic reduction correctness; the following milestone supplies encoded-output size only.
encodedFormula_size_le bounds the actual canonical unary-indexed CNF encoding by an explicit fixed-verifier polynomial evaluated at external input length. Its closure is [Quot.sound, propext], with no project or choice axiom.
Boundary: A raw formula builder and construction-runtime polynomial, packaged PolynomialReduction, CNF-SAT NP-completeness, CNF-SAT in P, and P = NP remain absent.
formulaBitSchedule_length proves an exact external-input polynomial slot count, and formulaBitSchedule_emit_eq_encodedFormula proves that removing empty slots reproduces the canonical encoded formula. The schedule is answer-independent and its closure is [Quot.sound, propext], with no project or choice axiom.
Boundary: This is a pure schedule specification. It supplies no constant-time raw interpretation, raw formula builder, construction-runtime polynomial, FunctionProgram.RawRefinement, packaged PolynomialReduction, NP-completeness, CNF-SAT in P, or P = NP.
Direct constraint, clause, token, and raw-bit decoders agree with the canonical schedules while distinguishing out-of-range, valid padding, and populated slots. Exact prefix, full, one-step-short, terminal, and excess-fuel theorems culminate in FormulaBitCursor.run_full_emit_eq_encodedFormula. All 129 explicit declarations are audited; the 16 reviewed theorem types use [Quot.sound, propext], with no project or choice axiom.
Boundary: This is a Lean specification cursor. It proves no constant-time raw slot interpretation, raw finite builder, construction-runtime theorem, FunctionProgram.RawRefinement, packaged PolynomialReduction, NP-completeness, CNF-SAT in P, or P = NP.
BuilderInputLength.workRunExact_after_totalInputFramer connects a fixed 19-rule work machine to the proved all-input framer endpoint. It preserves every source bit, appends one unary tally symbol per input bit in fresh workspace, and returns to the source head. It accepts after exactly 2*n*n + 4*n + 2 work steps; the compiled raw run takes exactly 12*n*n + 24*n + 12 steps. Malformed internal scan symbols and one-step-short fuel time out. All 39 public declarations are audited; the ten reviewed theorem types use only [Quot.sound, propext], with no project or choice axiom.
Boundary: This is only input-length preparation. It does not emit formula bits, interpret direct cursor slots as raw transitions, compose a complete raw formula builder, construct a FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNF-SAT NP-completeness, establish CNF-SAT in P, or prove P = NP.
BuilderInputPrefix.workRunExact proves one literal finite work machine runs the all-input framer, takes an explicit nine-symbol launch transition, and executes the fixed 19-rule tally machine in pairwise-disjoint state namespaces. It preserves the represented input and reaches the exact unary tally after totalInputFramerWorkSteps(input) + 1 + 2*n*n + 4*n + 2 work steps. The compiled execution has external raw bound 18*n*n + 63*n + 93. Malformed tally-scan symbols and one-step-short fuel time out. All 40 public declarations are audited; the fourteen reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext], with no project or choice axiom.
Boundary: This prefix emits no formula bits and does not interpret the direct cursor, complete the raw formula builder, construct a builder FunctionProgram.RawRefinement, package a concrete PolynomialReduction, establish CNF-SAT NP-completeness, establish CNF-SAT in P, or prove P = NP.
BuilderTokenAppender.appendToken_workRunExact proves a fixed 59-rule finite work machine appends each requested token exactly for every represented input, unary tally, prior output, and exterior tape. The first-header specialization emits the first two direct formula bits and has compiled external raw bound 24*n + 48. Malformed tally/output phase symbols and one-step-short fuel time out. All 68 public declarations are audited; the seventeen reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext], with no project or choice axiom.
Boundary: This milestone audits the reusable appender independently. Its composed first-token use is the next milestone; neither milestone traverses the remaining header/body schedule or completes the raw formula builder.
BuilderFirstTokenPrefix.workRunExact proves one literal 184-rule finite machine contains all 116 input-prefix rules, nine symbol-preserving bridge rules, and all 59 appender rules under injective disjoint state maps. Every raw input is framed, tallied, launched, and extended with exactly the first T token. The emitted two bits equal encodedFormula.take 2, and the compiled external bound is 18*n*n + 87*n + 147. Prefix-endpoint, malformed tally/output, and one-step-short cases time out. All 37 public declarations and 25 reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext].
Boundary: This emits only the fixed first token. It does not compute the remaining width header, traverse a dynamic cursor, complete the formula builder, construct a builder FunctionProgram.RawRefinement, package a reduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderCompleteHeader.workRunExact proves one literal finite work machine composes the 184-rule input/first-token prefix, a structurally generated unary NatPolynomial evaluator, a 16-rule controller, two 59-rule appender copies, and five total nine-symbol bridges under injective pairwise-disjoint state maps. Its rule table has exactly 363 + BuilderUnaryPolynomial.ruleCount(widthPolynomial verifier) entries. Every raw input emits exactly FormulaWidth copies of T followed by F; finalTokenBits_eq_encodedFormula_header identifies those bits with encodedFormula.take (2 * (FormulaWidth + 1)), and an external NatPolynomial bounds the compiled run. The evaluator's 74 and composition's 84 public declarations are completely axiom-audited; all 48 reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext].
Boundary: This is the complete answer-independent width header only. It does not implement the dynamic cursor or formula body, complete the formula builder, construct a builder FunctionProgram.RawRefinement, package a reduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderBodyStartPrefix.workRunExact proves one literal finite work machine composes the complete width-header machine, a unary evaluator for the next token slot, and the reusable appender. Every raw input emits T^FormulaWidth F Sep; bodyStartTokens_eq_canonical_prefix identifies the token sequence with the canonical prefix, while nextTokenSlot_eq_formulaVariableSlotBound_add_two and finalOutside_contains_nextTokenSlot retain the next token coordinate. Its rule table has exactly 440 + BuilderUnaryPolynomial.ruleCount(widthPolynomial verifier) + BuilderUnaryPolynomial.ruleCount(nextTokenSlotPolynomial verifier) entries, and an external NatPolynomial bounds the compiled run. All 60 public declarations are axiom-audited; all 42 reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext].
Boundary: This emits only the fixed separator that starts the formula body. It does not implement the dynamic cursor or subsequent body tokens, complete the formula builder, construct a builder FunctionProgram.RawRefinement, package a reduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFirstLiteralPrefix.workRunExact proves one literal finite work machine composes the body-start prefix, a unary evaluator for the next token slot, and two reusable appender copies. Every raw input emits T^FormulaWidth F Sep T F, the canonical first positive literal for variable zero; firstLiteralTokens_eq_canonical_formula_prefix identifies the exact token prefix, while nextTokenSlot_eq_formulaVariableSlotBound_add_four retains the following token coordinate. Its rule table has exactly 585 + BuilderUnaryPolynomial.ruleCount(widthPolynomial verifier) + BuilderUnaryPolynomial.ruleCount(BuilderBodyStartPrefix.nextTokenSlotPolynomial verifier) + BuilderUnaryPolynomial.ruleCount(nextTokenSlotPolynomial verifier) entries, with an external NatPolynomial compiled bound. All 74 public declarations are axiom-audited; all 52 reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext].
Boundary: This emits only the fixed first literal. It does not implement a dynamic cursor or subsequent body tokens, complete the formula builder, construct a builder FunctionProgram.RawRefinement, package a reduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFirstClausePrefix.workRunExact proves one literal finite work machine composes the first-literal prefix, a unary evaluator for the retained next-token coordinate, and a fixed eight-token tail. Every raw input emits T^FormulaWidth F Sep T F T T F T T T F Finish, the canonical prefix through the complete positive first clause on variables zero, one, and two; firstClauseTokens_eq_canonical_formula_prefix identifies the exact token prefix, while nextTokenSlot_eq_formulaVariableSlotBound_add_twelve retains formulaVariableSlotBound + 12 as the following token coordinate. Its rule table has exactly 1138 + BuilderUnaryPolynomial.ruleCount(widthPolynomial verifier) + BuilderUnaryPolynomial.ruleCount(BuilderBodyStartPrefix.nextTokenSlotPolynomial verifier) + BuilderUnaryPolynomial.ruleCount(BuilderFirstLiteralPrefix.nextTokenSlotPolynomial verifier) + BuilderUnaryPolynomial.ruleCount(nextTokenSlotPolynomial verifier) entries, with an external NatPolynomial compiled bound. All 79 public declarations are axiom-audited, and the combined 80-declaration audit covers predecessor halt separation; all 43 reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext].
Boundary: This emits only the fixed complete first clause and retains its following coordinate as data. It does not implement a dynamic cursor or remaining body tokens, complete the formula builder, construct a builder FunctionProgram.RawRefinement, package a reduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderDynamicTokenCursorStep.workRunExact proves one literal finite machine composes the complete first-clause machine, nine launch rules, and a fixed 45-rule cursor advance. Every raw input preserves the complete first-clause output, consumes the proved first in-range padding opportunity, and advances the retained unary coordinate from formulaVariableSlotBound + 12 to + 13. The suffix costs exactly 2*cursorWord.length + 8 work steps including launch and fits BuilderFirstClausePrefix.rawTimeBound + 48 + 12*cursorWord.length compiled steps. All 47 public declarations, including the two downstream dispatch facts, are axiom-audited; all 31 reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext].
Boundary: This is one padding transition, not a general dynamic cursor loop or arbitrary raw slot decoder. It emits no token and supplies no remaining formula body, complete builder, builder FunctionProgram.RawRefinement, packaged reduction, CNF-SAT NP-completeness or in-P, or P = NP.
BuilderFirstClausePaddingRun.workRunExact proves one literal finite machine composes the preceding cursor step, two structurally generated unary evaluators, and a fixed 25-rule countdown controller. Every raw input executes exactly D = (FormulaVariableSlotBound - 1) * (FormulaVariableSlotBound + 6) = FormulaTokensPerClause - 12 remaining first-clause padding opportunities without emitting a token, then reaches FormulaVariableSlotBound + 1 + FormulaTokensPerClause, whose next direct schedule outcome is Sep. Its literal table has 1244 plus six inherited/generated evaluator rule counts, with an explicit external NatPolynomial compiled bound. The 84-line combined audit covers 83 public declarations plus one predecessor transport theorem; all 48 reviewed theorem types use only empty closure, [propext], or [Quot.sound, propext].
Boundary: This is the exact remaining first-clause padding block and second-clause boundary only. It is not a general dynamic formula cursor and supplies no remaining formula-body emitter, complete builder, builder RawRefinement, PolynomialReduction, CNF-SAT NP-completeness or in-P result, or P = NP theorem.
BuilderSecondClauseSeparatorStep.workRunExact proves one literal finite machine composes the complete padding run with a selected 59-rule Sep appender, two total nine-symbol bridges, and the existing fixed 45-rule cursor advance. Its table has 1366 plus six inherited/generated unary-evaluator rule counts. Every raw input emits the canonical separator beginning clause two, advances the retained coordinate by one, and emits bits equal to encodedFormula.take (2 * (FormulaWidth + 13)); nextTokenSlot_direct_eq_f proves that the following direct token is F. The compiled run is bounded by BuilderFirstClausePaddingRun.rawTimeBound + 246 + 24*n + 12*FormulaWidth + 12*cursorWord.length. The combined audit covers 54 new public declarations and two predecessor dispatch facts; all 56 audited declarations use only empty closure, [propext], or [Quot.sound, propext]. Malformed appender tally/output, malformed cursor scratch, both unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed populated Sep transition and advances to the following F coordinate. It is not a general dynamic formula cursor, does not emit that F or the remaining body, and supplies no complete builder, builder RawRefinement, PolynomialReduction, CNF-SAT NP-completeness or in-P result, or P = NP theorem.
BuilderSecondClauseFirstLiteralPrefix.workRunExact proves one literal finite machine composes the complete separator prefix with two selected 59-rule F appenders, four total symbol-preserving bridges, and two copies of the fixed 45-rule cursor advance. One F/cursor component has 113 rules, the two-component suffix has 235 rules, and the global table has 1610 plus six inherited/generated unary-evaluator rule counts. Every raw input emits T^FormulaWidth F Sep T F T T F T T T F Finish Sep F F, the canonical prefix through the complete negative literal on variable zero in clause two. The emitted bits equal encodedFormula.take (2 * (FormulaWidth + 15)), the retained coordinate is secondClauseStart + 3, and direct schedule facts prove the sign, unary-zero terminator, and following sign are all F. The compiled run is bounded by BuilderSecondClauseSeparatorStep.rawTimeBound + 564 + 48*n + 24*FormulaWidth + 24*cursorWord.length. All 85 new public declarations plus two reviewed cursor dead-loop facts are axiom-audited: 25 have empty closure, 18 use only [propext], and 44 use only [Quot.sound, propext]. Malformed tally/output in either appender, malformed scratch in either cursor, all four unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed negative literal on variable zero and advances to the following negative-sign coordinate. It does not complete clause two, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderSecondClauseSecondLiteralPrefix.workRunExact proves one literal finite machine composes the complete first-literal prefix with selected 59-rule F, T, and F appenders, six total symbol-preserving bridges, and three copies of the fixed 45-rule cursor advance. The selected T/cursor component has 113 rules, the T/F tail has 235 rules, the complete suffix has 357 rules, and the global table has 1976 plus six inherited/generated unary-evaluator rule counts. Every raw input emits T^FormulaWidth F Sep T F T T F T T T F Finish Sep F F F T F, the canonical prefix through the complete negative literal on variable one in clause two. The emitted bits equal encodedFormula.take (2 * (FormulaWidth + 18)), the retained coordinate is secondClauseStart + 6 at the following Finish, and direct schedule facts prove the sign F, unary unit T, terminator F, and following Finish. The compiled run is bounded by BuilderSecondClauseFirstLiteralPrefix.rawTimeBound + 1026 + 72*n + 36*FormulaWidth + 36*cursorWord.length. All 113 new public declarations plus two reviewed cursor dead-loop facts are axiom-audited: 34 have empty closure, 25 use only [propext], and 56 use only [Quot.sound, propext]. Malformed tally/output in any appender, malformed scratch in any cursor, all six unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed negative literal on variable one and retains the following Finish coordinate. It does not emit that Finish or clause terminator, complete clause two, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderSecondClausePrefix.workRunExact proves one literal finite machine composes the complete second-literal prefix with a selected 59-rule Finish appender, two total symbol-preserving bridges, and one copy of the fixed 45-rule cursor advance. The suffix has 113 rules and the global table has 2098 plus six inherited/generated unary-evaluator rule counts. Every raw input emits T^FormulaWidth F Sep T F T T F T T T F Finish Sep F F F T F Finish, the canonical prefix through the complete second clause. The emitted bits equal encodedFormula.take (2 * (FormulaWidth + 19)), the retained coordinate is secondClauseStart + 7 at the first in-range padding opportunity, and direct schedule facts prove the executed token is Finish while the retained next opportunity is padding. The compiled run is bounded by BuilderSecondClauseSecondLiteralPrefix.rawTimeBound + 390 + 24*n + 12*FormulaWidth + 12*cursorWord.length. All 55 new public declarations plus two reviewed cursor dead-loop facts are axiom-audited: 15 have empty closure, 10 use only [propext], and 32 use only [Quot.sound, propext]. Malformed appender tally/output, malformed cursor scratch, both unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed Finish terminator that completes clause two and advances to its first padding coordinate. It does not traverse clause-two padding, reach clause three, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderSecondClausePaddingRun.workRunExact proves one literal finite machine composes the complete second-clause prefix with structurally generated unary evaluators for D = (V - 1) * (V + 6) + 5 and the clause-three coordinate, the fixed 25-rule padding countdown, and three total symbol-preserving bridges. Its table has 2150 plus eight inherited/generated unary-evaluator rule counts. Every raw input traverses all D = C - 7 remaining second-clause padding coordinates without emitting a token, reaches V + 1 + 2*C, and proves the retained direct schedule value is Sep. The emitted bits remain encodedFormula.take (2 * (FormulaWidth + 19)). The compiled run has an explicit external input-size polynomial bound. All 65 new public declarations plus three reviewed reused-countdown declarations are audited: 26 have empty closure, 9 use only [propext], and 33 use only [Quot.sound, propext]. Malformed countdown root/scratch, the unlaunched predecessor endpoint, and one-step-short fuel time out.
Boundary: This executes exactly the remaining clause-two padding block and reaches clause three only as a retained coordinate. It does not emit the retained Sep, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderThirdClauseSeparatorStep.workRunExact proves one literal finite machine composes the complete clause-two padding run with a selected 59-rule Sep appender, two total nine-symbol bridges, and the existing fixed 45-rule cursor advance. Its table has 2272 plus eight inherited/generated unary-evaluator rule counts. Every raw input emits the canonical separator beginning clause three, advances the retained coordinate by one, and emits bits equal to encodedFormula.take (2 * (FormulaWidth + 20)); nextTokenSlot_direct_eq_f proves the following direct token is F. The compiled run is bounded by BuilderSecondClausePaddingRun.rawTimeBound + 330 + 24*n + 12*FormulaWidth + 12*cursorWord.length. The combined audit covers 48 new public declarations and eight reviewed suffix interfaces: 14 have empty closure, 11 use only [propext], and 31 use only [Quot.sound, propext]. Malformed appender tally/output, malformed cursor scratch, both unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed populated Sep transition beginning clause three and advances to the following F coordinate. It is not a general dynamic formula cursor or arbitrary raw decoder, does not emit that F or the remaining formula body, and does not supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderThirdClauseFirstLiteralPrefix.workRunExact proves one literal finite machine composes the complete third-clause separator prefix with the reused 235-rule two-F appender/cursor suffix behind one total nine-symbol bridge. Its global table has 2516 plus eight inherited/generated unary-evaluator rule counts. Every raw input emits the canonical prefix through the complete negative literal on variable zero in clause three. The emitted bits equal encodedFormula.take (2 * (FormulaWidth + 22)), the retained coordinate is thirdClauseStart + 3, and direct schedule facts prove the literal sign, unary-zero terminator, and following sign are all F. The compiled run is bounded by BuilderThirdClauseSeparatorStep.rawTimeBound + 732 + 48*n + 24*FormulaWidth + 24*cursorWord.length. The combined audit covers 74 new public declarations, eleven reviewed reused suffix/cursor interfaces, and two predecessor cursor facts: 24 have empty closure, 18 use only [propext], and 45 use only [Quot.sound, propext]. Malformed tally/output in either appender, malformed scratch in either cursor, all four unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed negative literal on variable zero in clause three and advances to the following negative-sign coordinate. It does not emit that following F, complete clause three, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderThirdClauseSecondLiteralPrefix.workRunExact proves one literal finite machine composes the complete first-literal prefix with a fixed 479-rule F T T F appender/cursor suffix behind one total nine-symbol bridge. Its nested tables have 113, 235, 357, and 479 rules, and its global table has 3004 plus eight inherited/generated unary-evaluator rule counts. Every raw input emits the canonical prefix through the complete negative literal on variable two in clause three. The emitted bits equal encodedFormula.take (2 * (FormulaWidth + 26)), the retained coordinate is thirdClauseStart + 7, and direct schedule facts prove the sign F, both unary units T, terminator F, and following Finish. The compiled run is bounded by BuilderThirdClauseFirstLiteralPrefix.rawTimeBound + 1752 + 96*n + 48*FormulaWidth + 48*cursorWord.length. All 145 public declarations are axiom-audited: 46 have empty closure, 32 use only [propext], and 67 use only [Quot.sound, propext]. Malformed tally/output in all four appenders, malformed scratch in all four cursors, all eight unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed negative literal on variable two in clause three and advances to the following Finish coordinate. It does not emit that following Finish, complete clause three, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderThirdClausePrefix.workRunExact proves one literal finite machine composes the complete second-literal prefix with a selected 59-rule Finish appender, two total symbol-preserving bridges, and one copy of the fixed 45-rule cursor advance. The suffix has 113 rules and the global table has 3126 plus eight inherited/generated unary-evaluator rule counts. Every raw input emits the canonical prefix through the complete third clause. The emitted bits equal encodedFormula.take (2 * (FormulaWidth + 27)), the retained coordinate is thirdClauseStart + 8 at the first in-range padding opportunity, and direct schedule facts prove the executed token is Finish while the retained next opportunity is padding. The compiled run is bounded by BuilderThirdClauseSecondLiteralPrefix.rawTimeBound + 498 + 24*n + 12*FormulaWidth + 12*BuilderThirdClauseSeparatorStep.cursorWord.length. All 55 new public declarations plus two reviewed cursor dead-loop facts are axiom-audited: 14 have empty closure, 10 use only [propext], and 33 use only [Quot.sound, propext]. Malformed appender tally/output, malformed cursor scratch, both unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed Finish terminator that completes clause three and advances to its first padding coordinate. It does not traverse clause-three padding, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderThirdClausePaddingRun.workRunExact proves one literal finite machine composes the complete third-clause prefix with two structurally generated unary-polynomial evaluators, the reused 25-rule PaddingCountdown controller, and three total symbol-preserving bridges. Its global table has 3178 plus ten inherited/generated unary-evaluator rule counts. Every raw input traverses exactly FormulaTokensPerClause - 8 remaining clause-three padding coordinates without emission, preserves encodedFormula.take (2 * (FormulaWidth + 27)), and reaches FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause, where direct lookup proves Sep. The combined 68-declaration audit has 26 empty closures, 9 using only [propext], and 33 using only [Quot.sound, propext]. Malformed countdown root/scratch states, the unlaunched predecessor endpoint, and one-step-short fuel time out.
Boundary: This executes exactly the remaining third-clause padding block and reaches clause four only as a retained coordinate. It does not emit the fourth-clause separator, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFourthClauseSeparatorStep.workRunExact proves one literal finite machine composes the complete third-clause padding run with the reused 113-rule selected Sep appender/cursor machine through one total nine-symbol bridge. Its literal table has 3300 plus ten inherited/generated unary-evaluator rule counts. Every raw input emits exactly the fourth-clause Sep, preserves encodedFormula.take (2 * (FormulaWidth + 28)), advances the retained coordinate to FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause + 1, and proves the following direct token is F. The compiled run is bounded by BuilderThirdClausePaddingRun.rawTimeBound + 426 + 24*n + 12*FormulaWidth + 12*cursorWord.length. The combined 56-declaration audit covers all 48 new public declarations plus eight reused separator/cursor and dead-state interfaces using only the approved Lean-standard closure, with no project axiom or Classical.choice. Malformed appender tally/output, malformed cursor scratch, both unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only the fixed separator beginning clause four. It does not emit the following F, complete clause four, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFourthClauseFirstLiteralPrefix.workRunExact proves one literal finite 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 bridge. Its literal table has 3666 plus ten inherited/generated unary-evaluator rule counts. Every raw input emits the complete first negative literal on variable one in clause four, preserves encodedFormula.take (2 * (FormulaWidth + 31)), advances the retained coordinate to FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause + 4, and proves the following direct token is F. The compiled run is bounded by BuilderFourthClauseSeparatorStep.rawTimeBound + 1422 + 72*n + 36*FormulaWidth + 36*cursorWord.length. The combined 115-declaration audit covers all 97 new public declarations, 16 reviewed reused suffix interfaces, and two cursor dead-state facts: 33 have empty closure, 25 use only [propext], and 57 use only [Quot.sound, propext]. No audited declaration uses a project axiom or Classical.choice. Malformed tally/output and cursor scratch in all three appender stages, all six unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only 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, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFourthClauseSecondLiteralPrefix.workRunExact proves one literal finite 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 bridge. Its literal table has 4154 plus ten inherited/generated unary-evaluator rule counts. Every raw input emits the complete second negative literal on variable two in clause four, preserves encodedFormula.take (2 * (FormulaWidth + 35)), advances the retained coordinate to FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause + 8, and proves the following direct token is Finish. The compiled run is bounded by BuilderFourthClauseFirstLiteralPrefix.rawTimeBound + 2232 + 96*n + 48*FormulaWidth + 48*cursorWord.length. The combined 147-declaration audit covers all 124 new public declarations, 21 reviewed reused suffix interfaces, and two cursor dead-state facts: 46 have empty closure, 32 use only [propext], and 69 use only [Quot.sound, propext]. No audited declaration uses a project axiom or Classical.choice. Malformed tally/output and cursor scratch in all four appender stages, all eight unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits only 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, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFourthClausePrefix.workRunExact composes the complete second-literal prefix with a selected 59-rule Finish appender, the existing 45-rule cursor advance, and two total nine-symbol bridges. Its selected suffix has 113 rules, and its literal table has 4276 plus ten inherited/generated unary-evaluator rule counts. Every raw input emits the Finish that completes clause four, preserves encodedFormula.take (2 * (FormulaWidth + 36)), advances to FormulaVariableSlotBound + 1 + 3 * FormulaTokensPerClause + 9, and proves the next direct token is padding. The compiled run is bounded by BuilderFourthClauseSecondLiteralPrefix.rawTimeBound + 618 + 24*n + 12*FormulaWidth + 12*BuilderFourthClauseSeparatorStep.cursorWord.length. The 57-declaration audit covers all 55 new public declarations and two cursor dead-state facts: 14 have empty closure, 10 use only [propext], and 33 use only [Quot.sound, propext]. No audited declaration uses a project axiom or Classical.choice. Malformed appender tally/output, malformed cursor scratch, both unlaunched endpoints, and one-step-short fuel time out.
Boundary: This emits exactly the fixed Finish terminator that completes clause four and advances to its first padding coordinate. It does not by itself traverse clause-four padding, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFourthClausePaddingRun.workRunExact composes the complete fourth-clause prefix with two structurally generated unary evaluators, the reused 25-rule PaddingCountdown machine, and three total nine-symbol bridges. Its literal table has 4328 plus twelve inherited/generated unary-evaluator rule counts. Every raw input traverses exactly FormulaTokensPerClause - 9 remaining padding opportunities without emitting a token, preserves encodedFormula.take (2 * (FormulaWidth + 36)), advances to FormulaVariableSlotBound + 1 + 4 * FormulaTokensPerClause, and proves the target is padding in the intentionally empty fifth clause rectangle. The compiled run is bounded by BuilderFourthClausePrefix.rawTimeBound + 18 plus six times the count-evaluator work, countdown bound, and target-evaluator work. The 68-declaration audit covers all 65 new public declarations and three reused countdown interfaces: 26 have empty closure, 9 use only [propext], and 33 use only [Quot.sound, propext]. No audited declaration uses a project axiom or Classical.choice. Both malformed countdown phases, the unlaunched predecessor endpoint, and one-step-short fuel time out.
Boundary: This traverses only the remaining padding in clause four. It does not traverse the empty fifth rectangle, reach the next constraint, emit another token, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFifthClausePaddingRun.workRunExact composes the complete fourth-clause padding run with two structurally generated unary evaluators, the reused 25-rule PaddingCountdown machine, and three total nine-symbol bridges. Its literal table has 4380 plus fourteen inherited/generated unary-evaluator rule counts. Every raw input traverses exactly FormulaTokensPerClause padding opportunities across the entire intentionally empty fifth clause rectangle without emitting a token, preserves encodedFormula.take (2 * (FormulaWidth + 36)), advances to FormulaVariableSlotBound + 1 + 5 * FormulaTokensPerClause, and proves every traversed opportunity and the target in the intentionally empty sixth clause rectangle are padding. The compiled run is bounded by BuilderFourthClausePaddingRun.rawTimeBound + 18 plus six times the count-evaluator work, countdown bound, and target-evaluator work. The 68-declaration audit covers all 65 new public declarations and three reused countdown interfaces: 28 have empty closure, 9 use only [propext], and 31 use only [Quot.sound, propext]. No audited declaration uses a project axiom or Classical.choice. Both malformed countdown phases, the unlaunched predecessor endpoint, and one-step-short fuel time out.
Boundary: This traverses only the intentionally empty fifth clause rectangle. It does not traverse the empty sixth rectangle, reach the next constraint, emit another token, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderFirstConstraintPaddingRun.workRunExact composes the fifth-clause padding predecessor with two structurally generated unary evaluators, the reused 25-rule PaddingCountdown machine, and three total nine-symbol bridges. Its literal table has 4464 plus sixteen inherited/generated unary-evaluator rule counts. Every raw input traverses exactly (FormulaVariableSlotBound - 2) * (FormulaVariableSlotBound + 2) * FormulaTokensPerClause remaining empty token opportunities in the first scheduled constraint without emitting a token, preserves encodedFormula.take (2 * (FormulaWidth + 36)), and advances to FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause. Direct schedule lookup proves every traversed opportunity is padding and the retained token is the Sep beginning the second scheduled constraint. The compiled run is bounded by BuilderFifthClausePaddingRun.rawTimeBound + 18 plus six times the count-evaluator work, countdown bound, and target-evaluator work. The 68-declaration audit covers all 65 new public declarations and three reused countdown interfaces, with only the approved Lean-standard closure and no project axiom or Classical.choice. Both malformed countdown phases, the unlaunched predecessor endpoint, and one-step-short fuel time out.
Boundary: This traverses only the remaining empty clause rectangles of the first scheduled constraint. It observes but does not emit the separator beginning the second scheduled constraint, does not emit the next constraint's first literal, implement a general dynamic formula cursor or arbitrary raw decoder, emit the remaining formula body, supply a complete builder or builder RawRefinement, package a PolynomialReduction, establish CNF-SAT NP-completeness or in-P, or prove P = NP.
BuilderSecondConstraintSeparatorStep.workRunExact proves that, 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.
BuilderSecondConstraintFirstLiteralSignStep.workRunExact proves that, for every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete second-constraint separator with the reused 113-rule selected T appender/cursor suffix 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 T sign beginning the first literal in the second scheduled constraint; preserves encodedFormula.take (2 * (FormulaWidth + 38)); and retains coordinate FormulaVariableSlotBound + 1 + FormulaClauseSlotsPerConstraint * FormulaTokensPerClause + 2, whose direct next schedule token is the unary T beginning variable zero. 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 appender/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 positive sign beginning the second constraint's first literal. It observes but does not emit the following unary T, complete that literal or traverse the second constraint, 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.
BuilderSecondConstraintFirstLiteralFirstUnaryUnitStep.workRunExact proves that, 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.
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.
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.
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.
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.
For every fixed concrete polynomial-time verifier, one literal finite work machine composes the complete width-selected 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 handles exactly one width-dependent opportunity after the successor token: it consumes padding without emission at width one or emits the first unary T of the second literal at wider widths. It does not consume the following padding opportunity at width one or second 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.
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.
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.
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.
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.
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.
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.
Typed topological Boolean NAND programs and ordered multi-output direct-wire semantics.
Boundary: This does not establish circuit minimization, SAT, or P = NP.
Exhaustive finite Boolean direct-wire search under the empty-profile reference model.
Boundary: No polynomial-runtime result is obtained from this exhaustive reference search.
The concrete serial framed context with support outputs and explicit bypass wires.
Boundary: This is not an arbitrary-support replacement theorem for the global family.
Typed local macro candidates, source-derived counts, and five finite local square baselines.
Boundary: Local minima are not a global BaselineDistinct or locked-NAND threshold theorem.
For every finite topologically ordered NAND circuit, an exact X/T/O/R/L/z carrier gives inputs and each gate six tagged coordinates plus one fresh final lock coordinate. There are exactly three distinguished checks per gate. Completeness constructs a coherent carrier trace from ordinary evaluation, soundness recovers the same evaluation from any accepted trace, and satisfiability is equivalent to the existence of a coherent trace. The 71-declaration audit uses only propext and Quot.sound beyond the Lean kernel, with no project axiom or Classical.choice.
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.
For every finite topologically ordered NAND circuit, the construction assembles an exact source-derived baseline candidate of size B with B outputs and a full candidate of size B + 4 with B + 1 outputs. The original source and initial conjunction semantics are preserved, the fresh final output has its exact conjunction meaning, neither candidate uses internal constants, and the baseline outputs are structurally independent of the fresh final lock. The complete module audit now covers 64 public declarations and uses only propext and Quot.sound beyond the Lean kernel.
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.
For every finite topologically ordered NAND circuit, all exposed baseline outputs are nonconstant, are not positive input projections, and are pairwise semantically distinct. Those facts satisfy the global BaselineDistinct package and prove the exact exhaustive reference minimum is B. The five reviewed theorem types close only over propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: Baseline distinctness 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.
For every finite topologically ordered NAND circuit, unsatisfiability makes the full candidate's final coordinate false on the entire carrier, including inconsistent workspace assignments, and fixes the exhaustive reference minimum at B. Both reviewed theorem types close only over propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This branch is retained as one side of the later typed semantic threshold; by itself it does not prove satisfiable separation or construct the uniform polynomial builder.
For every finite topologically ordered NAND circuit, one answer-independent full candidate supplies all six typed semantic premises. Its exact exhaustive reference minimum is at least B + 1 exactly when the source circuit is satisfiable, and its residual slack is at most 4. The eight reviewed theorem pins close only over propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: This typed semantic theorem does not construct or compile the encoded polynomial-time SAT-to-locked-NAND builder, establish CNF-SAT in P, prove NP-hardness transport, discharge the abstract locked-NAND threshold axiom, or prove P = NP.
A strict version-zero codec gives exact token, normalized-circuit, and complete-instance round trips. For every successfully decoded circuit, a pure construction emits the full candidate bytes and preserves the typed threshold: encoded_fullCandidate_threshold_iff_satisfiable is true exactly when the source circuit is satisfiable. Malformed source bytes are rejected. The 48-declaration audit uses only approved Lean-standard closure.
Boundary: The downstream parser, emitter, and concrete reduction now make this construction executable with exact language equivalence. This milestone alone does not discharge the abstract locked-NAND threshold, establish CNF-SAT NP-completeness or in P, or prove P = NP.
One literal nine-symbol finite work machine validates every source bitstring. Its 228 states and 2,052 pairwise-query-distinct rules accept exactly ValidEncodedCircuit, preserve valid bytes byte-for-byte, reject invalid bytes with empty output, and cannot time out within the compiled bound 6 * 4096 * (n + 1)^3. Polynomial-time machine/function witnesses and the validator leaf's exact RawRefinement are proved. The audit covers 380 public declarations: 247 have empty closure, 58 use only propext, and 75 use only propext and Quot.sound.
Boundary: The downstream emitter and reduction now compose with this parser. The source language is still the project-specific EncodedNANDSAT, not ordinary CNF-SAT, and the abstract threshold, hardness transport, CNF-SAT results, and P = NP remain unresolved.
One fixed nine-symbol grammar-only controller has exactly 1,387,921 pairwise-query-distinct rules. It rejects malformed grammar with empty output and emits the exact direct target for every grammar-decoded circuit. Lean proves an explicit all-input degree-five runtime polynomial, a quadratic output-size bound, compiled polynomial-time machine and function witnesses, exact leaf RawRefinement, and composition with the strict parser computing buildLockedNANDInstance. The audit covers 3,295 declarations: 2,224 have empty closure, 429 use only propext, and 642 use only propext and Quot.sound.
Boundary: The standalone emitter deliberately accepts grammar-valid circuits with intrinsically invalid references; parser composition supplies strict failure. The downstream reduction packages that strict composition, but this emitter alone does not discharge the abstract threshold assumption, establish CNF-SAT NP-completeness or in P, transport NP-hardness, or prove P = NP.
The parser/emitter composition is packaged as a concrete polynomial many-one reduction from EncodedNANDSAT to EncodedLockedNANDThreshold. Five reviewed theorems prove exact function identity, exact output, all-bitstring language equivalence, the ReducesTo witness, and recursive raw-machine refinement. The complete 16-declaration audit uses only propext and Quot.sound, with no project axiom or Classical.choice.
Boundary: The downstream all-input CNF compiler now identifies CNFSAT with this source language through a fixed finite machine and composes with this reduction. This milestone does not discharge the abstract target-language assumption, prove the report-level threshold theorem, put CNF-SAT in P, complete ZeroSlack, or prove P = NP.
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. Eighteen reviewed theorem types pass the expanded 68-declaration audit; 28 declarations have empty closure, 19 use only propext, and 21 use only propext and Quot.sound.
Boundary: This is the pure semantic and size-bound layer; the following all-input milestone supplies the finite-machine and reduction interfaces. Neither layer decides CNF-SAT, puts it in deterministic polynomial time, discharges the abstract threshold premise, completes ZeroSlack/PCCMin, or proves P = NP.
One fixed 135,070-rule three-node parser/carrier/controller work graph halts on every bitstring, rejects malformed CNF words with empty output, and emits exactly the verified NAND encoding for every valid source. Lean proves one external polynomial runtime, a non-timeout PolynomialTimeFunction, literal RawRefinement, a direct PolynomialReduction from CNFSAT to EncodedNANDSAT, and composition to EncodedLockedNANDThreshold. The complete 1,316-declaration audit has 864 empty, 151 propext-only, and 301 propext plus Quot.sound closures, with no project axiom or Classical.choice.
Boundary: This syntax-directed compiler does not decide CNF-SAT, establish SAT NP-hardness or CNF-SAT NP-completeness, discharge the abstract report-level threshold premise, put CNF-SAT in P, complete residual minimization or ZeroSlack/PCCMin, or prove P = NP.
A proof-bearing six-premise candidate boundary for an arbitrary satisfiable proposition.
Boundary: The premises are not instantiated by a uniform polynomial-time SAT-to-locked-NAND reduction.
Executable strict-gain search over a caller-supplied finite implementation list.
Boundary: Unresolved excludes no gain outside the supplied list and cannot imply ZeroSlack.
Every finite proof-bearing or executably accepted chain of adjacent strict equivalent gains preserves complete semantics and the exhaustive reference minimum. The endpoint residual slack plus the chain length is at most the starting residual slack; for the complete locked-NAND candidate, every accepted chain therefore has at most four steps. Twelve generic declarations are axiom-free, and the four locked specializations use only propext and Quot.sound.
Boundary: This validates and bounds a disclosed chain. It does not find gains, prove route or list completeness, justify stopping early, construct ZeroSlack, compute an exact minimizer, prove polynomial checker or PCCMin runtime, put SAT in P, discharge an assumption, or prove P = NP.
For every finite direct-wire implementation, positive residual slack is equivalent to the existence of a smaller semantically equivalent implementation. Zero slack and semantic minimality are each equivalent to the 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. All ten reviewed theorem pins and all twelve public declarations are axiom-free.
Boundary: This uses the exhaustive reference minimum as a semantic witness and requires a proof over every finite implementation. It is not a stopping algorithm, finite-search completeness theorem, gain generator, ZeroSlack certificate, polynomial PCCMin runtime result, project-assumption discharge, or P = NP theorem.
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 equals the exhaustive reference minimum. Positive residual slack is equivalent to a cheaper whole-span full realization, each such realization strictly lowers residual slack, and zero slack is equivalent to the absence of one. All thirteen reviewed theorem pins and all twenty-two audited public declarations are axiom-free.
Boundary: This is the direct-wire terminal full-mode specialization. It does not formalize the quotient carrier or quotient-to-full firewall, proper or governed supports, support saturation, BCEL/BN2–BN6, packet or selector completeness, route generation, ZeroSlack, PCCMin, polynomial minimum search or checking, SAT in P, assumption discharge, or P = NP.
For every finite direct-wire implementation, a computed profile records ten terminal carrier roles and an explicit forgetful projection selects 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; keeping all coordinates lifts directly, and obligation discharge transports across a checked lift. All twelve reviewed theorem pins and all twenty-nine audited public declarations are axiom-free.
Boundary: This is a terminal comparison and 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, PCCMin exactness or polynomial runtime, SAT-in-P result, assumption discharge, or P = NP.
For every finite direct-wire implementation, computed terminal profile, and explicit forgetful projection, exhaustive scans through the current gate count compute attained full-profile and quotient-profile minima. Both minima universally lower-bound every matching realization, projection cannot increase the minimum, and the full minimum is the quotient minimum plus a nonnegative defect. The defect is zero exactly when an attained quotient minimum has a checked full lift. Fourteen reviewed theorem pins cover the milestone; all twenty-seven public declarations use only the permitted propext closure or no axioms.
Boundary: These are exhaustive finite reference minima, not a polynomial-time minimizer. This does not construct proper or governed supports, an arbitrary manuscript quotient carrier, saturation, ZeroSlack, PCCMin, a SAT-in-P result, assumption discharge, or P = NP.
For four supplied terminal-profile corners sharing one observer and one projection, signed full and quotient minimum deltas obey the exact Section 5.2 transfer identity. Lean also proves that when the meet and both side defects are zero and the join defect is D, the projection excess equals D and is positive whenever D is positive. The four reviewed pins are terminalProjectionDefect_int, TerminalProjectionFourCorners.transferIdentity, TerminalProjectionFourCorners.constantCutEquation_of_defects, and TerminalProjectionFourCorners.projectionExcess_pos_of_constantCut; they use only permitted Lean-standard closure.
Boundary: This is signed arithmetic over supplied corners. It does not construct or certify the proper governed support square, prove saturation, complete ZeroSlack or PCCMin, establish polynomial runtime, discharge an assumption, or prove P = NP.
For every finite terminal primitive-record universe and every explicitly supplied Boolean dependency system tagged by the manuscript's ten closure mechanisms, terminalSaturate_closed proves that the generated reflexive transitive closure is dependency-closed, while companion theorems prove that it contains the seed. It is the least closed superset, is monotone and idempotent, and fixes exactly the already closed supports. Seven reviewed theorem pins and all eighteen public declarations use only the permitted Lean-standard closure; fifteen declarations are axiom-free and three use propext with Quot.sound.
Boundary: This theorem does not derive dependencies 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, discharge an assumption, or prove P = NP.
For every finite direct-wire candidate, explicit terminal dependency system, and finite seed list, mem_terminalSaturateRecords_iff proves that a deterministic finite work list computes exactly the inductive saturation. completeTerminalPhysicalSupport_incoming_complete and completeTerminalPhysicalSupport_outgoing_complete prove that the actual program computes canonically ordered incoming boundary and outgoing interface wires; every crossing wire appears on the correct side, no unrelated wire appears, and the composed physical support is compatible. Fourteen reviewed theorem pins and all thirty-five audited public declarations use only the permitted Lean-standard closure; eight declarations are axiom-free, twenty-four use only propext, and three use propext with Quot.sound.
Boundary: The dependency system remains explicit input rather than an extracted profile frontier. This 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, complete ZeroSlack or PCCMin, establish polynomial runtime, discharge an assumption, or prove P = NP.
For every finite direct-wire candidate and finite terminal record list, including noncontiguous selections, extractTerminalSupport_semantics proves that the actual extracted candidate equals an independently defined open-support function for every boundary valuation. extractTerminalSupport_induced recovers the original interface values on whole-circuit-induced boundaries, and the construction composes with executable terminal saturation. Twenty-one reviewed theorem pins and all thirty-four audited public interfaces use only the permitted Lean-standard closure; three declarations are axiom-free, eleven use only propext, and twenty use propext with Quot.sound.
Boundary: The record list and dependency system remain explicit inputs rather than the manuscript’s derived profile frontier. This does not construct 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, complete ZeroSlack or PCCMin, establish polynomial runtime, discharge an assumption, or prove P = NP.
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 absence of such a seed. All twenty-two reviewed theorem pins use only the permitted Lean-standard closure; the thirty-seven-declaration audit contains six axiom-free declarations, three using only propext, and twenty-eight using propext with Quot.sound.
Boundary: The dependency system remains explicit input rather than a frontier derived from the circuit, and the search is exhaustive rather than polynomial. This does not prove global gain completeness, the manuscript's full support completion or square legitimacy, ZeroSlack, PCCMin, SAT in P, assumption discharge, or P = NP.
For every finite direct-wire candidate, explicit terminal dependency system, and pair of finite terminal seeds, Lean computes saturated left and right supports, their canonical closed meet, and their closed saturated-union join. It proves the exact greatest-lower-bound and least-upper-bound laws, seed extensionality, physical compatibility, exact gate count, open-support semantics, and whole-circuit recovery for all four corners. All twenty-three reviewed theorem pins use only the permitted Lean-standard closure; the forty-declaration audit contains six axiom-free declarations, thirteen using only propext, and twenty-one using propext with Quot.sound.
Boundary: The dependency system remains explicit input rather than a profile frontier derived from the circuit. This finite closed-corner algebra is not the manuscript's obstruction routing, frontier pushout, projection-compatible square, side-tight four-corner minima, BN2 square legitimacy, SaturatePositive, complete residual routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
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. All twenty-six reviewed theorem pins use only the permitted Lean-standard closure; the forty-two-declaration audit contains nine axiom-free declarations, twenty-six using only propext, and seven using propext with Quot.sound.
Boundary: The dependency system remains explicit input rather than a profile frontier derived from the circuit. This governed finite completion is not obstruction routing, frontier pushout, the manuscript's projection-compatible square, side-tight minima, square legitimacy, SaturatePositive, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
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. All twenty-eight reviewed theorem pins use only the permitted Lean-standard closure; the thirty-nine-declaration audit contains four axiom-free declarations, twenty-two using only propext, and thirteen using propext with Quot.sound.
Boundary: The dependency system remains explicit input rather than a profile frontier derived from the circuit. This exact gluing result is not projection compatibility, side-tight four-corner minima, square legitimacy, SaturatePositive, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
For every finite direct-wire candidate, explicit terminal dependency system, computed saturated support square, and forgetful terminal projection, Lean retains the exact physical frontier, filters all ten role profiles exactly, and proves that projection commutes with both the shared meet and the side-only frontier pushout. All twenty-three reviewed theorem pins use only the permitted Lean-standard closure; the thirty-three-declaration audit contains six axiom-free declarations, twenty-one using only propext, and six using propext with Quot.sound.
Boundary: The dependency system remains explicit input rather than a profile frontier derived from the circuit. This structural commutation result is not side-tight four-corner minima, square legitimacy, SaturatePositive, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
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 existing delta only when meet, left, right, and join all attain their exact minima; both canonical independently attained minimum bases pass. All twenty-four reviewed theorem pins use only the permitted Lean-standard closure. The forty-three-declaration audit contains nineteen axiom-free declarations, seventeen using only propext, and seven using propext with Quot.sound.
Boundary: The canonical corner minima are independently attained. This numerical result does not construct one coherent four-corner basis, coherent completion, maximization over a finite tight family, square legitimacy, SaturatePositive, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
For every finite computed saturated terminal support square, direct-wire candidate, and forgetful terminal projection, Lean places the meet, left, right, and join endpoints in common ambient coordinates. It proves duplicate-free boundary, interface, and profile lists, transports the meet and join profiles exactly, and classifies every present side physical coordinate as retained or constructively internalized through fail-closed queries. All twenty-seven reviewed theorem pins use only the permitted Lean-standard closure. The thirty-eight-declaration audit contains five axiom-free declarations, twelve using only propext, and twenty-one using propext with Quot.sound.
Boundary: This is a structural carrier for computed corners. It does not transport four optimum realizers, construct a coherent four-corner optimum, prove coherent completion or square legitimacy, establish SaturatePositive, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
For every finite computed saturated terminal support square and every explicit observer, Lean embeds all four exact corner candidates into one common ambient carrier. It proves reversible semantic and gate-count preservation, exact agreement between ambient and corner reference minima, and localization of canonical full and quotient optima from one shared observer and projection without changing their exact minimum counts. All thirty reviewed theorem pins use only the permitted Lean-standard closure. The fifty-seven-declaration audit contains thirteen axiom-free declarations, five using only propext, and thirty-nine using propext with Quot.sound.
Boundary: The full and quotient optima are independently attained. This result does not prove coherent transport along the square legs, construct a coherent four-corner optimum, prove side-tight completion or square legitimacy, derive the terminal dependency system, establish SaturatePositive, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
For every finite computed terminal support square, explicit observer, terminal projection, and full or quotient mode, Lean checks the four square legs in a deterministic order. It returns either one coherent canonical optimum tuple with exact transport, side-tight, and incidence facts, or the exact first open-obligation, semantic, profile, charge-profile, or mode mismatch. All nineteen reviewed theorem pins use only the permitted Lean-standard closure. The thirty-seven-declaration audit contains twelve axiom-free declarations, three using only propext, and twenty-two using propext with Quot.sound.
Boundary: This is a coherence-or-first-failure classifier. It does not prove that every square is coherent, construct the later no-outcome route, prove sideTightCompletionExists or BN2 square legitimacy, establish SaturatePositive, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
For every finite computed terminal support square, explicit observer, and full or quotient mode, the first local coherence query now returns either a proof-bearing sound route or the complete checked side-tight coherent optimum tuple when there is computed local route silence. The completed tuple retains the exact minimum incidence value, while quotient promotion remains behind its own firewall. All twenty reviewed theorem pins use only the permitted Lean-standard closure. The twenty-eight-declaration audit contains two axiom-free declarations, two using only propext, and twenty-four using propext with Quot.sound.
Boundary: This is conditional local completion. 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 the complete tight-basis family, establish SaturatePositive, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
For every finite computed terminal support square, explicit observer, and full or quotient mode, Lean enumerates every exact profile-constrained minimum implementation at each corner, crosses the complete four-corner family, filters it with the arbitrary-family coherence query, and proves under exact local route silence that the signed maximum equals the selected delta. All twenty-eight reviewed theorem pins use only the permitted Lean-standard closure. The forty-five-declaration audit contains twelve axiom-free declarations, five using only propext, and twenty-eight using propext with Quot.sound.
Boundary: This is a local all-finite maximum under computed 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, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
For every square computed 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. It keeps full and quotient minimum quantities on the same carrier and returns either the complete local conclusion under exact route silence or the deterministic full-then-quotient proof-bearing first route. All twenty reviewed theorem pins use only propext with Quot.sound; the focused audit covers fifteen new declarations.
Boundary: This result does not derive the 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, complete obstruction routing, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
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 enumerates every positive anchor subfamily and selects the canonical minimum-cardinality nucleus. It then returns an insufficient nucleus, the exact first anchor-algebra mismatch, the exact first proper-cut defect mismatch, the first proof-bearing full-before-quotient route, or exact constant-cut and local BN2 conclusions for every proper cut. Thirty-six reviewed theorem pins use only the permitted Lean-standard closure. The focused 79-declaration audit has 7 empty closures, 8 using only propext, and 64 using propext with Quot.sound.
Boundary: The positive whole-support projection defect and terminal dependency system are explicit premises. This result does not derive either premise, identify the manuscript's activation or charge classes, connect a local failure to the complete global route system, establish SaturatePositive, Package E, BCELReady, ZeroSlack, PCCMin, polynomial runtime, SAT in P, assumption discharge, or P = NP.
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 projection defect. Zero returns an attained quotient minimum with a checked full lift, while positive delegates exactly to the existing fail-closed BCEL anchor-nucleus classifier. Twelve reviewed theorem pins use only the permitted Lean-standard closure. The focused 20-declaration audit has 1 empty closure, 4 using only propext, and 15 using propext with Quot.sound.
Boundary: This closes only projectionPositivityNotLostSilently in the current finite terminal model. The dependency system and governed proper-positive support remain explicit premises. This result 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; discharge an assumption; or prove P = NP.
For every finite direct-wire candidate, executable observer, forgetful projection, and finite seed, Lean derives the physical and context-sensitive dependency system and computes a deterministic rule-labelled saturation trace. It proves exact support and full-circuit cost balance with preserved slack, positivity, and nondecreasing projection defect throughout a transparent history, or records the exact first nontransparent event and complete transparent prefix. Seventeen reviewed theorem pins use only the permitted Lean-standard closure. The focused 53-declaration audit has 10 empty closures, 6 using only propext, and 37 using propext with Quot.sound.
Boundary: This closes only the finite terminal forms of transparentSaturationCostBalanced and firstNontransparentStepRecorded. The observer and projection remain explicit inputs, and a nontransparent event is recorded rather than routed. It does not discharge interfaceExposureRoutesToE or originKernelObligationClosureRouted, establish full SaturatePositive, Package E or BCELReady, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, discharge an assumption, or prove P = NP.
For every finite direct-wire candidate, executable observer, forgetful projection, and finite seed, Lean recognizes only an exact candidate-derived interface-consumer edge. It proves each recognized event transparently cost-balanced or produces a proof-bearing local E-route, then records the exact first interface-exposure event and complete transparent prefix. Ten reviewed theorem pins use only the permitted Lean-standard closure. The focused 28-declaration audit has 2 empty closures, 1 using only propext, and 25 using propext with Quot.sound.
Boundary: This closes only the finite local form of interfaceExposureRoutesToE. The local E-route is an exposure-obligation coordinate, not a full Package E acceptance, verified global gain, or global route-completeness theorem. The observer and projection remain explicit inputs. It does not discharge originKernelObligationClosureRouted, establish full SaturatePositive, Package E or BCELReady, prove ZeroSlack, PCCMin, polynomial runtime, SAT in P, discharge an assumption, or prove P = NP.
For every finite direct-wire candidate, executable 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 and profile orientations. It checks cost transparency, obligation discharge, and forgotten-profile stability, then 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. Nine reviewed theorem pins use only the permitted Lean-standard closure. The focused 37-declaration audit has 7 empty closures, 1 using only propext, and 29 using propext with Quot.sound.
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. The positive initial full-slack premise remains explicit. It does not establish manuscript-wide SaturatePositive, BCELReady, RankWF, ZeroSlack, PCCMin, polynomial runtime, SAT in P, discharge an assumption, or prove P = NP.
Lean defines the residual terminal rank as exactly ten natural-number coordinates in the manuscript priority order. It proves that the executable Boolean comparison agrees with the lexicographic proposition, supplies all ten first-decreasing-coordinate witnesses, packages proof-bearing descent, and proves accessibility, induction, and kernel-checked well-foundedness. Eighteen reviewed theorem pins use only the permitted Lean-standard closure. The focused 39-declaration audit has 37 empty closures and 2 using only propext.
Boundary: This establishes the fixed rank domain and RankWF only. It does not map the current finite terminal routes into the complete global outcome system, prove that any existing route strictly decreases the rank, establish route completeness or Package E, remove the finite composition's explicit positive premise, establish manuscript-wide SaturatePositive or BCELReady, prove ZeroSlack or PCCMin, establish polynomial runtime, put SAT in P, discharge an assumption, or prove P = NP.
After the computed finite BCEL anchor-nucleus classifier succeeds, Lean enumerates every proper cut and constructs one canonical duplicate-free request-identity list. Executable request membership is exact, monotone, and stable; minimal consumers are exact singletons; active incidence is duplicate-free; and one canonical full-or-quotient side-tight basis family is selected jointly across all cuts. Eleven reviewed theorem pins use only the permitted Lean-standard closure. The focused 84-declaration audit has 8 empty closures, 3 using only propext, and 73 using propext with Quot.sound.
Boundary: This is an exact finite reference construction after a successful nucleus, but it enumerates all subsets and can take exponential time. It does not derive the dependency system, construct BN4 through BN6, map every residual route into a decreasing complete global outcome system, prove selector or realizer completeness, establish global ZeroSlack or polynomial PCCMin, put SAT in P, discharge an assumption, or prove P = NP.
After the finite BN3 classifier succeeds, Lean gives every request atom a canonical singleton activation code, checks a complete typed key, totals positive and negative natural mass only at the same key, and returns a canonical balanced, positive, or negative residual. Thirteen reviewed theorem pins prove exact integer mass conservation, preserved key identity, positive residual mass, no opposite-sign residual pair, duplicate-free ledger keys, and fail-closed wrapper behavior. The focused 33-declaration audit has 11 empty closures, 6 using only propext, and 16 using propext with Quot.sound.
Boundary: The cell ledger, semantic signatures, and transport types are explicit inputs rather than derived from the four-corner bases. This is not the full historical BN4 theorem, has no polynomial construction or size bound, and does not construct PkgC or BN6; complete global routes, selectors, or realizers; global ZeroSlack or polynomial PCCMin; SAT in P; assumption discharge; or P = NP.
Starting from an explicit negative BN4 cancellation result, payload list, cut, and quotient-shadow ledger, Lean validates exact unit refinement, computes cut silence, and otherwise returns complete multiplicity coverage or a strict Hall deficit. Twelve reviewed theorem pins preserve complete coordinates, prove a literal smaller shadow-neighbour fibre, and route the deficit to local X1 so unmatched active units cannot disappear silently. The focused 40-declaration audit has 23 empty closures, 11 using only propext, and 6 using propext with Quot.sound.
Boundary: The payloads and shadow universe are explicit inputs rather than derived from four-corner bases. Complete matching is not connected back to a BN4 contradiction, and this does not prove the full CritC/Q/E/L/X2/X3/X4 diagnosis or the full historical BN5 theorem. It does not construct PkgC or BN6; complete global routes, selectors, or realizers; polynomial generation or runtime; global ZeroSlack or PCCMin; SAT in P; assumption discharge; or P = NP.
For every explicit finite minimal-consumer antichain, Lean scans in canonical order for the first disjoint pair that is not singleton-singleton. No pair is exactly V54's singletonization premise. A found pair's atoms become canonical exact-coordinate quotient units, and an explicit finite full-restoration universe is classified into complete multiplicity coverage or a strict Hall deficit with a deterministic local Q route. Every restoration edge preserves the full coordinate. The exhaustive classifier is PNP.DirectWire.classifyTerminalPkgCSeparatingConsumers_exhaustive. Nine reviewed theorem pins use only permitted Lean-standard closure. The focused 27-declaration audit has 11 empty closures, 6 using only propext, and 10 using propext with Quot.sound.
Boundary: The consumer antichain and restoration universe remain explicit inputs. Complete coverage is not connected back to a BN4 or BN5 contradiction, and the local Hall route is not embedded in the complete global outcome system. This does not prove full PkgC route silence or the full historical PkgC theorem, derive the inputs from terminal candidates, complete BN6 or Packet selector and realizer results, prove polynomial generation or runtime, global ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
For every explicit finite minimal-consumer antichain and typed coordinate-preserving restoration operation, Lean materializes one full-restoration candidate for every atom of the canonical first disjoint nonsingleton pair. It proves the exact candidate count, positional coordinate preservation, exact full and shadow equality-fibre multiplicities, complete coverage, and that the resulting graph cannot have a strict Hall deficit. If no such pair exists, the total classifier proves exactly V54 singletonization. The exhaustive classifier is PNP.DirectWire.classifyTerminalPkgCTypedRestoration_exhaustive. Nine reviewed theorem pins use only permitted Lean-standard closure. The focused 17-declaration audit has 7 empty closures, 3 using only propext, and 7 using propext with Quot.sound.
Boundary: The typed restoration operation remains explicit caller data. This result does not construct it from a terminal candidate or prove its full semantic adequacy, 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, complete BN6 or Packet selector and realizer results, prove polynomial generation or runtime, global ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
For every atom of the canonical first disjoint nonsingleton pair, Lean constructs a positive unit cell for the quotient atom and a negative unit cell for its typed restored candidate. Exact preservation of the complete BN5 coordinate proves that both cells have the same nested BN4 key. Lean proves the exact cell count, equal positive and negative multiplicity at every key, an empty computed residual, and zero signed mass. The exhaustive classifier PNP.DirectWire.classifyTerminalPkgCSameKeyCancellation_exhaustive returns either exact V54 singletonization or a proof-bearing cancellation realization; exact absence of every such outcome forces singletonization. Eleven reviewed theorem pins use only permitted Lean-standard closure. The focused 21-declaration audit has 4 empty closures, 5 using only propext, and 12 using propext with Quot.sound.
Boundary: The typed restoration operation and complete coordinate maps remain explicit inputs, and the generated opposite-sign cells are not yet proved to be the terminal candidate's ambient BN4 ledger. This result does not construct semantic restorations from terminal data, embed cancellation or Hall outcomes into the complete global route system, prove global route silence or the full historical PkgC theorem, complete BN6 or Packet selector-realizer results, prove polynomial generation or runtime, global ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
For every finite carrier and explicit antichain of minimal consumers, Lean proves request monotonicity, empty-request inactivity, and that nonzero two-sided cut activation is equivalent to a disjoint consumer pair. Under the exact premise that every disjoint pair is singletonized, it proves literal equality with the cut indicator of the singleton footprint in PNP.DirectWire.terminalV54_consumerAntichain_normal_form. Seven reviewed theorem pins use only permitted Lean-standard closure. The focused 28-declaration audit has 11 empty closures, 9 using only propext, and 8 using propext with Quot.sound.
Boundary: The theorem itself consumes an explicit minimal-consumer antichain. The finite BN6 bridge transports explicitly grouped instances into V53, and the new PkgC classifier proves singletonization when no separating pair exists, but this does not complete PkgC construction or route silence, derive or group inputs from terminal candidates, 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.
For an arbitrary finite duplicate-free carrier and sparse nonnegative weighted hypergraph with positive listed cells, Lean proves the complete classification forced by one common positive value on every nonempty proper cut. With two anchors, the full-span weight is the cut value. With three anchors, all pair weights agree at one value and full-span weight plus twice that value is the cut value. With four or more anchors, every proper footprint has zero weight and the full-span weight is the cut value. The main theorem is PNP.DirectWire.terminalV53_constantCut_hypergraph_rigidity. Ten reviewed theorem pins use only permitted Lean-standard closure. The focused 58-declaration audit has 9 empty closures, 18 using only propext, and 31 using propext with Quot.sound.
Boundary: The finite BN6 bridge now constructs this hypergraph and cut equation from explicit grouped V54 cells and retains payload witnesses, but full PkgC construction and route silence, terminal-candidate derivation and grouping, the full historical BN6 and Packet selector and realizer results, global routes, polynomial runtime, ZeroSlack, PCCMin, SAT in P, removal of a project assumption, and P = NP remain unproved.
For an arbitrary finite duplicate-free anchor carrier and explicit already-grouped positive payload-bearing survivor cells, Lean transports V54 activation exactly into the constructed V53 hypergraph cut sum. A supplied common positive value on every nonempty proper cut then yields the pair, mixed three-anchor balanced-triple or full-span, or four-or-more-anchor full-span classification, together with witnesses back to the original payloads. The main theorem is PNP.DirectWire.terminalBN6_hypergraph_packet. Eight reviewed theorem pins use only permitted Lean-standard closure. The focused 21-declaration audit has 4 empty closures, 6 using only propext, and 11 using propext with Quot.sound.
Boundary: The survivor family, grouping, positive atom ledger, payload data, PkgC singletonization proofs, and BCEL constant-cut equation are explicit inputs. This result does not complete PkgC or route silence, derive or group survivors from a terminal candidate, establish the full historical BN6 or Packet selector and realizer results, complete global routes, prove polynomial generation or runtime, ZeroSlack or PCCMin, put SAT in P, remove a project assumption, or prove P = NP.
PNP.Main.locked_nand_threshold packages the composed finite parser, compiler, and emitter as a uniform all-bitstring polynomial reduction from CNFSAT to EncodedLockedNANDThreshold. Its one reviewed theorem pin uses only Quot.sound and propext.
Boundary: This is a many-one reduction, not a polynomial-time target decider, a CNF-SAT NP-hardness or NP-completeness theorem, a ZeroSlack or PCCMin result, activation of the legacy string-handle bridge, or P = NP.
For arbitrary finite explicit BN4 cell ledgers, a proof-bearing exact multiset decomposition identifies the generated PkgC opposite-sign cancellation cells 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 candidate-derived BN4 kernel proves every embedded generated cell uses its canonical request-atom space. The theorem PNP.DirectWire.terminalPkgC_computedAmbientBN4_silence_singletonizes proves that complete bindings plus exact absence of every computed bridge imply V54 singletonization. Twelve reviewed theorem pins use only permitted Lean-standard closure. The focused 17-declaration audit has 4 empty closures, 5 using only propext, and 8 using propext with Quot.sound.
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 does not derive them from a terminal candidate, prove the restorer's semantic adequacy, embed local outcomes into the complete global route system, prove global PkgC route silence or the full historical PkgC theorem, establish polynomial runtime, global ZeroSlack or PCCMin, put SAT in P, discharge an assumption, or prove P = NP.
Complete residual routing, global ZeroSlack contradiction, exact minimization, and polynomial bounds.
Boundary: The finite BN3 envelope supplies stable request identities, the finite BN4 kernel supplies exact same-key integer cancellation, the finite BN5 kernel localizes explicit multiplicity failure to a strict Hall deficit and local X1 route, and the finite PkgC classifiers return exact singletonization, a local-Q restoration dichotomy, typed complete restoration coverage with no Hall deficit, and proof-bearing same-key cancellation with an empty residual. V54 proves an exact consumer-antichain normal form under explicit inputs, V53 classifies any explicit finite constant-cut hypergraph, and the finite BN6 bridge transports explicit grouped survivors into that classification with payload witnesses. The construction still does not derive the BN4 ledger, BN5 payload and shadow universe, PkgC antichain, typed restoration operation, or coordinate maps from terminal candidates; derive the ambient BN4 ledger, typed restorer, exact embedding certificate, or successful candidate kernel from the terminal candidate; derive the V54 antichain and singletonization premise or the BN6 survivor family, grouping, payloads, and constant-cut equation; connect matching or cancellation back to a contradiction; establish the full historical BN4, BN5, PkgC, BN6, or Packet selector and realizer results; complete decreasing global routing; establish global ZeroSlack; or prove polynomial PCCMin.
Raw-machine-linked complexity classes, concrete SAT completeness and a SAT decider, plus the publication root theorem.
Boundary: The concrete target definition is inactive; raw-machine linkage, concrete SAT completeness/deciding, and PNP.Main.p_eq_np remain absent. The legacy string-handle bridge is ineligible.
| Gate input | Current result | Why publication stays closed |
|---|---|---|
| Concrete standard-model target | present, inactive | PNP.Main.ConcretePEqualsNP is an axiom-free definition, not a proof. Raw-machine eligibility is established, but the required CNF-SAT theorems are absent. |
| Compatibility root theorem | false | PNP.Main.p_eq_np is absent. |
| Reviewed kernel fingerprints | unconfigured | Expected target/root/closure fingerprints are null; null never matches null. |
| Axiom closure | false | No eligible root exists to audit against the immutable Lean-standard allowlist. |
| Abstract bridge eligibility | false | The string-handle PNP.PEqualsNP definition is explicitly ineligible. |
| Strict conjunction | passed = false | Theorem statement, conclusion, establishment, and emission fields derive only from this gate. |
Formal.ConcreteSATFormal.ResidualBandMinimizerFormal.ZeroSlackFormal.PolynomialRuntimeAndCertificateBoundsFormal.RootTheoremAndAxiomAuditPNP.CheckPCCPackexpPNP.GeneratePCCPackPNP.LockedNANDThresholdPNP.ResidualBandExactMinimizationNo site wording, report digest, Boolean/string field, JavaScript checker acceptance, historical activation record, or review status clears these obligations.
The canonical download is generated from the compiled theorem inventory. It reports the earned CNF-SAT NP-membership, raw-machine compiler, Cook-Levin semantic bridge and bounded builder prefix, concrete locked-NAND reductions, the verified residual and terminal-support chain through computed BN2 square legitimacy, the canonical positive BCEL anchor nucleus, candidate-derived saturation and finite routing, the fixed residual RankWF, the exact finite BN3 request envelope, the finite BN4 cancellation kernel, the finite BN5 full-shadow localization kernel, the finite PkgC separating-consumer restoration dichotomy, typed restoration realization, same-key cancellation classifier, and ambient-BN4-ledger embedding, the V54 consumer-antichain normal form, the V53 constant-cut hypergraph rigidity classification, and the finite BN6 grouped hypergraph-packet bridge, together with the closed gate, exact counts, axiom closures, assumptions, and blockers.
The old direct-claim manuscript is preserved at tag final-pnp-proof-report-hardened-7072f8d, commit 7072f8d0bda6d44d240f9bb3fad624fd357e1278, with provenance in archive/legacy-v0/ARCHIVE.json. It is not current authority.