translationAut
plain-language theorem explainer
Lattice translation by any t in (Z/NZ)^3 yields a relabeling automorphism of the periodic Freudenthal torus packaged as a BoundedComplex. Probe C6 (Aut-vacuity landmine) cites this map as the embedding of the translation group into Aut(T_N). The construction conjugates componentwise mod-N translation through the canonical Fin-indexings of vertices, edges, and tets; incidence commutation is pure addBits algebra, with no enumeration.
Claim. For each side length $N \ge 1$ and each lattice point $t \in (\mathbb{Z}/N\mathbb{Z})^3$, translation by $t$ defines a relabeling automorphism of the bounded complex obtained from the periodic Freudenthal torus of side $N$: vertices, edges, and tetrahedra are permuted by conjugating the typed translation maps through the canonical finite indexings, and the two incidence-commutation identities hold.
background
Lane O of Seven Gaps Phase 2b records path-sum probes only. It attaches the canonical periodic Freudenthal torus at side $N$ to the scoped path-sum state space BoundedComplex and checks that the translation group does not collapse under that packaging. No measure, limit, or continuum claim is made.
Vertices of the torus are Vertex N N N = Fin N × Fin N × Fin N under componentwise mod-$N$ addition. Edges and tetrahedra carry canonical Fin-indexings (edgeFinEquiv, tetFinEquiv, vertexFinEquiv). Local cube geometry uses tetVerts (six tets per cube as vertex-bit lists) and addVertexBits (add a cube-corner bit-offset to a lattice vertex).
An automorphism here is a triple of permutations of the finite vertex/edge/tet index sets that commute with the incidence maps of the bounded complex (edge endpoints and tet corners). The typed translations on the geometric side already exist; this definition only conjugates them into the Aut interface of the embedded complex.
proof idea
Definitional construction of the three equiv fields: each is the conjugate
(finEquiv).trans (translateX t).trans (finEquiv).symm
for vertices, edges, and tets respectively.
edge_comm reduces by cancelling edgeFinEquiv with apply_symm_apply, invoking translateEdge_endpoints (endpoints shift by $t$), then cancelling vertexFinEquiv and applying translateVertex_apply on each endpoint.
tet_comm likewise cancels tetFinEquiv, rewrites the translated base vertex via addVertexBits_add_right (bit-offset after adding $t$), cancels vertexFinEquiv, and finishes with translateVertex_apply. No case split on $N$ or on tet labels.
why it matters
This is the constructive half of Probe C6 branch (a): translations embed into Aut of the torus image. Downstream, translationAut_injective recovers $t$ from the vertex permutation at the origin; translationAut_add and the zero case make the map a monoid homomorphism into relabelings; translationAut_ne_refl and nontrivial_aut_three exhibit concrete nontrivial autos.
The count form autCard_ge_translations then gives $|\mathrm{Aut}(T_N)| \ge N^3$, which feeds the landmine bound $\mu(T_N) \le 1/N^3$. Without this embedding the Aut group could have been trivial after packaging, collapsing the path-sum symmetry story. The module remains non-flag-bearing: the definition only supplies the group action used by those cardinality and nontriviality lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.