pith. sign in
module module high

IndisputableMonolith.Complexity.PvsNPAssembly

show as:
view Lean formalization →

The module assembles the complete conditional argument that P ≠ NP in Recognition Science, given a topological obstruction in the J-cost landscape for unsatisfiable formulas. Complexity theorists studying circuit lower bounds and non-natural proofs would cite it as the capstone of the RS P vs NP program. The structure imports and chains results from J-frustration, circuit lower bounds, and RSatEncoding without introducing new proofs.

claimConditional on a non-contractible topological obstruction (positive Betti-1) in the J-cost landscape of unsatisfiable k-CNF formulas, P ≠ NP.

background

The module sits in the Complexity domain and imports eight supporting modules. RSatEncoding defines the R̂ operator that reaches zero J-cost in O(n) steps for satisfiable instances but encounters a topological obstruction for unsatisfiable ones. JFrustration introduces JFrust as a binary measure (0 for SAT, 1 for UNSAT) that quantifies the depth of the J-cost barrier. NonNaturalness shows that J-frustration satisfies the three Razborov-Rudich conditions for a non-natural property. CircuitLedger and CircuitLowerBound establish that high J-frustration forces super-polynomial circuit size. JCostLaplacian supplies the weighted hypercube graph whose edge weights are differences in satJCost.

proof idea

This is an assembly module, no proofs. It imports CircuitLedger, CircuitLowerBound, JCostLaplacian, JFrustration, NonNaturalness, RSatEncoding, SpectralGap, and Constants, then exposes the combined conditional statement through sibling declarations such as PneqNPConditional and p_neq_np_assembled.

why it matters in Recognition Science

The module feeds the parent result in IndisputableMonolith.Core.Complexity. It completes the Recognition Science P vs NP program by assembling the conditional argument on the topological obstruction, directly matching the module doc-comment. The assembly closes the chain from the R̂ SAT encoding through J-frustration and circuit lower bounds.

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)