variance_pairResolve
plain-language theorem explainer
Each forced pair resolution lowers the level-field variance by exactly half the squared gap between the two endpoints. Cosmologists and dynamicists cite this as the exact Lyapunov decrement for the Phase-7 forward dynamics. The proof unfolds variance and rewrites via mean conservation plus the reference-independent drop identity.
Claim. For any finite level field $x:\mathrm{Fin}\,n\to\mathbb{R}$ and distinct indices $i,j$, if one replaces both $x_i$ and $x_j$ by their arithmetic mean (leaving all other coordinates fixed), then the variance about the mean satisfies $\mathrm{Var}(x')=\mathrm{Var}(x)-(x_i-x_j)^2/2$.
background
The module formalizes the Phase-7 forward dynamics on a recognition level field $x:\mathrm{Fin},n\to\mathbb{R}$. Each tick posts one forced recognition event: resolve a coupled pair by sending both endpoints to their mean. That move is the $\sigma=0$, $J$-minimal update (no free rate parameter).
pairResolve implements the update: at $i$ and $j$ the value becomes $(x_i+x_j)/2$, elsewhere $x$ is unchanged. The mean level is the average of the level sum; variance is the second moment about that mean (varAround at meanLevel). Upstream, meanLevel_pairResolve records that the mean is invariant under resolution (because the level sum is conserved), and varAround_pairResolve gives the exact drop of the second moment about an arbitrary reference: the drop is always $(x_i-x_j)^2/2$, independent of the reference point.
proof idea
Short rewrite proof. Unfold variance to varAround at the mean. Replace the post-resolution mean by the original mean via meanLevel_pairResolve. Then apply varAround_pairResolve at the original mean, which supplies the exact algebraic identity
$\mathrm{varAround}(x',c)=\mathrm{varAround}(x,c)-(x_i-x_j)^2/2$
with $c=\mathrm{meanLevel},x$. No further arithmetic is needed.
why it matters
This is the variance Lyapunov law named in the module doc: the decrement equals the recognition gap that was resolved, so descent is strict until every coupled pair is equal. It is the exact law-level counterpart of the numeric checks in the Python forward dynamics.
Downstream, variance_nonincreasing is the immediate corollary (spread never grows). The package theorem recognitionEquilibrium packages the drop as the variance_drop field of the equilibrium structure for every level field and coupling graph. Foam-topology freeze-out arguments sit further downstream in the same cosmology stack. Within the broader RS chain this is the discrete Lyapunov engine that drives the field to the $J$-cost ground state (consensus on edges), complementary to T5 $J$-uniqueness and the RCL cost calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.