ckLevels
plain-language theorem explainer
Defines the integer rung assignment on the three-site path graph as the position index itself: sites carry rungs 0, 1, and 2. Cosmology proofs cite it as the minimal concrete field on which unit-step holds and on which a non-top single-cell descent breaks that invariant. The body is the identity cast Fin 3 → ℤ.
Claim. Let the three-site chain have vertices $\{0,1,2\}$. Define the integer rung field $k:\{0,1,2\}\to\mathbb{Z}$ by $k(i)=i$. Equivalently, the rung at each site is its position index along the chain.
background
Phase 59 of the Recognition cosmology stack studies whether integer rung updates preserve the minimal-distinction invariant UnitStep: every edge changes the integer rung by at most one. That invariant is the hypothesis under which Phase 56's graded recognition-cost law is well-defined, and Phase 57 wires it into the runtime cost meter.
The live engine does not move rungs by real-valued means; it descends a region by exactly one rung when a distinction is forced. The module therefore works with fields $k:V\to\mathbb{Z}$ and with the elementary shift that subtracts one on a chosen set $S$. The three-site chain with consecutive rungs is the smallest nontrivial unit-step example, and the natural place to test whether descending a non-top cell is safe.
This definition is that example field: on $\mathrm{Fin},3$ the rung equals the vertex index, so the ordered edges $0$--$1$ and $1$--$2$ each have gap one.
proof idea
Pure definition: map each $i:\mathrm{Fin},3$ to its underlying natural number cast to $\mathbb{Z}$. No lemmas, no tactics; the term is the identity embedding of the three indices as rungs $0,1,2$.
why it matters
This field is the concrete witness behind the Phase-59 necessity half. Downstream, ckLevels_unitStep decides that the chain is unit-step before any move, and ckLevels_descend_min_breaks shows that descending the bottom cell (rung $0$ to $-1$) opens a gap of $2$ on the edge to rung $1$, so UnitStep fails. The headline t59_rung_descent_preservation packages that counterexample with the positive theorem that top-rung descent always preserves UnitStep under a rung upper bound.
Together with Phase 58 (the real-valued mean move does not preserve unit-step globally), this closes the honest answer: only the forced top-rung descent keeps the graded-rung invariant cycle to cycle, so the Phase-56 cost law remains theorem-backed along the active dynamics. The three-site ladder is the minimal discrete analogue of the phi-ladder rung structure used elsewhere in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.