ckLevels_descend_min_breaks
plain-language theorem explainer
On the three-site chain with integer rungs 0,1,2, descending only the bottom cell breaks the unit-step invariant: the edge to its neighbour then has gap 2. Anyone citing the top-rung descent theorem needs this to show the top-rung restriction is necessary. The proof is a one-line unfold-and-decide on the finite edge set.
Claim. Let $V = \mathrm{Fin}\,3$ with edges $\{(0,1),(1,2)\}$ and rung field $k(0)=0$, $k(1)=1$, $k(2)=2$. After shifting down the singleton $\{0\}$ by one rung, the resulting field is not unit-step on those edges: some adjacency differs by more than one integer rung.
background
Phase 56 defines 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 engine maintains this because T-3 descends one rung at a time, and the Phase-56 cost law charges only under that invariant.
Phase 59 studies the integer update the cost meter actually uses: shiftDown S k subtracts one from $k$ on a set $S$. The positive theorem is that descending the top rung (any upper bound $M$ on rungs present in $E$) preserves unit-step unconditionally. The dual raises the bottom rung.
This declaration is the necessity counterexample on the concrete chain. The edges are the ordered pairs $(0,1)$ and $(1,2)$; the levels are the identity rungs $0,1,2$. Descending only the vertex at rung $0$ is the non-top single-cell move that the headline theorem pairs against the safe top descent.
proof idea
Pure finite check. Unfold the definition of unit-step (universal quantification over the two chain edges and the three admissible gaps) and run decide on the concrete Finset and the shifted integer field. No lemmas are invoked; the kernel evaluates that after sending cell $0$ from rung $0$ to $-1$, the edge $(0,1)$ has difference $2$, which is outside ${0,\pm 1}$.
why it matters
Feeds the Phase-59 headline t59_rung_descent_preservation, which bundles two facts: top-rung descent preserves unit-step for any unit-step field with an upper bound (so the Phase-56 cost law applies to the next cycle), and this chain shows a non-top single-cell descent breaks it. The module doc states the honest status: together with Phase 58 (the real-valued mean move does not preserve unit-step globally), this is the complete answer to whether the dynamics preserves the graded-rung invariant.
In the Recognition framework the cost meter is theorem-backed only along updates that keep unit-step. The top-rung restriction is therefore load-bearing, not cosmetic: without this counterexample the positive preservation theorem would look stronger than the dynamics allow. Closes the "active dynamics preserves UnitStep cycle to cycle" item with the exact truth rather than a blanket claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.