chain3_unitStep
plain-language theorem explainer
The three-site chain with levels 0, 1, 2 and edges (0,1), (1,2) satisfies the real unit-step invariant: every edge gap is at most 1. Cosmology and recognition-dynamics work cites this as the pre-move baseline for the counterexample that mean-move resolution can break unit-step. The proof is a two-case membership check on the edge list, discharged by norm_num.
Claim. Let $x : \mathrm{Fin}\,3 \to \mathbb{R}$ be the level assignment $x(0)=0$, $x(1)=1$, $x(2)=2$, and let $E = \{(0,1),(1,2)\}$. Then for every edge $e \in E$, $|x(e_1) - x(e_2)| \le 1$.
background
Phase 56 forced a minimal-distinction invariant: adjacent rungs differ by at most one. The real-valued form used here, UnitStepReal, says that every listed edge has absolute level gap at most 1. That formulation is needed because the active mean-move pairResolve can produce half-rungs even from integer inputs.
This module sits in the cosmology recognition-equilibrium layer. The honest claim is not that mean-move always preserves unit-step (it does not). Instead one proves a local preservation lemma under an edge-touching side condition, and separately records a three-site counterexample.
The chain data are elementary: levels $0,1,2$ on three sites, edges $(0,1)$ and $(1,2)$. The present theorem is the pre-resolution half of that counterexample setup: the configuration is unit-step before any move.
proof idea
Unfold the definition of the real unit-step predicate and introduce an arbitrary edge $e$ in the chain edge list. Simplify membership in chain3Edges, which is exactly the two-element list $[(0,1),(1,2)]$. Case-split on that membership: either $e = (0,1)$ or $e = (1,2)$. In each case the absolute difference of the corresponding levels is $|0-1|=1$ or $|1-2|=1$, both $\le 1$, discharged by norm_num. No external lemmas are required beyond list membership and arithmetic.
why it matters
This is the baseline fact for the module's main negative result: after resolving the first edge, levels become $1/2,1/2,2$ and the second edge has gap $3/2$, so unit-step fails. Without a proved pre-move unit-step configuration, that counterexample would be incomplete.
In the Recognition framework the graded-rung cost law (Phase 56) is only safe to apply when unit-step holds. The module doc is explicit: the live engine may use that cost law only after auditing or proving the local unit-step condition for the update. A blind global "mean-move preserves UnitStep" lemma would be false. This theorem pins the honest pre-state of the three-site witness.
No downstream consumers are wired yet (used_by is empty); the declaration exists as the first half of the counterexample pair inside this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.