translateEdge_trans
plain-language theorem explainer
Edge translations on the periodic Freudenthal torus compose: translating by t then by s equals translating by t+s. Cited by anyone packaging the Z_N^3 action as a monoid homomorphism into torus automorphisms. Proof is extensionality of equivalences plus associativity of vertex addition.
Claim. Let $N\ge 1$ and let $t,s$ be vertices of the $N\times N\times N$ periodic cubic lattice. Writing $\tau_u$ for translation of positive-displacement periodic edges by a vertex $u$, one has $\tau_t\circ\tau_s=\tau_{t+s}$.
background
The ambient geometry is the canonical periodic Freudenthal torus: vertices are Vertex N N N $=\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$ under componentwise mod-$N$ addition, and a positive-displacement periodic edge is a pair (base vertex, one of seven cube displacements). Translation of an edge by a lattice vector shifts only the base; the displacement label is fixed.
This module is a non-flag-bearing path-sum probe lane. It attaches the torus to the scoped BoundedComplex state space and checks that the translation group embeds into relabeling automorphisms (PROBE C6), without claiming measures, continuum limits, or path-sum values.
Upstream, the only arithmetic fact needed is associativity of addition on the vertex type (and its foundation ancestors). The edge type and the pointwise translation map are the local geometric primitives.
proof idea
Term-mode via Equiv.ext: it suffices that the two equivalences agree on every periodic edge $e$. Both sides keep the same displacement label; the bases are $e.\mathrm{base}+t+s$ versus $e.\mathrm{base}+(t+s)$. One rewrite by add_assoc closes the equality.
why it matters
This is the edge half of the translation composition law used by translationAut_add, whose doc-comment states the group-hom law: translation by $t+s$ is the composite relabeling, so together with the zero law one obtains a monoid-hom package $\mathbb{Z}_N^3\to\mathrm{Aut}(T_N)$ under relabel composition.
That package is the content of PROBE C6 branch (a) in the module doc: translations embed. Immediate consequences recorded downstream are the cardinality lower bound $N^3\le|\mathrm{Aut}(T_N)|$ and the path-sum measure upper bound $\mu(T_N)\le 1/N^3$. No continuum or gravity claim is made here; the lemma only keeps the discrete symmetry bookkeeping honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.