variance_nonneg
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.