variance_const_zero
plain-language theorem explainer
Variance of any constant real-valued function on the hypercube {0,1}^n equals zero. Analysts of convergence rates for gradient descent on the J-cost landscape cite this baseline fact. The proof is a one-line term-mode reduction that unfolds the variance sum and cancels all deviation terms via algebraic simplification.
Claim. Let $V$ be the variance of a real-valued function on the hypercube with $2^n$ vertices, defined as the sum of squared deviations from the mean value. For any $n : ℕ$ and constant $c : ℝ$, $V(f) = 0$ where $f$ maps every vertex to $c$.
background
The module examines the spectral gap of the J-cost Laplacian on the hypercube, which controls how fast recognition processes modeled as gradient descent converge to minima. Variance is defined as the sum over all inputs $a$ of $(x a - $ average of $x)^2$. The local setting treats variance as a tool for analyzing flat versus structured cost landscapes in the Recognition framework.
proof idea
The term proof unfolds the Variance definition then applies simp with sub_self and sq to reduce the constant case directly to zero.
why it matters
This establishes the zero-variance case for constant functions on the hypercube, a prerequisite for spectral-gap arguments in the J-cost setting. It supports module results on convergence rates and iteration bounds. It aligns with the framework's use of variance to separate flat regions from the phi-ladder structure in recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.