pairResolve_other
plain-language theorem explainer
If a site is not one of the two endpoints being resolved, the forced pair-resolution leaves its recognition level untouched. Cosmology proofs that split sums or variances into the resolved pair versus the rest cite this pointwise identity. The argument unfolds the definition and discharges the if-branch by the two inequalities.
Claim. Let $x : \{0,\ldots,n-1\} \to \mathbb{R}$ and fix indices $i,j,k$. If $k \neq i$ and $k \neq j$, then the forced pair-resolution of $(i,j)$ satisfies $(\mathrm{resolve}_{i,j} x)(k) = x(k)$.
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 the sigma-conserving, $J$-minimal update (no rate parameter).
The definition pairResolve implements exactly that: at $k \in {i,j}$ the value becomes $(x_i + x_j)/2$; elsewhere the field is copied. The present lemma is the off-pair clause of that piecewise definition.
Local setting (module header): resolutions conserve the level sum, drop variance by exactly $(x_i - x_j)^2/2$, and drive total recognition cost to zero precisely at edgewise consensus. Downstream unit-step preservation also relies on sites away from the resolved pair remaining fixed.
proof idea
One-line definitional argument. Unfold pairResolve, then rewrite by if_neg: the disjunction $k = i \lor k = j$ is false because both disjuncts contradict the hypotheses $k \neq i$ and $k \neq j$ (proved by a short rintro on the two cases). The else-branch is exactly $x,k$.
why it matters
This is the bookkeeping identity that lets every global invariant of a resolution reduce to a two-point calculation on ${i,j}$.
It is used directly in pairResolve_levelSum (sigma conservation: the sum splits into the resolved pair plus an unchanged remainder) and in varAround_pairResolve (exact variance drop $(x_i-x_j)^2/2$, again via pointwise agreement off the pair). Unit-step preservation in RecognitionUnitStepPreservation cites it for disjoint edges: pairResolve_unitStep_of_local and EdgeTouches treat non-touching edges as automatically unit-step because levels are copied; chain3_resolved_second_gap evaluates a concrete three-site gap after resolving the first edge.
In the Recognition framework this supports the Phase-7 claim that forward dynamics is strict $J$-descent to consensus while conserving sigma, with open-system conjugate births later reusing the same conservation pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.