translationAut_eEquiv
plain-language theorem explainer
The edge component of translation-by-t on the embedded Freudenthal torus equals conjugation of edge translation by the canonical Fin-indexing of periodic edges. Anyone unpacking Aut structure for the Z_N^3 embedding (PROBE C6) cites this. The equality is definitional: a one-line rfl from the Aut constructor.
Claim. For every $N \ge 1$ and every lattice point $t \in (\mathbb{Z}/N\mathbb{Z})^3$, the edge permutation of the translation automorphism by $t$ equals $\iota \circ \tau_t \circ \iota^{-1}$, where $\iota$ is the canonical finite indexing of positive-displacement periodic edges and $\tau_t$ translates the edge basepoint by $t$ while keeping the displacement class fixed.
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 $\mathbb{Z}_N^3$ (additive group of Vertex $N,N,N$ $= \mathrm{Fin},N \times \mathrm{Fin},N \times \mathrm{Fin},N$) embeds into relabeling automorphisms of the torus image freudenthalBoundedComplex $N$.
Vertex is the periodic cubic lattice. edgeFinEquiv is the canonical equivalence between Fin-indices and positive-displacement PeriodicEdge values. translateEdge $t$ acts on those edges by translating the base and keeping the displacement class (one of seven Freudenthal directions). translationAut packages both vertex and edge actions as an Aut of the embedded complex by conjugating the typed translations through the Fin-indexings.
This lemma isolates the edge field of that package.
proof idea
One-line term proof by rfl. The right-hand side is exactly the eEquiv field written in the constructor of translationAut, so the equality is definitional and needs no lemmas beyond unfolding.
why it matters
Parent results translationAut_zero and translationAut_add use the projected edge (and vertex) fields under Relabel.ext to show that translationAut sends $0$ to the identity relabeling and sends sums to composites. Together those form the monoid-hom package $\mathbb{Z}_N^3 \to \mathrm{Aut}(T_N)$ under Relabel.trans, which is branch (a) of PROBE C6: the translations embed.
Downstream consequences recorded in the module doc include autCard_ge_translations ($N^3 \le |\mathrm{Aut}(T_N)|$) and the measure bound $\mu(T_N) \le 1/N^3$. The lemma itself is pure bookkeeping; it does not touch continuum limits, path-sum values, or any forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.