chain3_resolved_second_gap
plain-language theorem explainer
After a mean-move on the first edge of the three-site chain with levels 0,1,2, the residual gap on the second edge is exactly 3/2. Cosmology and runtime-cost authors cite this as the arithmetic heart of the unit-step counterexample. The proof evaluates the resolved field at the two endpoints via the pair-resolve simplification lemmas and finishes by numerical normalization.
Claim. Let the three-site field be $x(0)=0$, $x(1)=1$, $x(2)=2$. After the mean-move that replaces both endpoints of the edge $(0,1)$ by their average, the absolute difference between the new values at sites $1$ and $2$ equals $3/2$.
background
Phase 56 forced the graded-rung cost law under the minimal-distinction invariant UnitStep: adjacent rungs differ by at most one. The active dynamics update is pair-resolve, which sends a coupled pair to their arithmetic mean and leaves every other site fixed. The module asks whether that mean-move automatically preserves UnitStep on the whole edge list.
It does not. The three-site chain with initial levels $0,1,2$ is unit-step on edges $(0,1)$ and $(1,2)$. Resolving $(0,1)$ produces levels $1/2,1/2,2$. The second edge then has gap $3/2>1$. This lemma isolates that residual gap as an exact real equality, before the parent theorem packages it as a UnitStep failure.
Upstream, pairResolve_at_j evaluates the resolved field at a resolved endpoint to the mean, and pairResolve_other leaves any third site unchanged. The initial field chain3Levels is the case-split $0,1,2$ on Fin 3.
proof idea
Two decide facts record that site 2 is distinct from both resolved endpoints. Rewrite the left-hand side with pairResolve_at_j (so the value at site 1 becomes the mean of levels 0 and 1) and pairResolve_other (so the value at site 2 stays 2). The absolute difference collapses to $|1/2-2|$, which norm_num evaluates to $3/2$.
why it matters
This is the arithmetic step inside chain3_pairResolve_breaks_unitStep, the module's explicit counterexample that a unit-step field need not remain unit-step after a mean-move. The parent theorem quotes the post-move levels $1/2,1/2,2$ and the gap $3/2>1$ to refute any global claim that pair-resolve preserves UnitStep.
In the Recognition framework the live engine may apply the Phase-56 graded-rung cost law only after the local unit-step audit pairResolve_unitStep_of_local succeeds. Blind global preservation would be false; this gap computation is the concrete witness. It does not touch the forcing chain T0-T8 directly, but it disciplines how the eight-tick runtime may meter rung costs under active recognition dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.