sum_split_pair
plain-language theorem explainer
If two real configurations on a finite index set agree off a distinct pair of sites, the difference of their totals equals the difference of their values on that pair alone. Cosmology proofs of sigma conservation and the exact variance drop under pair-resolution cite it. The argument splits the universe sum into the pair plus complement and cancels the common rest by pointwise agreement.
Claim. Let $f,g:\{0,\ldots,n-1\}\to\mathbb{R}$ and $i\neq j$. If $f(k)=g(k)$ for every $k\notin\{i,j\}$, then $\sum_k f(k)-\sum_k g(k)=(f(i)+f(j))-(g(i)+g(j))$.
background
The module formalizes Phase-7 forward dynamics on a field of recognition levels $x:\mathrm{Fin},n\to\mathbb{R}$. Each tick resolves one coupled pair $(i,j)$ by sending both endpoints to their mean (the $\sigma=0$, $J$-minimal move). The Python reference checks conservation and descent numerically; here they are theorems.
levelSum is the plain sum of levels (the conserved sigma). pairResolve replaces $x_i$ and $x_j$ by their average and leaves every other site fixed. varAround measures squared spread about a reference. The present lemma is the elementary Finset bookkeeping that isolates the pair contribution whenever two configurations agree off ${i,j}$.
No Recognition-Science constants enter: the statement is pure finite-sum algebra over $\mathbb{R}$, reused by both the closed-system descent facts and (indirectly) the driven birth extension that keeps sigma conserved.
proof idea
Fix the two-element set ${i,j}\subseteq\mathrm{univ}$. Rewrite $\sum f$ via Finset.sum_sdiff plus Finset.sum_pair (using $i\neq j$) as the sum over the complement plus $f(i)+f(j)$; do the same for $g$. On the complement, membership in the sdiff forces $k\neq i$ and $k\neq j$, so the agreement hypothesis gives pointwise equality and thus equal partial sums by Finset.sum_congr. Substitute both decompositions and cancel the common rest by ring.
why it matters
Direct parent of pairResolve_levelSum ("Sigma is conserved. Resolving a pair leaves the total level unchanged") and of varAround_pairResolve ("Resolving a pair lowers the spread by exactly $(x_i-x_j)^2/2$"). Those two facts are the spine of the module: sigma conservation plus an exact Lyapunov decrement on variance imply strict descent to consensus on every edge, which is the $J$-cost ground state (totalCost_eq_zero_iff).
In the broader RS picture this is the discrete engine behind recognition equilibrium: forced pair resolutions conserve the level sum while driving the field to the unique zero-cost configuration. The same conservation is later paired with conjugate births so that open-system cosmogenesis keeps $\sigma=0$ while structure persists. The lemma itself is scaffolding-free bookkeeping; without it the two parent theorems cannot discharge their sum differences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.