translateTet_apply
plain-language theorem explainer
Translating a periodic Freudenthal tetrahedron by a lattice vector moves only the cubic cell index and leaves the local tet type fixed. Anyone checking the Z_N^3 action on the torus image (probe C6) cites this as the computational form of that action. The equality is definitional: it unfolds the product-congruence construction of the translation equivalence.
Claim. Let $N \ge 1$. For any lattice vector $t \in (\mathbb{Z}/N\mathbb{Z})^3$ and any periodic tetrahedron $p = (v,k)$ with cell vertex $v$ and local Freudenthal index $k \in \{0,\ldots,5\}$, translation by $t$ sends $p$ to $(v+t,\,k)$.
background
The ambient geometry is the periodic Freudenthal torus on the cubic lattice $(\mathbb{Z}/N\mathbb{Z})^3$. Vertices are triples in $\mathrm{Fin},N \times \mathrm{Fin},N \times \mathrm{Fin},N$. A periodic tetrahedron is a pair (cell vertex, local type): one of the six Freudenthal tets inside each cubic cell, so the type lives in $\mathrm{Fin},6$.
Translation by a lattice vector $t$ is defined on tetrahedra by acting on the cell factor via the vertex translation equivalence and leaving the local type alone (product congruence with the identity on $\mathrm{Fin},6$). Componentwise addition on $\mathrm{Fin},N$ is modular, via the bit-addition helper used throughout the torus module.
This file is the Seven Gaps Phase 2b path-sum probe lane. It attaches the canonical periodic torus to the scoped BoundedComplex state space and checks that lattice translations embed into relabeling automorphisms. It makes no continuum, measure, or path-sum value claims.
proof idea
One-line term proof by rfl. The translation map on tetrahedra is definitionally the product congruence of vertex translation with the identity on the six local types, so applying it to a pair $(v,k)$ is definitionally $(v+t,,k)$.
why it matters
This simp lemma is the computational face of tetrahedron translation inside probe C6 (Aut vacuity / translation embedding). The module records that $\mathbb{Z}_N^3$ embeds into the relabeling automorphisms of the torus image: the translation map is injective, sends zero to the identity, and sends sums to composites. Downstream consequences named in the module doc include the lower bound $|\mathrm{Aut}(T_N)| \ge N^3$ and the measure upper bound $\mu(T_N) \le 1/N^3$.
No declaration currently lists this lemma as a direct dependant in the graph snapshot, but it is the natural reduction step whenever a proof must evaluate how a translated tet sits in the periodic complex. It does not touch the forcing chain (T0–T8), RCL, or continuum gravity claims; it only stabilizes the discrete Aut bookkeeping for the path-sum probes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.