translations_embed_in_aut
plain-language theorem explainer
The additive group of the N×N×N periodic cubic lattice embeds into the relabeling automorphism group of the Freudenthal torus packaged as a bounded complex. Anyone bounding |Aut| or the path-sum measure μ on that complex cites this monoid embedding. The proof is a four-field term package of the already-built translation map and its injectivity, identity, and additivity lemmas.
Claim. For every positive integer $N$, there exists an injective map $f$ from the additive group of vertices $(\mathbb{Z}/N\mathbb{Z})^3$ into the relabeling automorphism group of the Freudenthal bounded complex of side $N$, such that $f(0)$ is the identity relabeling and $f(t+s)=f(t)\circ f(s)$ for all lattice vectors $t,s$.
background
Lane O of Seven Gaps Phase 2b records two cheap probes attaching the canonical periodic Freudenthal torus to the scoped path-sum state space BoundedComplex. Probe C3 packages that torus at side $N$ (any $N\ge 1$) as freudenthalBoundedComplex N with cap $B=7N^3$, inheriting vertex/edge/tet counts and both incidence maps from the canonical periodic triangulation; edge-in-tet slots and per-tet metrics are dropped by shape mismatch.
An automorphism here is a self-relabeling: bijections of the finite vertex, edge, and tet index sets that commute with the incidence maps. Vertices of the torus are the product type $(\mathrm{Fin},N)^3$ under componentwise mod-$N$ addition, i.e. the translation group $\mathbb{Z}_N^3$.
Probe C6 checks that this translation group is not vacuous inside Aut: the map sending a lattice vector $t$ to conjugation of typed translation through the canonical Fin-indexings yields a genuine monoid homomorphism into Aut.
proof idea
Term-mode package, not a fresh argument. The witness is the already-defined map translationAut N, which builds each Aut element by conjugating translateVertex / translateEdge / translateTet through the canonical Fin-equivalences of the embedded complex.
The three conjuncts are discharged by the sibling lemmas translationAut_injective, translationAut_zero, and translationAut_add. No enumeration over $N$ appears; commutation of incidence with translation is inherited from the typed addBits-compatibility proved upstream when those maps were constructed.
why it matters
This is the headline of Probe C6, branch (a): translations embed, so Aut of the embedded torus is at least as large as $\mathbb{Z}_N^3$. The module docstring records the immediate consequences (proved as siblings): $|\mathrm{Aut}(T_N)|\ge N^3$ and therefore the normalized path-sum measure satisfies $\mu(T_N)\le 1/N^3$.
In the Seven Gaps gravity program this is a landmine check, not a continuum claim. It rules out the vacuous-Aut failure mode that would make every orbit measure equal to 1 and collapse the path-sum bookkeeping. It does not yet touch the forcing chain T0–T8, the Recognition Composition Law, or the $\varphi$-ladder mass formula; it only secures that the discrete torus image carries a nontrivial translation symmetry inside the scoped Aut type used by later measure arguments.
No downstream dependents are wired yet (used_by is empty), so the declaration presently serves as the provenance anchor for those cardinality and measure inequalities inside the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.