ckLevels_unitStep
plain-language theorem explainer
The three-site integer chain with rungs 0,1,2 satisfies the unit-step (minimal-distinction) invariant on its two edges. Cosmology and graded-cost work cite this as the baseline configuration before any descent move. The proof is a one-line unfold-and-decide check on a finite Finset.
Claim. On the three-vertex chain with edges $0$--$1$ and $1$--$2$, the integer rung field $k(i)=i$ satisfies $k(u)-k(v)\in\{0,+1,-1\}$ for every edge $(u,v)$.
background
Phase 56 introduced UnitStep: a rung field $k:V\to\mathbb{Z}$ posts only single-rung distinctions across an edge set $E$, i.e. every adjacency changes the rung by at most one. The live engine maintains this because T-3 descends one rung at a time; the graded recognition-cost law of Phase 56/57 is only licensed when the invariant holds.
Phase 58 showed that a blind global claim "dynamics preserves unit-step" is false for real-valued mean moves. Phase 59 (this module) supplies the positive half for the object the cost meter actually charges: the integer rung field. The natural parameter-free relaxation is top-rung descent; the module proves that move preserves unit-step, and supplies a necessity counterexample that non-top descent need not.
The present declaration is the baseline: the ordered chain edges $0$--$1$--$2$ with levels $0,1,2$ already satisfy unit-step before any move. That configuration is the substrate for the necessity counterexample that follows in the file.
proof idea
One-line finite check. Unfold the definition of unit-step (universal quantification over edges of a difference in ${0,+1,-1}$), then decide discharges the Prop on the concrete two-edge Finset and the concrete level map $i\mapsto i$ on Fin 3. No lemmas are applied beyond decidability of integer arithmetic on a finite domain.
why it matters
This is the seed configuration for Phase 59's necessity story. Immediately after it, the module records that descending the bottom cell of the same chain sends rung $0$ to $-1$, so the edge to the rung-$1$ neighbour has gap $2$ and unit-step fails. That counterexample shows the top-rung hypothesis of the main preservation theorem is necessary, not cosmetic.
Together with shiftDown_top_unitStep and exists_top_descent_unitStep, the package closes the item "the active dynamics preserves the unit-step graded-rung invariant cycle to cycle" with the exact truth: the generic move does not (Phase 58), but forced top-rung descent does (Phase 59), so the Phase-56 cost meter is theorem-backed along that update. No downstream dependents are wired yet; the declaration is local scaffolding for the counterexample and the top-descent theorems in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.