IndisputableMonolith.Complexity.SpectralGap
The SpectralGap module defines variance of real functions on the Boolean hypercube, convergence rates, UNSAT gap conditions, and spectral gap certificates built on the J-cost Laplacian. Complexity researchers working on Recognition Science encodings for SAT cite these objects when assembling topological obstruction arguments. The module supplies supporting definitions and elementary lemmas that connect the weighted hypercube graph to positive gaps for unsatisfiable instances.
claimFor $f : (Fin n → Bool) → ℝ$, variance is $Var(f) := E[f^2] - (E[f])^2$. For a CNF formula φ, the J-cost Laplacian has edge weights |satJCost(φ,a) - satJCost(φ,a')|; SpectralGapCert asserts a positive lower bound on the gap when φ is unsatisfiable.
background
The module sits inside the Recognition Science treatment of complexity. It imports the J-cost Laplacian, which equips the Boolean hypercube with edge weights given by absolute differences in satJCost, and the RSatEncoding that links satisfiability to J-cost landscapes. Constants supplies the base time quantum τ₀ = 1 tick. Variance is introduced as the variance of a real-valued function on {0,1}^n; related objects include ConvergenceRate, iteration_bound_from_clauses, empty_formula_flat_landscape, UNSATGapCondition, and SpectralGapCert.
proof idea
This is a definition module, no proofs. It assembles the listed sibling definitions and the elementary lemmas variance_nonneg, variance_const_zero, unsat_has_positive_gap, and spectralGapCert from the imported JCostLaplacian and RSatEncoding structures.
why it matters in Recognition Science
The module supplies the gap and variance machinery required by PvsNPAssembly for the conditional P ≠ NP path that relies on UniformTopologicalObstructionHyp and J-frustration lower bounds. It also feeds Core.Complexity. The constructions directly support the claim that unsatisfiable formulas carry a positive spectral gap on the J-cost Laplacian.
scope and limits
- Does not prove P ≠ NP outright.
- Does not compute numerical gap values for concrete formulas.
- Does not address circuit-size lower bounds directly.
- Does not treat the natural-proofs barrier.