translateVertex_apply
plain-language theorem explainer
On the periodic cubic lattice $(\mathbb{Z}/N\mathbb{Z})^3$, translating a vertex $v$ by a lattice vector $t$ is ordinary componentwise modular addition. Anyone assembling the translation automorphisms of the embedded Freudenthal torus cites this identity. The proof is pure definitional equality (`rfl`).
Claim. Let $N\ge 1$ and let $t,v\in(\mathbb{Z}/N\mathbb{Z})^3$. The lattice translation by $t$ acts on vertices by $v\mapsto v+t$ (componentwise addition mod $N$).
background
The ambient space is the periodic cubic vertex set Vertex N N N $\simeq$ $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$, i.e. the additive group $(\mathbb{Z}/N\mathbb{Z})^3$. The module packages the canonical periodic Freudenthal triangulation of the $N$-torus as a path-sum BoundedComplex (Probe C3) and then checks that lattice translations embed into its relabeling automorphisms (Probe C6).
Translation of vertices is the group law of that torus: add the displacement $t$ componentwise mod $N$. The companion edge translation keeps the positive-displacement class and only moves the base vertex. Both are later conjugated through the canonical Fin-indexings to produce an element of Aut of the embedded complex.
The module is explicitly non-flag-bearing: it records provenance and a landmine check only, with no claim on measures, continuum limits, or path-sum values.
proof idea
One-line term proof by rfl. The definition of the vertex translation map is exactly componentwise addition of $t$, so the stated equality holds definitionally and is marked @[simp] for downstream rewriting.
why it matters
This simp lemma is the vertex half of the typed translation used to build translationAut: the automorphism conjugates translateVertex t (and the matching edge map) through the canonical vertex/edge Fin-equivalences of the embedded Freudenthal complex. Downstream, translationAut_injective recovers $t$ from the image of the origin under the vertex permutation, so distinct translations give distinct relabelings.
Together these close Probe C6 branch (a): the translation group $\mathbb{Z}_N^3$ embeds into $\mathrm{Aut}(T_N)$, yielding the cardinality lower bound $N^3\le|\mathrm{Aut}(T_N)|$ and the measure upper bound $\mu(T_N)\le 1/N^3$. In the Seven Gaps gravity lane this is the cheap honest check that the torus image is not automorphism-vacuous before any path-sum analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.