translateVertex_zero
plain-language theorem explainer
Translation by the zero vertex of the periodic cubic lattice equals the identity equivalence on vertices. Cited by anyone assembling the translation-group embedding into Aut of the Freudenthal torus image (Probe C6). The proof is a short Equiv.ext reduction to the additive identity law v + 0 = v.
Claim. For every positive integer $N$, translation by the zero element of $(\mathbb{Z}/N\mathbb{Z})^3$ is the identity equivalence on the vertex set $\mathrm{Fin}\,N \times \mathrm{Fin}\,N \times \mathrm{Fin}\,N$.
background
The ambient module records two non-flag-bearing path-sum probes attaching the canonical periodic Freudenthal torus to the scoped BoundedComplex state space. Probe C6 checks that the translation group $\mathbb{Z}_N^3$ embeds into the relabeling automorphisms of that image.
Vertices are the product type $\mathrm{Vertex},N,N,N := \mathrm{Fin},N \times \mathrm{Fin},N \times \mathrm{Fin},N$, the additive group of the $N$-periodic cubic lattice under componentwise mod-$N$ addition. Translation by a fixed vertex acts by that addition; the zero vertex is the additive identity of the product.
Upstream arithmetic supplies the identity law used here: addition by zero is a no-op on the underlying integer/rational carriers that back the finite-type coordinates.
proof idea
Pointwise extensionality for equivalences: apply Equiv.ext, introduce an arbitrary vertex $v$, reduce the goal to the additive statement $v + 0 = v$, and rewrite by add_zero. No case splits or induction; the finite-type product structure makes the identity law apply directly.
why it matters
This is the vertex half of the identity case for the translation embedding in Probe C6. Downstream, translationAut_zero lifts it to the full relabeling automorphism: the zero translation equals the identity Relabel on freudenthalBoundedComplex N, by rewriting the vertex component through this lemma and conjugating the edge component.
Together with injectivity and the homomorphism law for sums, the module obtains $|\mathrm{Aut}(T_N)| \ge N^3$ and the measure bound $\mu(T_N) \le 1/N^3$. Those are honest landmine checks only; the module claims nothing about continuum limits or path-sum values. In the broader gravity lane this anchors the discrete translation symmetry of the periodic triangulation before any continuum or measure argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.