translateEdge_endpoints
plain-language theorem explainer
On the periodic cubic lattice of side N, translating a positive-displacement edge by a lattice vector t shifts both of its endpoints by t. Anyone building translation automorphisms of the Freudenthal torus image cites this. The proof reduces endpoint definitions to the right-translation identity for addBits.
Claim. Let $N \ge 1$ and let $t$ be a vertex of the $N \times N \times N$ periodic cube. For any positive-displacement periodic edge $e$, the two endpoints of the edge translated by $t$ equal the two endpoints of $e$, each translated by $t$: $(\mathrm{translate}\, e\,\mathrm{by}\, t).\mathrm{ends} = (e.\mathrm{start}+t,\, e.\mathrm{end}+t)$.
background
The ambient geometry is the periodic Freudenthal torus: vertices are $V = (\mathbb{Z}/N)^3$, and a positive-displacement edge is a pair (base vertex, displacement index in $\mathrm{Fin},7$). The seven displacements are the nonzero positive cube steps (axis and face-diagonal), decoded by dispBits into three booleans and applied by addBits, which increments selected coordinates by one mod $N$. Endpoints of such an edge are therefore (base, base plus the decoded displacement).
This module is a non-flag-bearing probe lane: it attaches the canonical periodic torus to the scoped path-sum state space BoundedComplex and checks that the translation group embeds into relabeling automorphisms. No continuum, measure, or path-sum value is claimed. The present lemma is the edge half of the translation-commutation facts needed for that embedding.
proof idea
Unfold both sides via the definition of endpoints: left-hand side is (base+$t$, addBits(base+$t$, bits of disp)); right-hand side is (base+$t$, addBits(base, bits)+$t$). The first components match definitionally. The second components are equal by the already-proved right-translation law addBits_add_right, which says adding $t$ after applying the bit increments equals applying the increments to the already-translated base. One rw finishes the proof; no case split on the seven displacements is required.
why it matters
PROBE C6 asks whether translations of $\mathbb{Z}_N^3$ embed into $\mathrm{Aut}$ of the torus image inside BoundedComplex. The parent construction translationAut builds that embedding by conjugating vertex and edge translations through the canonical Fin-indexings; its edge map is translateEdge, and both Aut commutation fields are proved from addBits-translation compatibility. This lemma is exactly the edge-endpoint half of that compatibility: translating then reading endpoints equals reading endpoints then translating.
Downstream consequences recorded in the module (once the Aut map is assembled) include injectivity of the translation embedding, $N^3 \le |\mathrm{Aut}(T_N)|$, and the measure bound $\mu(T_N) \le 1/N^3$. The result is local lattice algebra, not a continuum gravity claim; it closes a landmine check that the Aut group is at least as large as the obvious translation group rather than collapsing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.