chain3Edges
plain-language theorem explainer
Defines the edge list of the three-site path graph 0—1—2 on Fin 3, namely the pairs (0,1) and (1,2). Cosmology proofs cite it as the fixed interaction skeleton for the Phase-58 unit-step counterexample. The body is a two-edge list literal built from the site indices f0, f1, f2.
Claim. Let the three sites be the elements of $\mathrm{Fin}\,3$. The three-site chain edge list is $E_3 = \{(0,1),\,(1,2)\}$.
background
This module studies whether active mean-move dynamics (pairResolve) preserves the real-valued unit-step invariant: adjacent rungs differ by at most one in absolute value. Phase 56 forced the graded-rung cost law under that invariant; Phase 57 wired it into the runtime cost meter. A global claim that every mean-move preserves unit-step is false.
The honest layer splits into a local preservation criterion (every edge touching the resolved pair stays within gap one after the move) and an explicit three-site counterexample. The sites are named f0, f1, f2 as the three elements of Fin 3. This definition supplies the fixed edge skeleton those theorems quantify over: the path connecting 0 to 1 to 2.
proof idea
Pure data definition: the list literal [(f0, f1), (f1, f2)] with no proof obligations. The three site constants are the standard Fin 3 constructors ⟨0, _⟩, ⟨1, _⟩, ⟨2, _⟩.
why it matters
Feeds the Phase-58 honesty package. Downstream, chain3_unitStep proves the initial levels 0,1,2 are unit-step on this edge list; chain3_pairResolve_breaks_unitStep shows that resolving the first edge yields levels 1/2, 1/2, 2 so the second edge has gap 3/2 and unit-step fails; t58_unitStep_preservation_honest packages the local criterion plus this counterexample as the headline that blind global preservation is false.
Without a fixed edge list the counterexample cannot be stated as a theorem. The construction is local to Recognition equilibrium dynamics on graded rungs; it does not touch the T0–T8 forcing chain, RCL, or the alpha band, but it gates safe use of the Phase-56 cost law in live cosmology updates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.