f2
plain-language theorem explainer
Names the third vertex of the three-site Fin 3 chain used as the unit-step counterexample. Cosmology and gravity audits cite it when building edges (1,2) and reading the initial level field. The body is the standard Fin constructor with a decide proof that 2 < 3.
Claim. Let $f_2$ be the element $2$ of the finite type $\{0,1,2\}$, i.e. the third site in the ordered three-site chain.
background
The module studies whether active mean-move dynamics (pairResolve) preserves the real-valued unit-step invariant: adjacent rungs differ by at most one. Phase 56 forced the graded-rung cost under that invariant; the naive claim that every mean-move keeps it is false.
The counterexample is the three-site chain with sites indexed by $\mathrm{Fin},3$ and initial levels $0,1,2$. The two edges are $(0,1)$ and $(1,2)$. After resolving the first edge the levels become $1/2,1/2,2$, so the second edge has gap $3/2>1$.
This definition is simply the third index. Sibling constants supply the first two indices; together they label vertices, edges, and the case-split level field used throughout the module.
proof idea
Definitional one-liner: package the natural number $2$ as an element of $\mathrm{Fin},3$ via the subtype constructor, discharging $2<3$ by decide. No lemmas are applied.
why it matters
Feeds the edge list of the three-site chain, the simp lemma that the initial level at this site is $2$, the gap computation after resolving $(0,1)$, and the main counterexample theorem that unit-step fails after that mean-move. Those results block a false global "mean-move preserves UnitStep" claim and force the live engine to audit the local unit-step side condition before applying the Phase-56 cost law. Downstream gravity backreaction certificates also mention the same identifier as a dummy index in monotonicity statements; the cosmological role is the primary one. No forcing-chain landmark (T0–T8) is proved here; the declaration is pure scaffolding for the honest counterexample layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.