shiftDown_top_unitStep

Phase 59 studies integer-rung descent as the positive complement to Phase 58. The live engine does not move rungs by real means; it descends a region by exactly one rung when a distinction is forced (T-3). The invariant that makes the Phase-56 graded cost law well-posed is UnitStep: every adjacency changes the integer rung by at most one, i.e. $k(p_1)-k(p_2)\in{0,+1,-1}$.

The elementary move is shiftDown S k, which sends every cell in a decidable set $S$ to $k(v)-1$ and leaves the complement fixed. The general preservation theorem is the cut criterion: descending $S$ preserves unit-step on all of $E$ exactly when every cut edge (one endpoint in $S$, one outside) still has gap in ${0,\pm 1}$ after the move. Interior and exterior edges are free, since both endpoints shift by the same amount or by none.

This declaration specialises that criterion to the top rung. Taking $S={v:k(v)=M}$ with $M$ an upper bound on every rung appearing in $E$ makes the cut condition automatic: a top cell cannot neighbour anything above it, and unit-step forbids a neighbour two or more below, so the neighbour sits at $M-1$.

One application of the cut criterion shiftDown_unitStep_of_cut with $S={v:k(v)=M}$, followed by a case split that discharges hcut.

For a cut edge $p\in E$, the two cut orientations are handled symmetrically. If the first endpoint is in $S$ and the second is not, the upper bound plus $k(p_2)\ne M$ gives $k(p_2)<M$; unit-step then forces $k(p_2)=M-1$ by omega. Evaluating the shifted field via shiftDown_pos on the top endpoint and shiftDown_neg on the exterior endpoint yields values $M-1$ and $M-1$, so the new gap is $0$. The opposite cut orientation is identical with the roles reversed. Non-cut edges are already covered by the cut lemma.

This is the unconditional top-rung discharge that Phase 59 needs. The module doc states the point directly: descending the coarsest (top) rung, the natural parameter-free relaxation move, provably keeps the field unit-step, so the Phase-56 cost law applies to the next cycle.

It is the first conjunct of the Phase-59 headline t59_rung_descent_preservation, which pairs this positive fact with the necessity counterexample on the chain $0,1,2$ (descending a non-top cell breaks unit-step). It is also the engine of exists_top_descent_unitStep: once $M$ is taken to be the realised maximum rung on the edge vertices, this theorem supplies a nontrivial preserving descent with no external parameter.

In the broader Recognition picture this closes the honest answer to invariant preservation under the active dynamics: the generic real mean move does not preserve unit-step globally (Phase 58), but forced top-rung integer descent does. That is exactly the update the cost meter charges when T-3 descends one rung at a time.