translationAut_add
plain-language theorem explainer
Translation by the sum of two lattice vectors equals the composite of the two individual translation automorphisms of the periodic Freudenthal torus. Anyone packaging the Z_N^3 action as a monoid homomorphism into Aut(T_N) cites this. The proof extends equality of relabelings by rewriting the three component equivalences and applying the corresponding translate-composition lemmas.
Claim. For every $N \ge 1$ and every pair of vertices $t,s \in (\mathbb{Z}/N\mathbb{Z})^3$, the automorphism given by translation by $t+s$ equals the composite (under relabeling composition) of translation by $t$ followed by translation by $s$.
background
The ambient setting is Phase 2b lane O of the Seven Gaps program: non-flag-bearing path-sum probes that attach the canonical periodic Freudenthal torus to the scoped BoundedComplex state space and check that the translation group is not vacuous in the automorphism monoid.
Vertices are the product lattice Vertex N N N := Fin N × Fin N × Fin N under componentwise addition mod $N$. A translation automorphism is a relabeling of the embedded torus freudenthalBoundedComplex N that acts by adding a fixed lattice vector on vertices, edges, and tetrahedra. Relabelings compose via Relabel.trans, whose vertex/edge/tet components are ordinary equivalence composition (trans_vEquiv, trans_eEquiv, trans_tEquiv).
Together with the zero-to-identity law, this statement is the additive monoid-hom package from $\mathbb{Z}_N^3$ into Aut under composition.
proof idea
Apply extensionality of relabelings (Relabel.ext), which reduces the claim to three component equalities (vertex, edge, tet equivalences). On each component, unfold the definition of translation automorphism, rewrite composition of relabelings to composition of the underlying equivalences, then apply the conjugation-transitivity identity conj_trans and the corresponding translate-composition lemma (translateVertex_trans, translateEdge_trans, or translateTet_trans). The three branches are parallel rewrites; no case split on $N$ is needed.
why it matters
This is one of the three legs of PROBE C6 (Aut vacuity landmine check), branch (a): translations embed. The parent theorem translations_embed_in_aut packages injectivity, the zero law, and this additivity into a single existential monoid embedding $\mathbb{Z}_N^3 \hookrightarrow \mathrm{Aut}(T_N)$. From that embedding the module derives the cardinality lower bound $N^3 \le |\mathrm{Aut}(T_N)|$ and the path-sum measure upper bound $\mu(T_N) \le 1/N^3$.
In the broader gravity lane the result certifies that the discrete torus carries a faithful translation symmetry before any continuum or measure claim is attempted. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law directly; it is infrastructure for the discrete geometric side of the Seven Gaps path-sum probes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.