pith. sign in
module module high

IndisputableMonolith.Complexity.PvsNPAssembly

show as:
view Lean formalization →

The PvsNPAssembly module completes the Recognition Science P ≠ NP argument by chaining J-frustration non-naturalness to circuit lower bounds, conditional on a topological obstruction in the J-cost landscape for unsatisfiable formulas. Complexity theorists studying natural-proof barriers would cite it as the capstone of the RS program. The module structure is an assembly of eight imports and sibling declarations that link RSatEncoding through CircuitLowerBound without new internal proofs.

claimP ≠ NP holds conditionally on the existence of a non-contractible topological obstruction (positive Betti-1) in the J-cost landscape of unsatisfiable k-CNF formulas, where high J-frustration implies super-polynomial circuit size.

background

The module sits inside the Recognition Science complexity program. It imports definitions of the J-cost Laplacian (weighted graph on the Boolean hypercube with edge weights |satJCost(φ,a) − satJCost(φ,a′)|) and J-frustration (binary measure 0 for SAT, 1 for UNSAT that quantifies topological depth of the landscape barrier). Upstream results establish that J-frustration is non-natural (Razborov-Rudich sense: constructive, large, and useful for circuit lower bounds) and that the R̂ operator reaches zero J-cost in O(n) steps for satisfiable instances but encounters a non-contractible obstruction for unsatisfiable ones.

proof idea

This is an assembly module with no internal proofs. It imports CircuitLedger, CircuitLowerBound, JCostLaplacian, JFrustration, NonNaturalness, RSatEncoding, SpectralGap, and Constants, then exposes sibling declarations (PneqNPConditional, dissolution_holds, currentStatus, pvsNPMasterCert) that combine the imported lemmas into the single conditional claim.

why it matters in Recognition Science

The module feeds the parent theorem in IndisputableMonolith.Core.Complexity. It supplies the complete P ≠ NP argument conditional on the topological obstruction, closing the Recognition Science complexity chain that begins with the R̂ SAT encoding and ends with circuit lower bounds from J-frustration.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (8)