autCard_ge_translations
plain-language theorem explainer
For any positive integer N, the automorphism group of the side-N periodic Freudenthal torus (packaged as a path-sum bounded complex) has cardinality at least N^3. Gravity path-sum auditors cite it as the count-form landmine that translations embed nontrivially. The proof injects the vertex set via the translation-automorphism map and rewrites the domain card as N^3.
Claim. For every positive integer $N$, if $T_N$ denotes the canonical periodic Freudenthal torus of side $N$ viewed as a bounded complex, then $N^3 \le |\mathrm{Aut}(T_N)|$, where $\mathrm{Aut}$ is the group of relabeling automorphisms of the complex.
background
Lane O of the Seven Gaps path-sum probes attaches the canonical periodic Freudenthal torus to the scoped path-sum state space without claiming measures, limits, or continuum values. The object freudenthalBoundedComplex N is that torus at side $N\ge 1$, with vertex count $nV=N^3$, edge count $nE=7N^3$, and tet count $nT=6N^3$, inherited from the periodic triangulation; edge-in-tet slots and per-tet metrics are dropped by shape mismatch.
Automorphisms of a bounded complex are relabelings of the complex onto itself (the type Aut K := Relabel K K). The translation group is the additive group of vertices $\mathbb{Z}_N^3 = \mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$ under componentwise mod-$N$ addition. Probe C6 checks that this group embeds into Aut of the torus image: the map sending a vertex shift to the corresponding relabeling is injective, sends zero to the identity, and sends sums to composites.
Upstream, card_vertex records that the periodic vertex set has exactly $N^3$ elements. That count is the orbit-size lower bound used here.
proof idea
Term-mode argument in two steps. First apply Nat.card_le_card_of_injective to the translation-automorphism map translationAut N together with its injectivity lemma translationAut_injective N; this yields $|\mathrm{Vertex}| \le |\mathrm{Aut}(T_N)|$. Then rewrite the left-hand side by Nat.card_eq_fintype_card and card_vertex, which identifies the vertex cardinality with $N^3$. No further case splits.
why it matters
This is the count-form half of Probe C6's Aut-vacuity landmine: translations embed, so the automorphism group cannot be trivial and is at least as large as the translation orbit. Downstream, mu_freudenthal_le_inv_cube converts the inequality into the measure-form landmine $\mu(T_N)\le 1/N^3$, the symmetry factor suppressing the torus configuration by at least its translation-orbit size. The specialization autCard_ge_27 is the $N=3$ instance used in concrete numerical checks.
In the Seven Gaps gravity lane this is provenance and a cheap honesty check only: it does not evaluate any path sum, does not force a continuum limit, and does not close a flag-bearing gap. It blocks the vacuous-Aut failure mode before measure comparisons are written.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.