chain3Levels
plain-language theorem explainer
The three-site initial level assignment sending vertices 0,1,2 to real values 0,1,2. Cosmology proofs cite it as the starting field for the mean-move counterexample: unit-step before resolution, broken after. Defined by exhaustive cases on Fin 3; no proof content.
Claim. The map $\ell:\{0,1,2\}\to\mathbb{R}$ defined by $\ell(0)=0$, $\ell(1)=1$, and $\ell(2)=2$.
background
Phase 56 forced a graded-rung cost law under the minimal-distinction invariant UnitStep: adjacent rungs differ by at most one in absolute value. Phase 57 wired that law into the runtime cost meter. The natural hope is that active mean-move dynamics (pairResolve) would preserve UnitStep automatically.
That hope is false. This module builds an honest theorem layer around a three-site path whose edges are the consecutive pairs among three Fin-indexed sites. UnitStepReal asks that every edge of a given edge set has absolute level gap at most 1. The present definition supplies the initial real-valued levels on those three sites: the arithmetic progression 0, 1, 2.
Sibling edge data (chain3Edges) and the mean-move operator pairResolve act on this field. After resolving the first edge, the second edge gap becomes 3/2, which violates the invariant.
proof idea
Pure definition by cases on Fin 3: the representative 0 maps to 0, 1 to 1, and 2 to 2. No tactics, no lemmas. Downstream simp lemmas are just rfl unfoldings of these three clauses.
why it matters
This is the seed configuration for the module's central negative result. It feeds chain3_unitStep (the field is unit-step before any move), chain3_resolved_second_gap (after resolving the first edge the second gap is 3/2), and the counterexample theorem chain3_pairResolve_breaks_unitStep: mean-move need not preserve UnitStep.
That counterexample blocks a false global lemma and forces the correct local criterion pairResolve_unitStep_of_local: preservation holds only when every edge touching a resolved endpoint still has gap at most one after the move. The honest status note in the module doc is the point: the live engine may use the Phase-56 cost law only after auditing that local condition. Downstream t58_unitStep_preservation_honest packages the same honesty claim for the broader chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.