translateEdge_apply
plain-language theorem explainer
On the N×N×N periodic Freudenthal torus, translating a positive-displacement edge by a vertex t shifts only the base vertex by t and leaves the Fin-7 displacement index unchanged. Anyone building translation automorphisms of freudenthalBoundedComplex or checking Aut-embedding for path-sum probe C6 will cite this. The equality is definitional (rfl), so it is a simp-ready unfolding lemma.
Claim. Let $N\ge 1$. For any torus vertex $t\in(\mathbb{Z}/N)^3$ and any positive-displacement periodic edge $e=(b,d)$ (base $b$, displacement index $d\in\{0,\ldots,6\}$), the translate of $e$ by $t$ is exactly $(b+t,\,d)$.
background
The ambient geometry is the canonical periodic Freudenthal torus: vertices are Vertex N N N ≅ Fin N × Fin N × Fin N under componentwise mod-N addition; a PeriodicEdge is a positive-displacement edge given by a base vertex and one of seven cube displacements (Fin 7).
This module (Seven Gaps, Phase 2b lane O) is probe-only. It attaches that torus to the scoped path-sum state space as freudenthalBoundedComplex N (probe C3) and checks that the translation group embeds into relabeling automorphisms (probe C6). No continuum, measure, or path-sum value is claimed.
Edge translation is the edge half of the cellwise action used to build translationAut: move the base cell by t, keep the local Freudenthal displacement label.
proof idea
Term proof by rfl. The statement is the definitional expansion of translateEdge on the structure constructor of PeriodicEdge, so both sides reduce to the same pair ⟨e.base + t, e.disp⟩.
why it matters
Probe C6 records that translations embed into Aut of the torus image: translationAut is injective, sends 0 to id, and sends sums to composites, yielding |Aut(T_N)| ≥ N³ and μ(T_N) ≤ 1/N³. This simp lemma is the edge-action identity those maps rest on (base shifts, displacement fixed).
It sits in the gravity Seven Gaps path-sum probe lane, not in the T0–T8 forcing chain. Downstream used_by is empty in the graph snapshot; the lemma is local infrastructure for the Aut-embedding landmine check rather than a flag-bearing continuum claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.