Variance
plain-language theorem explainer
Variance defines the sum of squared deviations from the mean for any real-valued function on the n-dimensional boolean hypercube. Researchers analyzing convergence of gradient descent on J-cost landscapes cite it when deriving iteration bounds from spectral gaps. The definition is a direct Finset sum over all 2^n assignments with no additional lemmas required.
Claim. For $x : (Fin n → Bool) → ℝ$, let $μ = 2^{-n} ∑_b x(b)$. Then Variance$(x) = ∑_a (x(a) - μ)^2$.
background
The module treats the spectral gap λ₂ of the J-cost Laplacian as the quantity controlling convergence speed of the recognition operator R̂ when viewed as gradient descent on the J-cost landscape. Variance supplies the elementary statistical object on the hypercube {0,1}^n that later lemmas use to certify non-negativity and constancy. The J-cost itself enters via the imported JCostLaplacian module and the Recognition Composition Law that defines edge weights.
proof idea
Definition that directly expands to a Finset.univ.sum of squared deviations; the mean is computed once via a second sum divided by Finset.univ.card.
why it matters
Variance is the base object inside the SpectralGapCert structure and is invoked by variance_nonneg and variance_const_zero. These feed the positive-gap extraction for UNSAT formulas and the iteration-bound scaling m/λ in the ConvergenceRate analysis. It therefore sits at the interface between the J-cost Laplacian and the eight-tick octave convergence claims of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.