chain3Levels_f1
plain-language theorem explainer
Evaluating the three-site counterexample level assignment at the middle vertex returns 1. Cosmology proofs that build or simplify the 0-1-2 chain cite this simp fact. The proof is pure reflexivity: the definition of the level map sends Fin-index 1 to the real 1.
Claim. If $L:\mathrm{Fin}\,3\to\mathbb{R}$ is the initial three-site level map with $L(0)=0$, $L(1)=1$, $L(2)=2$, and $v_1$ is the middle site (the unique element of $\mathrm{Fin}\,3$ with value $1$), then $L(v_1)=1$.
background
The module studies whether active mean-move dynamics (pairResolve) preserves the UnitStep invariant: adjacent rungs differ by at most one in real level. Phase 56 forced the graded-rung cost under that invariant; Phase 57 wired it into the runtime cost meter. A global preservation claim is false.
The counterexample is a three-site chain. The level assignment chain3Levels is defined by cases on Fin 3: site 0 has level 0, site 1 has level 1, site 2 has level 2. The name f1 is simply the middle index $\langle 1\rangle\in\mathrm{Fin},3$. Before any resolve step the successive gaps are 1 and 1, so UnitStep holds; after resolving the first edge the levels become $1/2,1/2,2$ and the second gap is $3/2$.
This lemma is the middle evaluation fact for that initial assignment.
proof idea
One-line definitional equality. Unfolding chain3Levels on the constructor f1 = ⟨1, _⟩ matches the middle case arm, which returns the real literal 1; rfl closes the goal. Marked @[simp] so later rewrites of the counterexample reduce automatically.
why it matters
Supports the honest negative result of the module: mean-move dynamics need not preserve UnitStep. The three-site chain with levels 0,1,2 is the concrete witness that resolving the first edge produces a gap of 3/2 on the second edge. This middle-site evaluation is the bookkeeping step that lets the initial configuration be stated and simplified cleanly.
No downstream consumers are recorded yet; sibling facts cover the other two sites and the full chain3_unitStep / break lemmas. In the broader Recognition framework the point is operational, not foundational: the live engine may invoke the Phase-56 graded-rung cost only after a local UnitStep audit. Blind global preservation would be false, so cost accounting in cosmology updates stays conditional on that check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.