autCard_ge_27
plain-language theorem explainer
The automorphism group of the side-3 periodic Freudenthal torus has at least 27 elements. Path-sum and Seven Gaps gravity work cites this as the concrete N=3 case of the translation-embedding lower bound. Proof is a one-line specialization of the general cube bound followed by numeric reduction of 3³.
Claim. Let $T_3$ be the bounded complex obtained by packaging the canonical periodic Freudenthal triangulation of the $3\times 3\times 3$ torus. Then the cardinality of its relabeling automorphism group satisfies $|\mathrm{Aut}(T_3)| \ge 27$.
background
Module lane is Seven Gaps Phase 2b, path-sum probes C3 and C6. It is explicitly non-flag-bearing: it attaches the canonical periodic Freudenthal torus to the scoped path-sum state space and records cheap Aut facts, claiming nothing about measures, limits, or continuum behavior.
For any $N\ge 1$, freudenthalBoundedComplex N packages the periodic Freudenthal torus of side $N$ as a BoundedComplex with vertex count $N^3$, edge count $7N^3$, and tet count $6N^3$, matching the canonical periodic triangulation on incidence data that the scoped class retains. Probe C6 checks that Aut is not vacuously trivial: the translation group $\mathbb{Z}_N^3$ (additive group of vertices $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$) embeds into the relabeling automorphisms via an injective monoid map sending $0$ to the identity and sums to composites.
The general consequence is $N^3\le|\mathrm{Aut}(T_N)|$. The present declaration is the numeric $N=3$ instance of that bound.
proof idea
One-line specialization. Instantiate the general lower bound autCard_ge_translations at $N=3$, which supplies $3^3\le\mathrm{Nat.card}(\mathrm{Aut}(T_3))$. Then norm_num rewrites the left-hand side to $27$, and the resulting inequality is returned. No new group-theoretic work occurs here; injectivity of the translation embedding and the cube cardinality of the vertex group are already discharged upstream.
why it matters
Closes the concrete $N=3$ case of Probe C6 (Aut vacuity landmine check) in the Seven Gaps path-sum lane. The module records that translations embed, so Aut is at least as large as the vertex lattice; the companion inequality $\mu(T_N)\le 1/N^3$ needs a nontrivial Aut lower bound to be informative rather than vacuous. Specializing to side 3 yields the familiar $27$, matching $|\mathbb{Z}_3^3|$.
No downstream consumers are wired yet (used_by empty). The result sits entirely inside the gravity / path-sum probe layer and does not touch the forcing chain (T5–T8), RCL, or mass-ladder landmarks. It is a bookkeeping lemma that keeps the Aut side of the probe honest before any measure or continuum claim is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.