pairResolve_at_j
plain-language theorem explainer
Evaluating the forced pair-resolution map at the second endpoint returns the arithmetic mean of the two levels. Anyone proving conservation or Lyapunov identities for the Phase-7 forward dynamics cites this simp fact. The proof is a one-line unfold plus if_pos rewrite on the right disjunct.
Claim. For any recognition-level field $x:\{0,\ldots,n-1\}\to\mathbb{R}$ and indices $i,j$, the field obtained by resolving the coupled pair $(i,j)$ takes the value $(x_i+x_j)/2$ at site $j$.
background
The module formalizes Phase-7 forward dynamics on a field of recognition levels $x:\mathrm{Fin},n\to\mathbb{R}$. Each tick posts one forced recognition event: resolve a coupled pair $(i,j)$ by sending both endpoints to their arithmetic mean. That move is sigma-preserving and $J$-minimal (no rate parameter).
The resolution map is defined pointwise: at $k$ equal to $i$ or $j$ it returns $(x_i+x_j)/2$; elsewhere it leaves $x_k$ unchanged. This lemma is the evaluation of that map at the second endpoint. Its twin for the first endpoint and the off-pair identity complete the case split used by every conservation and descent argument in the module.
proof idea
One-line wrapper. Unfold the resolution map, then rewrite by if_pos on the right disjunct of $k=i\lor k=j$, discharged by reflexivity at $k=j$. No arithmetic lemmas are needed.
why it matters
This simp fact is the evaluation half of the resolution map. Downstream, level-sum conservation uses it (with the off-pair identity) to show sigma is unchanged under a resolve. The exact variance drop identity likewise reduces the two changed sites to the mean and obtains the law-given decrement $(x_i-x_j)^2/2$. Outside the module, the three-site chain lemma after resolving the first edge rewrites the second-edge gap via this evaluation and gets $3/2$. Together these discharge the central convergence facts of the closed-system descent to the $J$-cost ground state (consensus on every edge).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.