shiftUp
plain-language theorem explainer
Defines the dual integer-rung update: raise every vertex in a decidable set S by exactly one rung, leave the complement fixed. Cosmology and graded-cost arguments cite it as the bottom-raise move dual to top-rung descent. The body is a pointwise if-then on membership in S.
Claim. Given a decidable predicate $S$ on vertices and an integer rung field $k:V\to\mathbb{Z}$, define the raised field by $(\mathrm{shiftUp}\,S\,k)(v)=k(v)+1$ if $v\in S$, and $k(v)$ otherwise.
background
Phase 59 works on the integer rung field $k:V\to\mathbb{Z}$ that the recognition cost meter actually charges, not on real-valued mean moves. The standing invariant is UnitStep: every edge changes the rung by at most one. Phase 56 made the graded cost law depend on that invariant; Phase 58 showed that a blind global claim that real pair-resolve preserves it is false.
The live engine descends (or raises) a region by exactly one integer rung when a distinction is forced. shiftDown lowers every cell in a set $S$ by one; this definition is the dual raise. Edges with both ends inside $S$ or both outside keep their gap automatically; only cut edges need a separate criterion.
The module's positive half is that top-rung descent (and, dually, bottom-rung raise) discharges the cut condition unconditionally, so the unit-step invariant and the Phase-56 cost law survive the natural parameter-free relaxation move.
proof idea
Pure definition: pointwise conditional. On $v$ with $S,v$, return $k,v+1$; otherwise return $k,v$. No lemmas. Downstream one-liners shiftUp_pos and shiftUp_neg just unfold the if_pos / if_neg cases.
why it matters
Supplies the dual move used by shiftUp_bot_unitStep: if $m$ lower-bounds every rung on the edge set and $S$ is the bottom level ${v:k(v)=m}$, raising $S$ by one preserves UnitStep unconditionally (a bottom cell's neighbour sits exactly one rung up, so the cut gap becomes $0$). That is the dual of shiftDown_top_unitStep and closes the positive half of Phase 59 for the raise direction.
Together with the top-descent theorems, it answers the open item left by Phases 56–58: the active integer dynamics preserves the unit-step graded-rung invariant cycle to cycle when the move is the forced extremal (top descend / bottom raise) update, so the cost meter stays theorem-backed. The necessity counterexample ckLevels_descend_min_breaks shows non-extremal raises/descents can break the gap-one law, so the dual pair of extremal moves is the precise safe class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.