IndisputableMonolith.Complexity.SpectralGap
Defines variance for real functions on the Boolean hypercube and derives positive spectral gaps for unsatisfiable CNF formulas via the J-cost weighted Laplacian. Builds convergence rates and gap certificates from the RSatEncoding framework. Supplies the analytic objects consumed by the P versus NP assembly to separate satisfiable and unsatisfiable instances.
claimFor $f : (Fin n) → Bool → ℝ$, variance is $Var(f) := E[f^2] - (E[f])^2$. For unsatisfiable φ the J-cost Laplacian on {0,1}^n has positive spectral gap: λ₂(L_φ) > 0, certified by SpectralGapCert.
background
The module sits inside Recognition Science complexity analysis and imports the J-cost Laplacian, which equips the Boolean hypercube with edge weights |satJCost(φ,a) - satJCost(φ,a')| for Hamming-distance-1 pairs. It also imports the RSatEncoding whose core claim is that satisfiable k-CNF instances reach zero J-cost in O(n) steps while unsatisfiable instances carry a non-contractible topological obstruction (positive Betti-1). Constants supply the base tick τ₀ = 1. The module introduces variance of real functions on {0,1}^n together with non-negativity, zero only for constants, and iteration bounds derived from clause count.
proof idea
This is a definition module. It first defines variance and proves non-negativity plus constancy-zero via direct expansion. It then constructs convergence-rate bounds from the number of clauses, shows the empty formula yields a flat landscape, and finally certifies that every unsatisfiable formula induces a positive gap on the J-cost Laplacian via the SpectralGapCert object.
why it matters in Recognition Science
The module supplies the spectral-gap and variance machinery that feeds the PvsNPAssembly, where it supports the conditional path asserting that high J-frustration implies exponential circuit size. It also populates the Core.Complexity namespace. The positive-gap result for UNSAT instances directly instantiates the non-contractible obstruction stated in the RSatEncoding doc-comment and aligns with the eight-tick octave and phi-ladder structure of the broader framework.
scope and limits
- Does not prove P ≠ NP unconditionally.
- Does not compute numerical gap values for concrete formulas.
- Does not treat quantum or non-Boolean encodings.
- Does not address time-dependent or continuous-variable extensions.