pairResolve_at_i
plain-language theorem explainer
Evaluating the forced pair-resolution map at the first endpoint returns the arithmetic mean of the two levels. Anyone proving level-sum conservation or the exact variance drop for a recognition tick cites this simp fact. The proof is a one-line unfold of the definition plus the true branch of the conditional.
Claim. For any $n$, any field $x:\{0,\ldots,n-1\}\to\mathbb{R}$, and any indices $i,j$, the pair-resolved field at site $i$ equals $(x_i+x_j)/2$.
background
The module formalizes Phase-7 forward dynamics: a field of recognition levels $x$ on a finite index set evolves by posting, each tick, one forced recognition event. That event resolves a coupled pair $(i,j)$ by sending both endpoints to their mean, the $\sigma=0$, $J$-minimal move (no rate, no free parameter).
The resolution map is defined pointwise: at $k\in{i,j}$ it returns $(x_i+x_j)/2$; elsewhere it leaves $x_k$ unchanged. This lemma records the value at the first endpoint. Sibling facts cover the second endpoint and the off-pair sites. Downstream, the level sum and the variance-around-a-reference are rewritten by splitting the finite sum into the pair contribution plus the unchanged remainder.
proof idea
One-line wrapper: unfold the pointwise definition of the resolution map, then rewrite by the positive branch of the conditional, using $k=i$ (via Or.inl rfl). No arithmetic lemmas are needed.
why it matters
This is the first evaluation fact for the forced recognition move. It is consumed by the sigma-conservation theorem (resolving a pair leaves the total level unchanged) and by the exact variance-drop theorem (spread falls by exactly $(x_i-x_j)^2/2$, independent of reference). Those two results are the core Lyapunov and conservation statements of the closed-system descent: variance is strictly decreasing until every coupled pair is equal, and the recognition ground state is consensus. In the broader RS picture this is the discrete, law-given step that drives the field to the $J$-cost minimum without introducing relaxation knobs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.