variance
plain-language theorem explainer
Level variance of a recognition field is the sum of squared deviations from its mean. Phase-7 forward-dynamics work cites it as the Lyapunov function of forced pair resolution: each resolve drops the spread by exactly half the squared gap. Defined by centering the reference-spread functional on the field's own mean, so later drop lemmas measure descent about a conserved center.
Claim. For a level field $x:\{0,\ldots,n-1\}\to\mathbb{R}$, the variance is $\mathrm{Var}(x)=\sum_k(x_k-\bar x)^2$, where $\bar x=n^{-1}\sum_k x_k$ is the mean level.
background
The module formalizes Phase-7 forward dynamics on a recognition level field $x:\mathrm{Fin},n\to\mathbb{R}$. Each tick resolves one coupled pair $(i,j)$ by sending both endpoints to their arithmetic mean (the $\sigma=0$, $J$-minimal move). The Python reference checks the resulting conservation and descent facts numerically; here they are theorems.
Two supporting functionals are already in place. The mean level is $\bar x=(\sum_k x_k)/n$. The reference-centered spread $\mathrm{varAround}(x,c)=\sum_k(x_k-c)^2$ measures squared deviation from an arbitrary center $c$. The present definition simply specializes that center to $\bar x$.
Because pair resolution conserves the level sum, the mean is invariant under the dynamics. Centering the Lyapunov function on that conserved mean makes the exact drop law independent of any external reference choice.
proof idea
One-line definitional wrapper: unfold to $\mathrm{varAround},x,(\mathrm{meanLevel},x)$. No proof obligations; the noncomputable tag is inherited from real division in the mean.
why it matters
This is the Lyapunov function named in the module brief: variance drops by exactly $(x_i-x_j)^2/2$ on each forced resolve, so the dynamics is a strict descent until every coupled pair agrees. The Equilibrium package packages that drop (with sigma conservation and cost nonnegativity) as the recognition-equilibrium law; recognitionEquilibrium then shows the package holds for every field and coupling graph.
Downstream, variance_pairResolve, variance_nonincreasing, and the total-cost zero-iff-consensus theorems all quote this functional. Foam-topology freeze-out arguments sit one layer up: once the descent has homogenized an inner ball, Euler-character drop statements record the topological simplification. In the broader RS chain this is the concrete Lyapunov witness that the forward dynamics reaches the $J$-cost ground state (consensus on edges), matching the closed-system half of the Phase-7 cosmogenesis story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.