pith. sign in
module module high

IndisputableMonolith.Complexity.PvsNPAssembly

show as:
view Lean formalization →

The module assembles the full conditional P ≠ NP argument in Recognition Science from J-frustration, circuit lower bounds, and non-naturalness. Researchers in the RS complexity program cite it as the capstone statement. It composes the imported lemmas on topological obstruction and super-polynomial size into one conditional claim.

claimConditional on a non-contractible topological obstruction (positive Betti-1) in the J-cost landscape of an unsatisfiable k-CNF, no polynomial-size feed-forward Boolean circuit decides SAT.

background

The module sits inside the Complexity domain and imports eight supporting modules. CircuitLedger treats Boolean circuits as restricted sub-ledgers whose size must be compared to the global J-cost gradient used by R̂. JCostLaplacian equips the Boolean hypercube with edge weights given by differences in satJCost. JFrustration defines the binary measure JFrust that equals 1 precisely when the landscape contains a non-contractible barrier. NonNaturalness recalls the Razborov-Rudich criteria that J-frustration satisfies. RSatEncoding supplies the O(n)-step recognition witness for satisfiable instances.

proof idea

The module performs no local proofs; it is an assembly that imports and re-exports the key statements from CircuitLowerBound, JFrustration, NonNaturalness, and RSatEncoding under the single conditional header supplied by the module doc-comment.

why it matters in Recognition Science

It supplies the complete conditional P ≠ NP statement that is imported by Core.Complexity. The assembly closes the RS complexity program whose core claim (high J-frustration implies super-polynomial circuit size) originates in the CircuitLowerBound and JFrustration modules.

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)