shiftUp_bot_unitStep
plain-language theorem explainer
Raising every cell at a global lower bound rung m by one preserves the unit-step adjacency law on any edge set. Cosmology and graded-cost authors cite it as the dual of top-rung descent: the parameter-free bottom raise is always safe. The proof is a four-way case split on whether each endpoint sits at m, using the lower bound to force cut neighbours to m+1.
Claim. Let $k:V\to\mathbb{Z}$ be a rung field and $E$ a finite set of ordered pairs. Suppose every adjacency changes $k$ by at most one (unit-step), and $m\in\mathbb{Z}$ is a lower bound on $k$ at both endpoints of every edge in $E$. Raising by one every vertex with $k(v)=m$ yields a new field that is still unit-step on $E$.
background
Phase 59 studies integer-rung updates that the live recognition engine actually performs: descend (or raise) a region by exactly one rung when a distinction is forced. The invariant that must survive is UnitStep: across every edge, the integer gap lies in ${-1,0,+1}$. That is the forced minimal-distinction property from GradedRungCost; the cost meter of Phase 56/57 is only theorem-backed while it holds.
The dual move shiftUp S k adds one to $k$ on the predicate $S$ and leaves other vertices fixed. The companion result for top-rung descent shows that lowering the global maximum is always safe. Here $S$ is the bottom level ${v\mid k(v)=m}$ under a global lower bound $m$ on all endpoints in $E$. Module framing: this is the positive integer half complementary to Phase 58's negative real-mean result; top descent is necessary as well as sufficient, and bottom raise is the symmetric dual.
proof idea
Fix an edge $p\in E$. The lower-bound hypothesis gives $m\le k(p_1)$ and $m\le k(p_2)$; unit-step on the old field gives the three-way gap. Case-split on whether each endpoint equals $m$.
Both raised: rewrite with shiftUp_pos twice; the $+1$ cancels in the difference, so the old gap is unchanged. First raised, second not: lower bound plus inequality forces $k(p_2)=m+1$ by omega; after raise the gap is $0$. Symmetric case for the other endpoint. Neither raised: both shiftUp_neg, old gap untouched. In every branch the new gap stays in ${-1,0,+1}$.
why it matters
Closes the dual half of Phase 59's positive story: not only does forced top-rung descent preserve unit-step (so the Phase-56 graded cost law applies next cycle), but raising the global bottom rung is likewise unconditional. The module doc lists this explicitly beside shiftDown_top_unitStep and the necessity counterexample that descending a non-top cell can break the invariant on the chain $0,1,2$.
In the Recognition framework this sits under the integer dynamics that implement T-3 one-rung steps and keep the minimal-distinction law the cost meter charges. No downstream dependents are wired yet in the graph; the declaration is the symmetry twin that makes the top/bottom story complete rather than one-sided. Honest status remains fully proved, zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.