shiftDown_neg
plain-language theorem explainer
Outside a chosen descent set S, the integer rung field is left unchanged by a one-rung down-shift. Cosmology and graded-cost arguments cite this when case-splitting on whether a vertex is selected for descent. The proof is the negative branch of the defining if-expression.
Claim. Let $S$ be a decidable predicate on vertices and $k:V\to\mathbb{Z}$ an integer rung field. If $v\notin S$, then the one-rung descent of $k$ on $S$ satisfies $(\mathrm{shift\downarrow}_S k)(v)=k(v)$.
background
Phase 59 studies integer-rung updates that the live cost meter actually charges. The move shiftDown takes a region $S$ and a field $k:V\to\mathbb{Z}$ and posts $k(v)-1$ on $S$, leaving every other vertex fixed. That is the T-3 single-rung descent: rungs change by exactly one integer step, never by a real mean.
The ambient invariant is UnitStep: every edge in the active edge set changes the integer rung by at most one. Phase 56 made the graded recognition-cost law depend on that invariant; Phase 58 showed that blind real-valued mean moves need not preserve it. The present module supplies the positive half for integer descent.
This lemma is the fixed-point branch of the definition: when the vertex is outside $S$, the if-expression returns $k(v)$ unchanged. Its dual sibling records the same fact for the up-shift.
proof idea
One-line definitional reduction. Unfold shiftDown to the pointwise if S v then k v - 1 else k v, then apply Mathlib's if_neg to the hypothesis $\neg S(v)$ to select the else branch.
why it matters
Case analysis on cut edges in the unit-step preservation theorems needs both branches of the descent. Downstream, shiftDown_unitStep_of_cut uses this lemma on endpoints outside $S$ (gap unchanged), and shiftDown_top_unitStep inherits it when discharging the cut condition for top-rung descent.
Together those results close the Phase-59 claim: descending the coarsest (top) rung preserves UnitStep unconditionally, so the Phase-56 graded cost law applies cycle to cycle along the forced T-3 move. The lemma itself is bookkeeping, but without the outside-set identity the cut/non-cut split does not typecheck.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.