PvsNPMasterCert
plain-language theorem explainer
PvsNPMasterCert assembles seven upstream certificates into one structure that collects the J-cost Laplacian positivity, spectral gap, J-frustration bounds, non-naturalness of high-depth properties, algebraic circuit lower bounds, dissolution argument, and circuit separation for the Recognition Science treatment of P versus NP. A researcher working inside the RS complexity module would cite this structure to invoke the full unconditional dissolution path in a single reference. The declaration is a bare structure definition with no proof steps or
Claim. A master certificate consists of the J-cost Laplacian certificate (positive semi-definiteness of the Laplacian form with constant kernel zero), the spectral gap certificate, the J-frustration certificate (JFrust ≥ 1 on UNSAT formulas and JFrust = 0 on SAT formulas), the non-naturalness certificate (high-depth properties are not natural), the circuit lower bound certificate, the dissolution structure (R̂ recognition in ≤ n steps for SAT, cost ≥ 1 obstruction for UNSAT, local blindness on partial decoders), and the circuit separation structure.
background
The PvsNPAssembly module presents two resolution routes for P versus NP inside Recognition Science. Path B (dissolution) is unconditional and rests on the claim that R̂ recognition decides SAT in linear steps while any circuit must read all inputs. The JCostLaplacianCert supplies the positive semi-definite form and constant kernel used to define cost landscapes. JFrustrationCert supplies the landscape depth lower bound of 1 for UNSAT formulas. NonNaturalnessCert supplies the barrier-bypass theorem that high-depth properties cannot be natural. CircuitLowerBoundCert and CircuitSeparation supply the algebraic restriction and the proved separation between R̂ time and circuit size.
proof idea
This is a structure definition that directly references the seven upstream certificates (JCostLaplacianCert, SpectralGapCert, JFrustrationCert, NonNaturalnessCert, CircuitLowerBoundCert, PvsNPDissolution, CircuitSeparation) with no tactics or lemmas applied.
why it matters
The structure feeds the single downstream definition pvsNPMasterCert and thereby supplies the complete certificate bundle for the unconditional dissolution path (Path B) described in the module documentation. It closes the proved half of the RS position that SAT recognition via R̂ is linear while circuit simulation incurs structural overhead, leaving only the open UniformTopologicalObstructionHyp for the conditional P ≠ NP route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.