variance_nonneg
Non-negativity of variance holds for every real-valued function on the n-dimensional hypercube. Analysts of convergence in the J-cost Laplacian cite this to establish the spectral gap certificate. The proof is a one-line term-mode reduction to the non-negativity of a sum of squares.
claimFor all natural numbers $n$ and all functions $x : (Fin n → Bool) → ℝ$, $0 ≤ Variance(x)$, where $Variance(x) := ∑_{a} (x(a) - (1/2^n) ∑_b x(b))^2$.
background
The SpectralGap module studies how the spectral gap of the J-cost Laplacian governs the convergence speed of R̂ modeled as gradient descent on the J-cost landscape. Variance is defined as the sum over all boolean assignments of the squared difference between the function value and its global average. This non-negativity theorem is the initial property needed before constructing the full spectral gap certificate.
proof idea
The proof is a direct term-mode application of Finset.sum_nonneg. It instantiates the sum with the function that maps each assignment a to the square of the deviation (x a minus the mean), which is non-negative by sq_nonneg.
why it matters in Recognition Science
This result supplies the variance_nonneg_cert component of the SpectralGapCert structure, which certifies the spectral gap for use in convergence rate bounds. It fills the first key result listed in the module documentation for the J-cost Laplacian. The module notes an open Cheeger-type inequality in unsat_has_spectral_gap as the remaining scaffolding.
scope and limits
- Does not prove that the variance is positive for non-constant functions.
- Does not relate the variance to the J-cost function or the Laplacian eigenvalues.
- Does not provide bounds in terms of n or other parameters.
- Does not connect to the Recognition Science forcing chain or constants.
formal statement (Lean)
38theorem variance_nonneg {n : ℕ} (x : (Fin n → Bool) → ℝ) :
39 0 ≤ Variance x :=
proof body
Term-mode proof.
40 Finset.sum_nonneg (fun a _ => sq_nonneg _)
41