varAround
plain-language theorem explainer
Defines the squared Euclidean spread of a finite real level field about an arbitrary reference value c. Cosmology and Lyapunov arguments cite it as the reference-independent building block of level variance. The body is a one-line sum of squared deviations; no proof obligations.
Claim. For $n \in \mathbb{N}$, a level field $x : \{0,\ldots,n-1\} \to \mathbb{R}$, and a reference $c \in \mathbb{R}$, the spread about $c$ is $\sum_k (x_k - c)^2$.
background
The RecognitionEquilibrium module formalizes Phase-7 forward dynamics on a coupling graph: each tick resolves one coupled pair $(i,j)$ by sending both endpoints to their mean (the $\sigma=0$, $J$-minimal move). The level field is $x : \mathrm{Fin}, n \to \mathbb{R}$; the dynamics is strict descent on a Lyapunov function until every coupled pair agrees.
Spread about a free reference $c$ is the natural intermediate quantity. The actual Lyapunov function is the special case with $c$ equal to the mean level: variance is defined as that specialization. Pair resolution conserves the level sum, so the mean is invariant under the closed-system step; the free-reference form is what makes the exact drop identity hold for every $c$, not only the mean.
Upstream, the module reuses $J$-cost nonnegativity from RefineTrigger and $\varphi$ from Constants. The ratio of two regions is forced as $\varphi^{x_i - x_j}$.
proof idea
Pure definition: unfold to the finite sum $\sum_k (x_k - c)^2$. No lemmas, no tactics. Downstream theorems unfold this def and rewrite the two resolved coordinates while the remaining terms cancel by agreement off ${i,j}$.
why it matters
Parent results are varAround_pairResolve (exact drop of spread by $(x_i - x_j)^2/2$ for any reference $c$) and variance (spread about the mean, the Lyapunov function of the descent). The free-reference form is essential: the drop identity is independent of $c$, so specializing $c$ to the mean immediately yields the variance decrement used in variance_pairResolve and variance_nonincreasing.
In the module narrative this underwrites the claim that closed-system recognition dynamics is strict descent to consensus (total recognition cost zero iff the field is constant on every edge). That is the Lean discharge of the central convergence facts checked numerically in the Phase-7 forward-dynamics scripts. It sits downstream of the forcing chain's $J$-uniqueness (T5) and the recognition composition law, which fix the $J$-minimal pair move that the dynamics posts each tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.