translationAut_ne_refl
plain-language theorem explainer
Any nonzero lattice translation on the side-N periodic Freudenthal torus induces a non-identity automorphism of the corresponding bounded complex. Gravity and path-sum workers cite it when ruling out Aut-vacuity for the torus image. The argument is a short contradiction: injectivity of the translation map plus the zero-to-identity clause forces the translation vector to vanish.
Claim. For every $N \ge 1$ and every nonzero vertex $t \in (\mathbb{Z}/N\mathbb{Z})^3$, the automorphism of the side-$N$ Freudenthal bounded complex induced by translation by $t$ is not the identity relabeling.
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 state space BoundedComplex (probe C3) and checks that the translation group does not collapse inside the automorphism group of that image (probe C6).
Vertices are the product lattice $\mathrm{Vertex},N,N,N = (\mathbb{Z}/N\mathbb{Z})^3$. An automorphism of a bounded complex is a relabeling: bijections of vertex, edge, and tet index sets that commute with the incidence maps. The translation map sends each lattice vector $t$ to the relabeling that adds $t$ componentwise mod $N$ on vertices (and correspondingly on edges and tets).
Upstream facts already available: the translation map is injective, and translation by the zero vector is exactly the identity relabeling. The module docstring records the intended consequence: $\mathbb{Z}_N^3$ embeds into $\mathrm{Aut}(T_N)$, so $|\mathrm{Aut}(T_N)| \ge N^3$.
proof idea
Assume for contradiction that translation by $t$ equals the identity relabeling. Compose that equality with the known identity translationAut N 0 = refl to obtain translationAut N t = translationAut N 0. Injectivity of the translation map then yields $t = 0$, contradicting the hypothesis. The whole argument is a two-line contradiction using those two lemmas.
why it matters
Probe C6 is an Aut-vacuity landmine check: if every translation collapsed to the identity, the path-sum measure bound $\mu(T_N) \le 1/N^3$ would be vacuous or false in spirit. This lemma is the pointwise non-identity half of the embedding. It feeds the concrete witness nontrivial_aut_three, which exhibits translation by $(1,0,0)$ at $N=3$ as a genuine nontrivial automorphism (via decide on the finite inequality). Together with injectivity and the homomorphism law, it underwrites the cardinality lower bound $|\mathrm{Aut}(T_N)| \ge N^3$ and the ensuing measure upper bound. The module remains non-flag-bearing: no continuum limit, no path-sum value, and no simpliciality claim is asserted here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.