variance_nonincreasing
plain-language theorem explainer
Under a forced pair resolution (both endpoints replaced by their mean), the level variance of a finite real field never increases. Cosmologists and analysts of the Phase-7 forward dynamics cite this as the Lyapunov inequality for recognition descent. The proof is a one-line rewrite through the exact drop identity, then nonnegativity of a square.
Claim. For any finite real-valued level field $x$ on $n$ sites and any two distinct indices $i,j$, if one replaces both $x_i$ and $x_j$ by their arithmetic mean (leaving all other sites fixed), then the variance of the resulting field is at most the variance of $x$.
background
The module formalizes the Phase-7 forward dynamics: a field of recognition levels $x:\mathrm{Fin},n\to\mathbb{R}$ evolves by posting, each tick, one forced recognition event on a coupled pair. That event is pairResolve: both endpoints are sent to their mean. This is the $\sigma=0$, $J$-minimal move (no relaxation rate, no free knob).
Level variance is the Lyapunov function of the descent: it is the sum of squared deviations of the levels about their mean. The exact identity upstream states that one resolution lowers variance by precisely $(x_i-x_j)^2/2$. The present inequality is the immediate corollary that the spread never grows.
The broader setting ties this to the recognition cost $J$ (nonnegative, zero only at ratio one) and to total cost on the coupling graph, whose ground state is exactly consensus. Closed-system descent therefore relaxes to a constant field on every edge.
proof idea
Rewrite the goal with the exact Lyapunov identity variance_pairResolve, which equates the post-resolution variance to the original variance minus $(x_i-x_j)^2/2$. The claimed inequality then reduces to nonnegativity of that subtracted term. Discharge with nlinarith using sq_nonneg on the difference $x_i-x_j$. No case splits and no induction.
why it matters
This is the inequality half of the variance Lyapunov law for recognition equilibrium. It is packaged into the Equilibrium structure as the field variance_nonincreasing, and discharged for every level field and coupling graph by recognitionEquilibrium (alongside sigma conservation, the exact drop, and nonnegativity of total cost).
In the framework it certifies that the forced mean-resolution dynamics is a genuine descent: variance is a Lyapunov function, so the forward evolution cannot wander away from consensus. That underwrites the closed-system half of Phase-7 cosmogenesis (open-system conjugate births conserve charge separately). Downstream foam-topology freeze-out arguments sit on the same equilibrium package: once the front homogenizes an inner ball, the variance law guarantees the descent has nowhere left to go except the vacuum configuration whose Euler characteristic drops by one.
No open scaffold remains here; the claim is fully proved and is the soft form of the exact drop already established upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.