shiftUp_pos
plain-language theorem explainer
If a vertex lies in the raised set S, the integer-rung field after shiftUp equals the old rung plus one. Cosmology proofs that raise the bottom rung cite this to evaluate the updated field on S. The proof is the standard if_pos reduction of the piecewise definition.
Claim. Let $S$ be a decidable predicate on vertices and $k:V\to\mathbb{Z}$ an integer rung field. For any vertex $v$ with $S(v)$, the raised field satisfies $\mathrm{shiftUp}(S,k)(v)=k(v)+1$.
background
Phase 59 of the cosmology stack studies integer-rung updates that preserve the unit-step invariant: every edge changes the rung by at most one. The dual of top-rung descent is bottom-rung raise: lift every cell at the global lower bound $m$ by one integer rung.
The update is the piecewise map shiftUp: on $S$ add one to $k$, elsewhere leave $k$ alone. Evaluating that map on a point known to lie in $S$ is the elementary identity recorded here. The ambient setting is the graded-rung cost law of Phase 56, which charges only fields obeying unit-step on the edge set.
proof idea
One-line wrapper: unfold shiftUp and apply if_pos to the hypothesis $S(v)$, which selects the then-branch $k(v)+1$.
why it matters
Feeds shiftUp_bot_unitStep, the dual of top-rung descent: raising the bottom rung set ${v:k(v)=m}$ preserves unit-step unconditionally when $m$ lower-bounds all rungs on $E$. Without this evaluation lemma the cut-edge case analysis cannot pin the post-move gap to zero on raised endpoints.
In the Recognition stack this closes the positive half of Phase 59: the live engine may raise the coarsest bottom rung (or descend the top) and keep the Phase-56 cost meter theorem-backed cycle to cycle. It is the integer dual of the forced one-rung moves tied to the eight-tick / minimal-distinction structure, not a real-valued mean move.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.