translateTet
plain-language theorem explainer
Lattice translation by a vector t acts on periodic tetrahedra by shifting the cubic cell and leaving the local Freudenthal index fixed. Anyone building translation automorphisms of the embedded Freudenthal torus (probe C6) cites this equivalence. It is the product of vertex translation with the identity on the six tet types.
Claim. For $N \ge 1$ and $t \in (\mathbb{Z}/N\mathbb{Z})^3$, translation by $t$ is the equivalence of periodic tetrahedra sending $(v,i)\mapsto(v+t,i)$, where $v$ is the cubic cell and $i\in\{0,\ldots,5\}$ is the local Freudenthal tetrahedron index inside that cell.
background
The module records path-sum probes only: it attaches the canonical periodic Freudenthal torus to the scoped BoundedComplex state space and checks that the translation group embeds into relabeling automorphisms. No continuum, measure, or path-sum value is claimed.
A periodic vertex is a triple in $(\mathbb{Z}/N\mathbb{Z})^3$. A periodic tetrahedron is a pair (cell, local index): the cell is such a vertex, and the index runs over the six Freudenthal tetrahedra that fill one cubic cell. Vertex translation by $t$ is componentwise addition mod $N$, with inverse subtraction; that equivalence is already defined upstream.
This definition lifts that cell translation to tetrahedra while freezing the local index, matching the geometric picture that lattice shifts move cells rigidly and do not reshuffle the six tet types inside a cell.
proof idea
One-line definition: product congruence of the existing vertex translation equivalence with the identity equivalence on Fin 6. No further lemmas; the pair structure of periodic tetrahedra (cell × local index) makes the construction definitional.
why it matters
Probe C6 asks whether translations embed into automorphisms of the torus image in the path-sum state space. This map is the tet component of that embedding: translationAut conjugates it through the canonical finite indexings, and translationAut_tEquiv records the projection onto the tet permutation as exactly this conjugation.
Sibling facts close the group action: translation by zero is the identity, and translations compose (translateTet_trans). Those feed injectivity of translationAut, the lower bound $|\mathrm{Aut}(T_N)|\ge N^3$, and the consequent upper bound $\mu(T_N)\le 1/N^3$. The declaration is scaffolding for the automorphism landmine check, not a gravity or continuum claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.