chain3_pairResolve_breaks_unitStep
plain-language theorem explainer
A three-site chain with levels 0,1,2 is unit-step, yet after the mean-move on the first edge the second edge has gap 3/2, so unit-step fails. Cosmology and runtime-cost authors cite this to kill any global "mean-move preserves UnitStep" claim. The proof assumes the resolved field is unit-step, specializes to the second edge, and reduces to the known gap 3/2 via a one-line numerical contradiction.
Claim. Let $x$ be the three-site field with levels $x(0)=0$, $x(1)=1$, $x(2)=2$, and let $E$ be the edge list $\{(0,1),(1,2)\}$. After the mean-move that sends sites $0$ and $1$ to their average, the resulting field is not unit-step on $E$: some edge has absolute level gap strictly larger than $1$.
background
Phase 56 forced the graded-rung cost law under the minimal-distinction invariant that adjacent rungs differ by at most one. The real-valued form used here, UnitStepReal, asserts that every listed edge $e$ satisfies $|x(e_1)-x(e_2)|\le 1$. It is the right formulation once mean-moves are allowed, since those can create half-rungs from integer inputs.
The active dynamics posts, each tick, the J-minimal resolution of one coupled pair: both endpoints are sent to their arithmetic mean (pairResolve). The module's local setting is that a blind global claim "pairResolve preserves UnitStepReal" is false. The honest layer is a local criterion (every edge touching the resolved pair stays within gap one after the move) plus an explicit three-site counterexample showing that criterion is necessary.
The counterexample data are fixed: chain edges $(0,1)$ and $(1,2)$, initial levels $0,1,2$. An upstream lemma already computes that after resolving $(0,1)$ the second edge has gap exactly $3/2$.
proof idea
Assume for contradiction that the resolved field remains unit-step on the three-site edge list. The second edge $(1,2)$ is in that list by unfolding the edge definition. Specialize the unit-step hypothesis to that edge to obtain a gap bound $\le 1$. Rewrite the gap via the upstream lemma that evaluates it to exactly $3/2$ after the mean-move on $(0,1)$. A numerical normalization then yields the contradiction $3/2\le 1$.
why it matters
This is the negative half of the Phase-58 headline on unit-step preservation for active recognition dynamics. Downstream, the honest packaging theorem conjoins the local preservation criterion with this counterexample to state that mean-move dynamics preserves unit-step exactly under the local post-move edge condition, and that the condition is necessary rather than cosmetic.
Without the counterexample, a runtime cost meter could silently apply the Phase-56 graded-rung cost law after every mean-move. The theorem forces an audit (or a later proof) of the local touching-edge condition before that law is reused. In the broader Recognition chain this sits downstream of the forcing landmarks that fix the cost shape and the eight-tick discrete tick structure; it does not itself touch T5--T8, but it polices when the graded cost may be invoked on live fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.