chain3Levels_f2
plain-language theorem explainer
On the three-site chain with initial levels 0, 1, 2, the third site has level exactly 2. Cosmology proofs that assemble the unit-step counterexample cite this as a simp fact. The proof is pure definitional reflexivity from the case-split level map.
Claim. For the initial three-site level assignment $\ell:\{0,1,2\}\to\mathbb{R}$ given by $\ell(0)=0$, $\ell(1)=1$, $\ell(2)=2$, one has $\ell(2)=2$.
background
This module sits in the cosmology layer after Phase 56 forced the graded-rung cost under the minimal-distinction invariant UnitStep (adjacent rungs differ by at most one). The natural hope that active mean-move dynamics (pairResolve) would preserve UnitStep automatically is false; the module records the honest local preservation theorem and an explicit three-site counterexample.
The counterexample chain has sites indexed by $\mathrm{Fin},3$ and initial real levels defined by cases: site 0 maps to 0, site 1 to 1, site 2 to 2. The three indices are packaged as named constants so later edge and resolution lemmas can refer to them cleanly.
This lemma is the third evaluation fact for that level assignment. Together with the parallel facts at sites 0 and 1 it feeds the pre-move unit-step check and the post-move gap computation that breaks the invariant.
proof idea
One-line term proof by rfl. The level map is defined by pattern-matching on $\mathrm{Fin},3$; the third index is definitionally $\langle 2,_\rangle$, so the matching branch is the constant 2 and equality holds by definitional reduction. Marked @[simp] for automatic unfolding in later chain lemmas.
why it matters
Infrastructure for the three-site counterexample that shows mean-move resolution need not preserve UnitStep. After resolving the first edge, levels become $1/2,1/2,2$, so the second edge has gap $3/2$ and the invariant fails. That forces the live engine to audit or prove the local unit-step side condition before invoking the Phase-56 graded-rung cost law; a blind global preservation lemma would be false.
No downstream used_by edges are recorded yet, but the sibling suite (chain3Levels_f0, chain3Levels_f1, chain3_unitStep, and the break lemma) makes the role clear: pure bookkeeping so the counterexample is a theorem, not a numerical observation. Not itself a forcing-chain landmark (T0–T8); it is local honesty in the cosmology runtime layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.