nontrivial_aut_three
plain-language theorem explainer
At side length N=3 on the periodic Freudenthal torus, lattice translation by (1,0,0) is a nontrivial automorphism of the bounded-complex image. Probe-C6 readers cite it as an explicit witness that the translation group is not Aut-vacuous. Proof is a one-line call to the general nonzero-translation lemma, with the finite inequality (1,0,0)≠0 discharged by decide.
Claim. The translation automorphism of the side-$3$ periodic Freudenthal bounded complex induced by the vertex $(1,0,0)\in(\mathbb{Z}/3\mathbb{Z})^3$ is not the identity relabeling.
background
This module is a non-flag-bearing probe lane (Seven Gaps, Phase 2b, lane O). It records two cheap facts linking the canonical periodic Freudenthal torus to the scoped path-sum state space BoundedComplex, and makes no claim about measures, limits, or continuum behavior.
Vertices of the $N\times N\times N$ periodic cubic lattice are triples in $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$. The translation map sends a lattice vector $v$ to the relabeling automorphism that adds $v$ (componentwise mod $N$) on every vertex of the torus image packaged as a bounded complex. By design the zero vector maps to the identity relabeling; the general nonzero-translation lemma then says any $v\neq 0$ yields a non-identity automorphism.
Probe C6 is the Aut-vacuity landmine check. Outcome branch (a) is that translations embed: the additive group $(\mathbb{Z}/N\mathbb{Z})^3$ injects into Aut of the torus image. Consequences recorded in the module include $|\mathrm{Aut}(T_N)|\ge N^3$ and the measure upper bound $\mu(T_N)\le 1/N^3$.
proof idea
One-line term proof. Apply the general lemma that any nonzero lattice vector induces a non-identity translation automorphism, specialized at $N=3$. Discharge the single finite hypothesis $(1,0,0)\neq 0$ in $\mathrm{Fin},3\times\mathrm{Fin},3\times\mathrm{Fin},3$ by decide (kernel decide on a finite product of Fin types; no native_decide).
why it matters
Concrete $N=3$ witness for probe C6 (Aut vacuity landmine) in the gravity Seven Gaps path-sum lane. The module status is PROBES ONLY: provenance record plus landmine check, with no continuum or path-sum evaluation claims. Exhibiting one nontrivial translation supports the embedding branch of C6, which underwrites the cardinality lower bound $N^3\le|\mathrm{Aut}(T_N)|$ and the consequent bound $\mu(T_N)\le 1/N^3$ stated in the module doc.
No downstream consumers are wired in the current graph (used_by empty). The result sits in discrete geometry scaffolding that feeds Recognition gravity path sums; it is not a step of the T0–T8 forcing chain, RCL, or the constants ladder. It closes the "Aut might be trivial at N=3" landmine for the torus image without claiming full Aut structure or simpliciality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.