shiftDown_pos

Phase 59 studies the integer rung field $k:V\to\mathbb{Z}$ that the recognition cost meter actually charges. The live engine does not move rungs by real means; it descends a region by exactly one rung when a distinction is forced (T-3 descends one rung at a time). The primitive update is the pointwise map that subtracts one on a chosen set $S$ and leaves the complement fixed.

That map is defined by a decidable case split: on $S$ send $k(v)$ to $k(v)-1$, otherwise leave $k(v)$ alone. The present lemma records the positive branch of that split. Its dual (the negative branch) is the companion identity that the field is unchanged off $S$. Together they let later arguments rewrite rung values after a descent without unfolding the definition at every site.

The ambient invariant is UnitStep: every edge changes the integer rung by at most one. Phase 56 made the graded cost law depend on that invariant; Phase 59 asks which integer descents preserve it.

One-line definitional reduction. The descent map is fun v => if S v then k v - 1 else k v. Under the hypothesis $S,v$, if_pos selects the then-branch and yields equality with $k(v)-1$. No further lemmas are required.

This is the elementary rewrite used by the two main preservation theorems of the module. The local cut criterion (shiftDown_unitStep_of_cut) case-splits on whether each endpoint of an edge lies in $S$; on the in-$S$ side it rewrites the post-move rung via this identity. The unconditional top-rung theorem (shiftDown_top_unitStep) applies the cut criterion to $S={v:k(v)=M}$ and again needs the in-$S$ evaluation to show cut gaps collapse to zero.

In the broader Recognition chain this closes the positive half of the Phase 56/57/58 story: the cost meter is theorem-backed along the forced top-rung descent, even though a blind real-valued mean move does not preserve unit-step (Phase 58). The lemma itself is pure bookkeeping, but without it the cut and top-rung arguments cannot evaluate the updated field on the descended region.