meanLevel_pairResolve
plain-language theorem explainer
Pair resolution leaves the mean recognition level unchanged: after both endpoints of a coupled pair are sent to their arithmetic mean, the field mean equals the original mean. Cosmology and dynamics workers cite this when tracking conserved sigma under forced recognition events. The proof is a one-line unfold of the mean plus the already-proved level-sum conservation identity.
Claim. For any finite field of recognition levels $x : \mathrm{Fin}\, n \to \mathbb{R}$ and distinct indices $i \neq j$, if one replaces both $x_i$ and $x_j$ by $(x_i + x_j)/2$ (leaving all other sites fixed), then the mean level of the updated field equals the mean level of $x$.
background
The module formalizes Phase-7 forward dynamics: a field of recognition levels on a coupling graph evolves by posting, each tick, one forced recognition event. That event resolves a coupled pair by sending both endpoints to their arithmetic mean (the sigma = 0, J-minimal move; no free relaxation rate).
The mean level is the total level sum divided by $n$. The level sum itself is conserved under pair resolution (pairResolve_levelSum: "Resolving a pair leaves the total level unchanged"). Variance about the mean is the Lyapunov function of the descent; the mean must therefore be stable under each tick so that variance comparisons stay well-defined at a fixed centre.
Local setting: closed-system descent relaxes toward consensus (constant field on every edge). Open-system births of conjugate pairs later conserve the same charge sum, so mean-zero structure can persist while resolutions keep homogenizing local gaps.
proof idea
One-line tactic proof. Unfold the definition of mean level (level sum over $n$). Rewrite the numerator by the upstream conservation theorem pairResolve_levelSum, which equates the level sum after resolution to the original level sum when $i \neq j$. The denominator $n$ is unchanged, so the means agree.
why it matters
This is the mean-stability lemma that unlocks the variance Lyapunov law. Downstream, variance_pairResolve rewrites through it and then applies the centred second-moment identity to obtain
$$\mathrm{Var}(\mathrm{pairResolve}, x, i, j) = \mathrm{Var}(x) - (x_i - x_j)^2/2.$$
That exact decrement is the recognition gap resolved each tick, so variance is a strict Lyapunov function until every coupled pair is equal. The module doc lists this chain as the Lean discharge of the Python forward-dynamics checks: level-sum conservation, variance drop, nonnegativity of total $J$-cost, and consensus as the unique ground state. In the broader Recognition framework it sits under the Phase-7 cosmogenesis story (forced $J$-minimal moves, conserved sigma), not under the T0–T8 forcing chain itself, but it makes the discrete descent to the $J$-cost ground state fully rigorous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.