pairResolve_unitStep_of_local
plain-language theorem explainer
The mean-move that resolves a coupled pair preserves the real unit-step invariant on an edge list exactly when every edge touching either resolved endpoint still has gap at most one after the move. Cosmology and runtime-cost authors cite this as the audit gate before applying the Phase-56 graded-rung cost law to an actively updated field. The proof is a case split: touching edges use the local hypothesis; disjoint edges are unchanged by the mean-move and inherit the old invariant.
Claim. Let $x:\{0,\ldots,n-1\}\to\mathbb{R}$ be a level assignment and $E$ a list of edges. Write $U(x,E)$ for the property that every $e\in E$ satisfies $|x(e_1)-x(e_2)|\le 1$. Let $R_{ij}x$ send both endpoints $i$ and $j$ to their arithmetic mean and leave all other sites fixed. If $U(x,E)$ holds and every edge that touches $i$ or $j$ still has gap at most one under $R_{ij}x$, then $U(R_{ij}x,E)$ holds.
background
Phase 56 established the graded-rung cost law under the forced minimal-distinction invariant that adjacent rungs differ by at most one. Phase 57 wired that law into the runtime cost meter. The natural next claim would be that active mean-move dynamics automatically preserves the invariant; this module records that the global claim is false.
The real-valued unit-step property says every listed edge has level gap at most one. It is the right formulation because the mean-move can create half-rungs even from integer inputs. The mean-move itself sends both endpoints of a coupled pair to their average and leaves every other site fixed; off-pair sites are recovered by the identity lemma for that move.
An edge touches the resolved pair when either of its endpoints is one of the two resolved vertices. Disjoint edges are therefore fixed pointwise, so the old unit-step bound carries them for free.
proof idea
Fix an edge $e$ in the list. Case on whether $e$ touches the resolved pair $(i,j)$.
If it does, the local hypothesis supplies the post-move gap bound directly.
If it does not, neither endpoint of $e$ equals $i$ or $j$. Apply the identity lemma for the mean-move at both endpoints to rewrite the post-move levels as the original levels, then invoke the pre-move unit-step hypothesis on $e$.
The argument is pure case analysis plus two rewrites; no arithmetic beyond the definition of the mean-move is required.
why it matters
This is the positive half of the Phase-58 honesty layer. The headline theorem packages it with the three-site counterexample: a chain with levels $0,1,2$ is unit-step before resolving the first edge, but after the move the second edge has gap $3/2$, so the local condition is necessary rather than cosmetic.
Downstream, the three-chain gap lemma and the Phase-58 headline both depend on this criterion. The live engine may apply the Phase-56 cost law only after auditing or proving the local post-move condition for the update being applied. A blind global "mean-move preserves unit-step" lemma would be false, which is why the module refuses to state one.
Within Recognition Science cosmology this gates when graded-rung cost accounting remains valid under active recognition equilibrium dynamics (the $\sigma=0$, $J$-minimal pair resolution posted each tick).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.