SpectralGapCert
plain-language theorem explainer
SpectralGapCert bundles the non-negativity of variance for any real-valued function on the n-dimensional hypercube with the vanishing of J-cost edge weights on the empty CNF formula. Researchers assembling the Recognition Science P versus NP dissolution cite it when constructing the master certificate that separates SAT convergence from UNSAT obstruction. The declaration is a pure structure definition that records these two properties without computational content or proof steps.
Claim. A spectral gap certificate consists of the assertions that the variance of every function $x : (Fin n → Bool) → ℝ$ satisfies $0 ≤ Var(x)$ and that the J-cost edge weight of the empty formula satisfies $w_J(⟨[], n, rfl⟩, a, k) = 0$ for every assignment $a$ and coordinate $k$.
background
The module develops the spectral gap of the J-cost Laplacian, where the gap λ₂ governs the geometric convergence rate of gradient descent on the satJCost landscape. Variance is the sum over all 2^n assignments of the squared deviation from the mean value of x. jcostEdgeWeight returns the absolute change in satJCost after flipping one bit. CNFFormula encodes a list of clauses together with a verified variable count. The empty formula is the base case whose landscape is completely flat.
proof idea
The declaration is a structure definition. It is populated by the one-line wrapper spectralGapCert, which supplies variance_nonneg_cert from the sibling lemma variance_nonneg and flat_empty from the sibling lemma empty_formula_flat_landscape.
why it matters
SpectralGapCert supplies the spectral component of both PneqNPConditional and PvsNPMasterCert in the P versus NP assembly. It establishes the zero-gap base case for the empty formula that is required before the positive-gap obstruction for unsatisfiable formulas can be stated. The construction directly supports the claim that R̂ converges in linear steps on satisfiable instances while UNSAT instances remain separated by a positive J-cost gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.