translateVertex
plain-language theorem explainer
Translation by a fixed lattice vector t acts as a bijection on the periodic cubic vertex set Z_N^3. Anyone building the translation subgroup of Aut(T_N) cites this equivalence. The inverse is subtraction of t; both sides cancel by the usual Fin-addition identities.
Claim. For $N \ge 1$ and fixed $t \in (\mathbb{Z}/N\mathbb{Z})^3$, the map $v \mapsto v + t$ is a bijection of the periodic cubic vertex set $(\mathbb{Z}/N\mathbb{Z})^3$ onto itself, with inverse $v \mapsto v - t$.
background
The ambient geometry is the periodic Freudenthal torus: vertices are the product type $\mathrm{Fin},N \times \mathrm{Fin},N \times \mathrm{Fin},N$, i.e. the additive group $(\mathbb{Z}/N\mathbb{Z})^3$ under componentwise mod-$N$ addition. The module packages that torus as a path-sum state space element (probe C3) and checks that lattice translations embed into its relabeling automorphisms (probe C6).
This definition is the vertex-level piece of that translation action. Edges and tetrahedra are translated by applying the same shift to the base cell while freezing the local displacement or Freudenthal index. Upstream arithmetic supplies associativity and zero laws for the underlying additive structure used in the inverse checks.
proof idea
Construct the Equiv with forward map $v \mapsto v+t$ and reverse $v \mapsto v-t$. Left inverse: rewrite $v+t-t$ via add_sub_assoc, cancel $t-t$ by sub_self, then add_zero. Right inverse: rewrite subtraction as addition of negation, associate, cancel by neg_add_cancel, finish with add_zero. No geometry beyond the group law on vertices is used.
why it matters
This is the seed map for probe C6 branch (a): translations embed into Aut of the embedded torus. Downstream, translateEdge and translateTet lift the same shift to edges and tets; translateVertex_zero and translateVertex_trans show the map is a group homomorphism into permutations; translationAut conjugates it through the canonical Fin-indexings to obtain an actual automorphism, and injectivity of that embedding yields $|\mathrm{Aut}(T_N)| \ge N^3$ and the measure bound $\mu(T_N) \le 1/N^3$. The module itself makes no continuum or path-sum value claim; it only records the discrete translation action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.