translateTet_zero
plain-language theorem explainer
Translation of periodic tetrahedra by the zero lattice vector is the identity equivalence. Anyone checking that the Z_N^3 translation group embeds into Aut of the Freudenthal torus image cites this as the unit case. The proof is a short term argument: extend equality of equivalences and cancel the zero summand on the cell coordinate.
Claim. For every $N \ge 1$, translation of periodic tetrahedra by the zero vertex $0 \in (\mathbb{Z}/N\mathbb{Z})^3$ equals the identity equivalence on the set of periodic tetrahedra (cell index in $(\mathbb{Z}/N\mathbb{Z})^3$ times local Freudenthal tet label in $\{0,\ldots,5\})$.
background
Module lane is Seven Gaps Phase 2b path-sum probes C3 and C6. It is non-flag-bearing: it only attaches the canonical periodic Freudenthal torus at side $N$ to the scoped path-sum state space BoundedComplex and checks that lattice translations embed into relabeling automorphisms. No continuum, measure, or path-sum value is claimed.
A periodic vertex is a triple in $\mathrm{Fin},N \times \mathrm{Fin},N \times \mathrm{Fin},N$. Periodic tetrahedra are pairs (cell vertex, local Freudenthal index in $\mathrm{Fin},6$). Translation by a lattice vector $t$ acts by translating the cell and leaving the local tet index fixed: it is the product of vertex translation with the identity on $\mathrm{Fin},6$.
The additive unit on vertices is componentwise zero. Upstream arithmetic supplies $n+0=n$ (and the corresponding integer form), which is exactly what the cell coordinate needs.
proof idea
Apply extensionality of equivalences and fix an arbitrary periodic tetrahedron $p=(v,i)$. Unfolding the product-congruence definition of tetrahedron translation by zero reduces the goal to $(v+0,i)=p$. Rewrite with add_zero on the cell coordinate; the local index is already untouched. Done in four tactic lines.
why it matters
This is the unit case of PROBE C6 (Aut vacuity landmine check), branch (a): translations embed. Downstream translationAut_zero lifts the same fact to the full relabeling automorphism of the packaged freudenthalBoundedComplex N, using the vertex and edge companions together with this tetrahedron identity.
That zero-to-identity step is required for the homomorphism property of translationAut and for the injectivity and cardinality lower bound $|\mathrm{Aut}(T_N)| \ge N^3$, which in turn yields the crude measure bound $\mu(T_N)\le 1/N^3$. Within Recognition gravity scaffolding it is bookkeeping, not a continuum claim: it only certifies that the discrete translation group sits inside Aut before any path-sum or continuum limit is discussed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.