pairResolve_levelSum
plain-language theorem explainer
Pair resolution preserves the sum of recognition levels: both endpoints move to their arithmetic mean, so the global sum (sigma) is unchanged. Cosmology and forward-dynamics arguments cite this as the closed-system conservation law. The proof splits the finite sum into the resolved pair versus the rest, substitutes the two mean values, and cancels by elementary algebra.
Claim. For any finite level field $x:\{0,\ldots,n-1\}\to\mathbb{R}$ and distinct indices $i\neq j$, if one replaces both $x_i$ and $x_j$ by their mean $(x_i+x_j)/2$ and leaves every other coordinate fixed, then $\sum_k x'_k=\sum_k x_k$.
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: a coupled pair $(i,j)$ is resolved by sending both endpoints to their arithmetic mean. That move is the unique sigma-neutral, $J$-minimal update (no rate parameter).
levelSum is the plain finite sum $\sum_k x_k$, the conserved sigma quantity of the closed system. pairResolve x i j is the updated field that equals $(x_i+x_j)/2$ at $i$ and at $j$, and equals $x$ elsewhere. The companion lemmas pin the values at the two endpoints and the agreement off ${i,j}$.
The local goal is the first conservation fact listed in the module: resolutions conserve sigma. Later, conjugate births conserve charge sum as well, so sigma remains zero through the driven open evolution.
proof idea
Unfold levelSum. Build the off-pair agreement hypothesis from pairResolve_other. Apply sum_split_pair to write the difference of the two full sums as the contribution on ${i,j}$ alone. Rewrite the resolved endpoints via the simp lemmas pairResolve_at_i and pairResolve_at_j, obtaining $((x_i+x_j)/2+(x_i+x_j)/2)-(x_i+x_j)$. That expression is identically zero by ring; linarith finishes the equality of the two sums.
why it matters
This is the closed-system half of sigma conservation in Recognition equilibrium. It is packaged directly into recognitionEquilibrium as the sigma_conserved field, and it is the one-line engine of meanLevel_pairResolve (mean equals sum over $n$). Together with the exact variance drop $(x_i-x_j)^2/2$, it shows the forward dynamics is a strict Lyapunov descent to consensus on every edge while holding the global level fixed.
In the broader framework this is the discrete conservation law behind the Phase-7 cosmogenesis scripts: resolutions never inject net level, so structure can only be sustained by the open conjugate-birth input. The foam-topology freeze-out theorem sits downstream in the same cosmology stack, using the equilibrium package that this lemma helps assemble. No scaffolding remains: the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.