translationAut_injective
plain-language theorem explainer
Distinct lattice translations of the periodic Freudenthal torus induce distinct relabeling automorphisms of the embedded complex. Anyone bounding |Aut(T_N)| from below or proving the Z_N^3 embedding (PROBE C6) cites this. The proof evaluates both automorphisms at the origin and recovers the translation vectors by injectivity of the vertex equivalence.
Claim. For every positive integer $N$, the map sending a vertex translation $t \in (\mathbb{Z}/N\mathbb{Z})^3$ to the corresponding relabeling automorphism of the embedded periodic Freudenthal complex is injective: if two translations induce the same automorphism, then they are equal.
background
The module records path-sum probes C3 and C6 only. It attaches the canonical periodic Freudenthal torus at side $N$ to the scoped BoundedComplex state space and checks that the translation group does not collapse under that attachment. No continuum, measure, or path-sum value is claimed.
Vertices are Vertex N N N := Fin N × Fin N × Fin N, the discrete 3-torus under componentwise mod-$N$ addition. The map translationAut N sends each translation vector to a relabeling automorphism of freudenthalBoundedComplex N by translating every vertex (via translateVertex) and transporting through the finite vertex equivalence vertexFinEquiv.
PROBE C6 asks whether these translations embed into Aut or collapse. Injectivity is the first half of the embedding: distinct $t$ must give distinct automorphisms. The ambient dimension $D=3$ (forcing chain T8) is already baked into the cubic vertex set.
proof idea
Tactic proof by evaluating both sides at the origin. Assume translationAut N t = translationAut N s. Apply both vertex equivalences to the origin (vertexFinEquiv N N N).symm 0. Rewrite with translationAut_vEquiv on each side, then cancel the outer vertexFinEquiv via Equiv.apply_symm_apply and expand translateVertex_apply. The resulting equality is 0 + t = 0 + s after injectivity of (vertexFinEquiv).symm. Two applications of zero_add yield $t = s$.
why it matters
This is the injectivity leg of PROBE C6 branch (a): translations embed into Aut of the embedded torus. Downstream, translations_embed_in_aut packages it with the monoid-hom laws into the headline existence statement; autCard_ge_translations turns it into the landmine count $|\mathrm{Aut}(T_N)| \ge N^3$; translationAut_ne_refl uses it to show nonzero translations are nontrivial; and translationAut_three_injective specializes to $N=3$.
In the Recognition gravity lane this blocks the vacuity failure mode where Aut would be too small for the discrete torus to carry a nontrivial path-sum symmetry. Combined with the cardinality bound it feeds mu_freudenthal_le_inv_cube ($\mu(T_N) \le 1/N^3$). It does not touch continuum limits or the actual path-sum measure; those remain outside this probe module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.