varAround_pairResolve
plain-language theorem explainer
Resolving a coupled pair by sending both endpoints to their mean lowers the squared spread around any fixed reference by exactly half the squared gap. Cosmologists and analysts of the Phase-7 forward dynamics cite this as the reference-independent identity behind the variance Lyapunov law. The proof splits the sum into the pair and the rest, simplifies the two changed sites, and finishes by ring algebra plus linarith.
Claim. For any finite level field $x:\mathrm{Fin}\,n\to\mathbb{R}$, distinct indices $i\neq j$, and any reference $c\in\mathbb{R}$, if one replaces both $x_i$ and $x_j$ by their arithmetic mean (leaving all other sites fixed), then $\sum_k(\tilde x_k-c)^2=\sum_k(x_k-c)^2-(x_i-x_j)^2/2$.
background
The module formalizes the Phase-7 forward dynamics on a field of recognition levels $x:\mathrm{Fin},n\to\mathbb{R}$. Each tick posts one forced recognition event: resolve a coupled pair $(i,j)$ by sending both endpoints to their mean. That move is the $\sigma=0$, $J$-minimal update; there is no relaxation rate or free knob.
pairResolve is exactly that update: at $i$ and $j$ it writes $(x_i+x_j)/2$, and elsewhere it leaves $x$ unchanged. The three evaluation lemmas pin the values at $i$, at $j$, and off the pair. varAround x c is the unnormalized squared spread $\sum_k(x_k-c)^2$ about an arbitrary reference $c$, not yet specialized to the mean.
The private helper sum_split_pair reduces a difference of two full sums to the two-site contribution whenever the summands agree off ${i,j}$. That is the only summation infrastructure the identity needs.
proof idea
Unfold varAround. Build an agreement hypothesis: off ${i,j}$, the squared deviations of the resolved field equal those of $x$, via pairResolve_other. Feed that into sum_split_pair so the full-sum difference collapses to the two changed sites. Simplify those sites with pairResolve_at_i and pairResolve_at_j. A one-line ring identity shows that twice the squared mean-deviation minus the two original squared deviations equals $-(x_i-x_j)^2/2$. Rewrite and close by linarith.
why it matters
This is the reference-free engine under the variance Lyapunov law. Downstream, variance_pairResolve specializes the reference to the mean level (using mean conservation under resolution) and obtains the exact decrement of the true variance: each forced resolution lowers variance by $(x_i-x_j)^2/2$. The module doc states the consequence: variance is a strict Lyapunov function until every coupled pair is equal, while total edge demand is not claimed monotone.
In the broader Recognition picture this is the closed-system half of cosmogenesis: resolutions conserve the level sum and strictly descend the spread toward consensus (the $J$-cost ground state on the coupling graph). The open-system conjugate-birth side conserves charge separately; together they keep $\sigma=0$ while preventing total homogenization. The identity is pure finite-dimensional algebra, independent of $\phi$, the eight-tick octave, and the forcing chain, yet it is what makes the discrete descent law exact rather than approximate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.