f0
plain-language theorem explainer
Labels the first vertex of the three-site chain on Fin 3, namely the index 0. Cosmology and geometry proofs that build the 0--1--2 counterexample cite it as a named endpoint. The body is the subtype constructor ⟨0, _⟩ with a decide proof that 0 < 3.
Claim. Define $f_0 \in \mathrm{Fin}\,3$ by $f_0 := 0$ (the unique element of $\{0,1,2\}$ equal to zero).
background
Phase 56 established the graded-rung cost law under the minimal-distinction invariant UnitStep: adjacent rungs differ by at most one. Phase 57 wired that law into the runtime cost meter. The natural next claim, that active mean-move dynamics (pairResolve) automatically preserves the invariant, is false.
This module records the honest layer: a local preservation criterion (every edge touching the resolved pair stays within gap one after the move) and an explicit three-site counterexample. The real-valued unit-step predicate UnitStepReal asserts that every listed edge $e$ satisfies $|x(e_1)-x(e_2)|\le 1$. EdgeTouches marks edges that share an endpoint with the resolved pair.
The counterexample lives on Fin 3 with edges $0$--$1$--$2$ and initial levels $0,1,2$. Named vertex indices $f_0,f_1,f_2$ make those constructions readable and simp-friendly.
proof idea
Pure definition: the Fin subtype constructor packing the natural number 0 with a decide proof of the bound $0 < 3$. No lemmas are applied.
why it matters
Supplies the first endpoint for chain3Edges (the list $[(f_0,f_1),(f_1,f_2)]$) and for the simp lemma chain3Levels_f0 (initial level at $f_0$ is 0). Those feed the gap computation chain3_resolved_second_gap and the counterexample theorem chain3_pairResolve_breaks_unitStep: after resolving $(f_0,f_1)$, levels become $1/2,1/2,2$ and the second edge has gap $3/2>1$.
The Phase-58 headline t58_unitStep_preservation_honest packages the local criterion together with this necessity witness. Downstream geometry (IncidenceEdgeSlotPartition, Regge edge-slot sums) reuses the same Fin-3 index style for local edge bookkeeping. In the Recognition framework this blocks a false global "mean-move preserves UnitStep" lemma, so the Phase-56 cost law may be applied to live updates only after the local post-move audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.