f1
plain-language theorem explainer
Names the middle vertex of a three-site chain as the Fin-3 index 1. Cosmology and gravity audits cite it when building the 0--1--2 edge list and evaluating levels after a mean-move. The body is a one-line subtype constructor discharged by decide.
Claim. Let $f_1$ be the element $1$ of the three-point index set $\{0,1,2\}$ (equivalently $\mathrm{Fin}\,3$).
background
The module studies whether active recognition dynamics preserve the unit-step invariant: adjacent rungs differ by at most one in absolute value. Phase 56 forced the graded-rung cost under that invariant; Phase 57 wired it into the runtime cost meter. The natural global claim that mean-move resolution (pairResolve) always preserves unit-step is false.
The honest layer isolates a local criterion (every edge touching a resolved endpoint stays within gap one after the move) and a concrete counterexample on a three-site chain with levels $0,1,2$. Resolving the first edge yields levels $1/2,1/2,2$, so the second edge has gap $3/2$.
This definition supplies the middle index of that chain. Sibling indices $f_0$ and $f_2$ complete the vertex set; the edge list is then $(f_0,f_1)$ and $(f_1,f_2)$.
proof idea
Definitional one-liner: construct the subtype element $\langle 1, _\rangle : \mathrm{Fin},3$ and discharge the bound $1 < 3$ by decide. No lemmas are applied.
why it matters
Without a named middle vertex the three-site counterexample cannot be stated. Downstream, chain3Edges builds the path $0$--$1$--$2$ from pairs involving this index; chain3Levels_f1 records that the initial level at this site is $1$; chain3_resolved_second_gap and chain3_pairResolve_breaks_unitStep use it to prove the post-move gap $3/2$ and thereby refute global unit-step preservation.
The Phase-58 headline t58_unitStep_preservation_honest packages the local criterion plus this necessity witness. External uses appear in gravity backreaction audit predictions and in lepton-generation tau-step exclusivity, where the same Fin-3 labeling is reused as a compact three-point test bed. The declaration itself carries no physics content; it is scaffolding for the honest negative result that blocks a false global lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.