translateTet_trans
plain-language theorem explainer
Translation maps on tetrahedra of the periodic Freudenthal torus compose: shifting by t then by s equals shifting by t+s. Anyone building the Z_N^3 embedding into Aut(T_N) cites this. The proof is a one-step Equiv.ext plus associativity of vertex addition.
Claim. For any $N \ge 1$ and vertices $t,s \in (\mathbb{Z}/N\mathbb{Z})^3$, the composition of the tetrahedron-translation equivalences satisfies $\mathrm{translateTet}(t)\circ\mathrm{translateTet}(s)=\mathrm{translateTet}(t+s)$.
background
The ambient object is the canonical periodic Freudenthal torus at side $N$: vertices are $\mathrm{Vertex},N,N,N=\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$ under componentwise mod-$N$ addition. Tetrahedra of the triangulation are pairs (base vertex, tet type); translating a tet by $t$ adds $t$ to the base vertex and leaves the type fixed.
This module is the Seven Gaps Phase 2b path-sum probe lane. It attaches the torus to the scoped BoundedComplex state space (probe C3) and checks that lattice translations embed into relabeling automorphisms (probe C6). No continuum, measure, or path-sum value is claimed.
Upstream, associativity of addition on the vertex group is the only arithmetic input; several foundation-level add_assoc lemmas supply it for the underlying additive structure.
proof idea
Term-mode via Equiv.ext: two equivalences on tetrahedra agree if they agree pointwise. On a pair $p=(v,\tau)$, both sides act as $(v+t+s,\tau)$ versus $(v+(t+s),\tau)$. A single rw [add_assoc] closes the equality. No case split on tet type is needed because translation ignores the type coordinate.
why it matters
Feeds translationAut_add, the group-hom law: translation by $t+s$ is the composite relabeling under Relabel.trans. Together with translationAut_zero and injectivity, that packages $\mathbb{Z}_N^3\hookrightarrow\mathrm{Aut}(T_N)$.
In the probe C6 landmine check this is the composition half of the monoid-hom package. Downstream consequences recorded in the module doc include $|\mathrm{Aut}(T_N)|\ge N^3$ and the crude measure bound $\mu(T_N)\le 1/N^3$. The result is scaffolding for the automorphism side of the path-sum state space, not a continuum gravity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.