chain3Levels_f0
plain-language theorem explainer
On the three-site counterexample chain, the level at the first vertex is exactly 0. Anyone building or citing the unit-step breakage example (levels 0,1,2 before a mean-move) uses this as a simp fact. The proof is pure definitional equality via rfl.
Claim. Let the three-site level map send vertices $0,1,2$ to $0,1,2$ respectively, and let $v_0$ be the first vertex of $\mathrm{Fin}\,3$. Then the level at $v_0$ equals $0$.
background
This module studies whether active mean-move dynamics (pairResolve) automatically preserve the unit-step invariant: adjacent rungs differ by at most one. Phase 56 forced the graded-rung cost law under that invariant; Phase 57 wired it into the runtime cost meter. A global preservation claim is false.
The three-site chain with real levels $0,1,2$ is the standard counterexample seed. The level assignment is the piecewise map on $\mathrm{Fin},3$ sending index $0\mapsto 0$, $1\mapsto 1$, $2\mapsto 2$. The first vertex is the Fin-literal $\langle 0\rangle$. Evaluating that map at the first vertex is the elementary fact recorded here.
Upstream, the local preservation criterion states that a resolve preserves unit-step globally only if every edge touching the resolved pair stays unit-step after the move; disjoint edges are free by the other-endpoint lemma.
proof idea
One-line definitional proof: unfold the level map on the first Fin case and the first-vertex literal; both sides reduce to the real $0$, so rfl closes. Marked @[simp] so later counterexample calculations rewrite automatically.
why it matters
Tiny bookkeeping lemma inside the honest counterexample layer of Recognition cosmology. The module's point is that blind global unit-step preservation under mean-move is false: resolving the first edge of levels $0,1,2$ yields $1/2,1/2,2$, so the second edge gap becomes $3/2$. This simp fact pins the initial level at site 0, which the breakage theorem and the sibling level lemmas for sites 1 and 2 rely on when stating the pre-move configuration.
No parent theorems currently list it in the used-by graph; it is infrastructure for the chain-three unit-step story and for any later audit that the live engine may apply the Phase-56 cost law only after checking the local unit-step side condition. It does not touch the forcing chain T0–T8 or the RCL directly; it sits in the cosmology runtime-cost layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.