translationAut_three_injective

Module lane O records path-sum probes only: no continuum, measure, or flag-bearing claims. Probe C6 checks that the translation group does not collapse under the embedding into automorphisms of the torus image.

A bounded complex is a finite labeled 3-complex in the path-sum state space. Its automorphism group consists of relabelings of that complex onto itself. The side-$N$ periodic Freudenthal torus is packaged as such a complex with $N^3$ vertices and $7N^3$ edges.

Translation by $t \in (\mathbb{Z}/N\mathbb{Z})^3$ acts by conjugating the typed lattice translation through the canonical Fin-indexings of vertices and edges. The general fact that distinct translations yield distinct relabelings is already proved: the image vertex permutation recovers $t$ at the origin.

One-line term wrapper: instantiate the general injectivity theorem for the translation-to-automorphism map at $N = 3$. No extra case analysis; the [NeZero 3] instance is immediate.

Closes the concrete $N = 3$ case of Probe C6 branch (a): translations embed rather than collapse. The module records the consequences $N^3 \le |\mathrm{Aut}(T_N)|$ and $\mu(T_N) \le 1/N^3$; at side 3 this yields $|\mathrm{Aut}(T_3)| \ge 27$ and the matching measure upper bound. Downstream used-by edges are empty on this page, so the declaration is a named specialization for the side-3 landmine check and for any later Aut-cardinality or path-sum bound that fixes $N = 3$. It does not touch the forcing chain (T0–T8) or the Recognition Composition Law; it only stabilizes the discrete geometry side of the gravity path-sum probes.