PneqNPConditional
plain-language theorem explainer
PneqNPConditional packages the six certificates spanning J-cost positivity, spectral gap, frustration depth, natural-proof bypass, uniform obstruction hypothesis, and algebraic circuit lower bounds into one conditional package for the P versus NP separation. A complexity theorist would cite it when invoking the full three-phase argument that high J-frustration on unsatisfiable formulas forces super-polynomial circuit size once the topological obstruction is granted. The declaration is realized as a record definition that simply aggregates the上游
Claim. A structure bundling six certificates: the J-cost Laplacian form is positive semidefinite with constants in its kernel; the spectral gap is positive on unsatisfiable formulas; J-frustration is at least 1 on unsatisfiable formulas and zero on satisfiable ones; high-depth properties are non-natural; the uniform topological obstruction supplies a fixed-exponent exponential circuit-size lower bound; and algebraic restrictions imply linear lower bounds on deciding circuits for unsatisfiable formulas.
background
The module presents two resolution paths for P versus NP. Path A is conditional on the uniform topological obstruction hypothesis: J-frustration is non-natural (Phase 2), unsatisfiable formulas carry J-frustration at least 1 (Phase 1), and high frustration forces exponential circuit size (Phase 3). Path B is the unconditional dissolution route that separates recognition time from Turing-machine overhead. JCostLaplacianCert asserts positive-semidefiniteness and constant kernel of the J-cost form. SpectralGapCert extracts a positive gap from the unsatisfiability condition. JFrustrationCert states that landscape depth is at least 1 for unsatisfiable formulas. NonNaturalnessCert proves that high-depth properties cannot be natural. UniformTopologicalObstructionHyp supplies the uniform exponential bound. CircuitLowerBoundCert gives the algebraic restriction implying linear size lower bounds.
proof idea
The declaration is a structure definition that packages the six upstream certificates. No derivation occurs inside the structure; each field is supplied directly by the corresponding certificate from JCostLaplacian, SpectralGap, JFrustration, NonNaturalness, CircuitLowerBound, and the obstruction hypothesis.
why it matters
This structure is the sole input to the theorem p_neq_np_assembled, which concludes that under the uniform obstruction no polynomial circuit family decides satisfiability for sufficiently large n. It completes the conditional Path A of the P versus NP assembly, linking J-frustration non-naturalness and lower-bound results to the classical separation. The construction touches the open question of discharging the algebraic restriction hypothesis inside CircuitLowerBoundCert. It aligns with the Recognition Science forcing chain by treating complexity measures through the J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.