shiftDown
plain-language theorem explainer
Integer single-rung descent: given a vertex set S and rung field k, lower every cell in S by exactly one and leave the rest fixed. Cosmology and graded-cost arguments cite it as the discrete T-3 move that the cost meter actually charges. The body is a pointwise if-then on the predicate S.
Claim. For a decidable predicate $S$ on vertices and an integer rung assignment $k:V\to\mathbb{Z}$, define the descended field by $(k\downarrow_S)(v)=k(v)-1$ if $v\in S$ and $(k\downarrow_S)(v)=k(v)$ otherwise.
background
Phase 59 sits in the cosmology rung-cost stack. Phase 56 forced the graded recognition-cost law to depend on the minimal-distinction invariant UnitStep: every adjacency changes the integer rung by at most one. Phase 57 wired that law into the runtime cost meter. Phase 58 showed that the real-valued mean move does not automatically preserve UnitStep; only a local post-move criterion works.
The live engine does not shift integer rungs by real means. When a distinction is forced, it descends a region by exactly one rung (the T-3 single-rung move). The object charged by the cost meter is therefore an integer field $k:V\to\mathbb{Z}$ on a vertex set $V$, together with an edge set $E$ on which UnitStep is checked.
This definition is that elementary update: pick any region $S$ and subtract one from $k$ on $S$. Sibling dual is the raise-by-one map. Downstream lemmas unpack the pointwise cases and feed the cut criterion that decides when UnitStep survives.
proof idea
Pure definitional construction, not a proof. The body is the pointwise conditional: on vertices satisfying $S$, return $k(v)-1$; otherwise return $k(v)$. Decidability of $S$ makes the branch computable. Immediate corollaries shiftDown_pos and shiftDown_neg are one-line if_pos / if_neg rewrites of those two branches.
why it matters
This is the integer move Phase 59 studies. Every preservation theorem in the module is stated about it: the local cut criterion (shiftDown_unitStep_of_cut), unconditional top-rung preservation (shiftDown_top_unitStep), existence of a nontrivial preserving descent (exists_top_descent_unitStep), and the necessity counterexample that descending a non-top cell can break UnitStep (ckLevels_descend_min_breaks).
Together those results close the open item left by Phases 56–58: the generic real mean move need not preserve unit-step, but the forced top-rung integer descent does, so the Phase-56 cost law remains theorem-backed cycle to cycle along the active dynamics. The dual raise-bottom map is the symmetric counterpart. No new axioms beyond Mathlib's standard three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.