pairResolve
plain-language theorem explainer
Defines the elementary forced move of the Phase-7 forward dynamics: given a recognition-level field on n sites and a coupled pair (i,j), replace both endpoints by their arithmetic mean and leave every other site fixed. Cosmology and equilibrium arguments cite it as the sigma-conserving, J-minimal tick. The body is a pure pointwise definition by cases, not a proved identity.
Claim. For a real field $x$ on $n$ sites and indices $i,j$, the pair-resolution field $x'$ is defined by $x'_k = (x_i + x_j)/2$ if $k \in \{i,j\}$, and $x'_k = x_k$ otherwise.
background
The module formalizes the Phase-7 forward dynamics on a recognition-level field $x : \mathrm{Fin}, n \to \mathbb{R}$ over a coupling graph. Each tick posts one forced recognition event: resolve a coupled pair by sending both endpoints to their mean. That move is the unique $\sigma = 0$, $J$-minimal update (no relaxation rate, no free parameter). The ratio of two regions is forced as $\varphi^{x_i - x_j}$, with $J$ the T5 cost reused from RefineTrigger.
The conserved bulk quantity is the level sum (sigma). The Lyapunov quantity is the level variance around the mean: each resolution drops it by exactly $(x_i - x_j)^2/2$. The zero-cost ground state of the total edge cost is consensus on every edge. This definition is the atomic operator those conservation and descent theorems act on.
proof idea
Pure definition: the returned field is the pointwise function that branches on whether the site equals $i$ or $j$. No lemmas are applied; downstream simp lemmas unfold this case split at $i$, at $j$, and off the pair.
why it matters
This is the elementary tick of recognition equilibrium. The Equilibrium package is stated entirely in terms of it: sigma conservation, the exact variance drop, and variance nonincrease are all quantified over pairResolve. Downstream theorems meanLevel_pairResolve, pairResolve_levelSum, varAround_pairResolve, and variance_nonincreasing are the Lean discharge of the Python forward-dynamics checks. Together they show closed-system descent is strict until consensus, while conjugate births (open extension) keep sigma = 0 so structure can persist. It sits under the cosmology side of the forcing chain: eight-tick cadence and $\varphi$-ladder ratios supply the discrete clock and cost, but the continuum field update itself is this mean-projection on edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.