shiftDown_unitStep_of_cut
plain-language theorem explainer
Descending an arbitrary vertex set by one integer rung preserves the unit-step invariant on the edge set exactly when every cut edge stays within gap {0, ±1} after the move. Cosmology and RS engine auditors cite this as the local safety criterion for forced rung updates. The proof cases on endpoint membership in the descended set and reduces non-cut edges to the original unit-step hypothesis by algebraic cancellation.
Claim. Let $k : V \to \mathbb{Z}$ be a rung field and $E$ a finite set of ordered edges such that every adjacency changes $k$ by at most one (the unit-step property). Fix a decidable set $S \subseteq V$. Write $k'$ for the field that equals $k-1$ on $S$ and $k$ off $S$. If every cut edge of $S$ in $E$ (exactly one endpoint in $S$) still has $k'$-gap in $\{0,+1,-1\}$, then $k'$ is unit-step on $E$.
background
Phase 56 introduced the forced minimal-distinction property UnitStep: a rung field $k : V \to \mathbb{Z}$ is unit-step on an edge set $E$ when every adjacency changes the rung by at most one, i.e. $k(p_1)-k(p_2) \in {0,+1,-1}$. The live recognition engine maintains this because T-3 descends one rung at a time; the graded cost law of Phase 56/57 charges only under that invariant.
Phase 58 showed that a blind global claim for the real-valued mean move is false; only a local post-move criterion holds. Phase 59 (this module) supplies the positive half for the object the cost meter actually charges: the integer rung field. The update is not a real mean; it descends a region by exactly one rung when a distinction is forced.
The local map shiftDown S k decreases $k$ by one on the predicate $S$ and leaves it unchanged off $S$. Edges with both endpoints in $S$ keep their gap (both shift by $1$); edges with neither endpoint in $S$ are untouched. Only cut edges can break unit-step, which is exactly the hypothesis of this theorem.
proof idea
Tactic proof by introducing an arbitrary edge $p \in E$ and casing on whether each endpoint lies in $S$ (four cases via nested by_cases).
Both in $S$: rewrite with the positive-shift lemmas so each endpoint drops by $1$; the difference $(k_1-1)-(k_2-1)$ equals $k_1-k_2$ by ring, and the original unit-step hypothesis applies.
Cut cases (exactly one endpoint in $S$): discharge directly by the cut hypothesis, feeding the matching disjunct of the cut predicate.
Neither in $S$: rewrite with the negative-shift lemmas (field unchanged) and again apply the original unit-step hypothesis.
No external lemmas beyond the local shift identities and the given UnitStep assumption.
why it matters
This is the integer analogue of Phase 58's local post-move criterion, and the workhorse lemma of Phase 59. Downstream, shiftDown_top_unitStep applies it with $S = {v : k(v)=M}$ for an upper bound $M$ on all rungs in $E$; the cut hypothesis is then forced (a top-rung neighbour cannot sit two below under unit-step, so after descent the cut gap is $0$). That unconditional top-rung result is what lets the Phase-56 graded cost law apply cycle to cycle under the engine's natural parameter-free relaxation move.
In the Recognition forcing picture, T-3 descends one rung at a time and the eight-tick / phi-ladder cost accounting assumes unit-step adjacencies. Closing "the active dynamics preserves UnitStep" required exactly this cut criterion plus the top-rung discharge: the generic move does not preserve the invariant, but forced top-rung descent does. The module also records the necessity counterexample (descending a non-top cell on the chain $0,1,2$ breaks the gap), so the top-rung restriction is sharp rather than cosmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.