translationAut_tEquiv
plain-language theorem explainer
The tetrahedron-index map of the translation-by-t automorphism equals conjugation of cell-wise tet translation by the canonical Fin-indexing of periodic tetrahedra. Anyone unpacking Aut components for the Z_N^3 monoid-hom laws cites this. The equality is definitional (rfl from the construction of translationAut).
Claim. For $N \ge 1$ and any vertex $t$ of the periodic cubic lattice $\mathrm{Fin}\,N \times \mathrm{Fin}\,N \times \mathrm{Fin}\,N$, the tetrahedron-index bijection of the translation-by-$t$ relabeling automorphism of the embedded Freudenthal complex equals $(\iota \circ \tau_t \circ \iota^{-1})$, where $\iota$ is the canonical finite indexing of periodic tetrahedra and $\tau_t$ translates the cell while keeping the local Freudenthal tet index.
background
Module PathSumProbes records two non-flag-bearing probes linking the canonical periodic Freudenthal torus to the scoped path-sum state space BoundedComplex. PROBE C6 checks that the translation group $Z_N^3$ (additive group of Vertex $N,N,N$) embeds into Aut of the torus image freudenthalBoundedComplex $N$.
A Relabel is a triple of bijections on vertex/edge/tet index sets commuting with incidence. The automorphism translationAut $N,t$ is built by conjugating the typed translations (on vertices, edges, and tets) through the canonical Fin-indexings. Upstream, translateTet $t$ is Equiv.prodCongr of vertex translation with the identity on the local Fin 6 tet label; tetFinEquiv is the canonical Fin-indexing of PeriodicTet.
This lemma isolates the tet component of that conjugation, matching the already-stated vertex and edge projections of translationAut.
proof idea
One-line term proof by rfl. The right-hand side is exactly how translationAut defines its tEquiv field (conjugate translateTet $t$ by tetFinEquiv), so the equality is definitional and needs no rewriting or case analysis.
why it matters
Parent results translationAut_zero and translationAut_add apply Relabel.ext and rewrite the three component projections; this lemma supplies the tet leg of those rewrites. Together with the vertex and edge projections they package translationAut as a monoid homomorphism $Z_N^3 \to \mathrm{Aut}(T_N)$ under Relabel.trans, which is branch (a) of PROBE C6 (translations embed). Downstream consequences recorded in the module are autCard_ge_translations ($N^3 \le |\mathrm{Aut}(T_N)|$) and the measure bound $\mu(T_N) \le 1/N^3$. No continuum, measure-limit, or simpliciality claim is made here; the module is explicitly probes-only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.