EdgeTouches
plain-language theorem explainer
An edge touches a resolved pair when either endpoint equals one of the two vertices being mean-moved. Cosmology proofs that audit unit-step after `pairResolve` cite this predicate to isolate the edges that can change. The body is a four-way disjunction on the ordered pair's components.
Claim. For $n \in \mathbb{N}$, indices $i,j \in \{0,\ldots,n-1\}$, and an ordered edge $e=(e_1,e_2)$, the edge touches the pair $(i,j)$ when $e_1=i$ or $e_1=j$ or $e_2=i$ or $e_2=j$.
background
Phase 56 established the graded-rung cost law under the minimal-distinction invariant that adjacent rungs differ by at most one (unit-step). Phase 57 wired that law into the runtime cost meter. The natural hope that active mean-move dynamics automatically preserves unit-step is false; this module records the honest local criterion and a three-site counterexample.
The mean-move itself is pairResolve: both endpoints of a coupled pair are sent to their arithmetic mean, the $\sigma=0$, $J$-minimal update the forward dynamics posts each tick. Edges disjoint from the pair are left unchanged (pairResolve_other). Only edges that share a vertex with the resolved pair can have their level gap altered, so the audit surface is exactly those touching edges.
EdgeTouches is the boolean filter naming that surface: an ordered edge touches $(i,j)$ when either of its endpoints is $i$ or $j$.
proof idea
Pure definitional abbreviation: the predicate is the four-way disjunction that the edge's first or second component equals either resolved index. No lemmas are applied; downstream theorems unfold or pattern-match on this Prop.
why it matters
Feeds the local preservation theorem: a mean-move preserves real unit-step on a whole edge list if every touching edge remains within gap one after the move; disjoint edges ride free on the old invariant. The Phase-58 headline packages that criterion with the three-chain counterexample (levels $0,1,2$ become $1/2,1/2,2$, gap $3/2$) to show the local condition is necessary, not cosmetic.
In the Recognition framework this is the audit gate before applying the Phase-56 cost law to an actively updated field. Blind global preservation would be false; the live engine may use the cost law only after checking or proving the touching-edge condition. Ties the cosmology runtime to the forced minimal-distinction structure underlying the graded-rung cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.