instFiniteAut
plain-language theorem explainer
The automorphism group of any bounded labeled complex is finite. Path-sum and gravity authors cite this to make the symmetry weight μ(K)=1/|Aut(K)| a well-defined real in (0,1]. The proof is a one-line Finite.of_injective wrapper: self-relabelings inject into a finite triple of index permutations.
Claim. For every bound $B\in\mathbb{N}$ and every bounded complex $K$ with at most $B$ vertices, edges, and tetrahedra, the group $\mathrm{Aut}(K)$ of combinatorial self-relabelings of $K$ is finite.
background
Lane 2 of the Seven Gaps gravity program builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped configuration class at fixed lattice scale. Configurations are bounded combinatorial complexes: incidence data with at most $B$ vertices, edges, and tetrahedra, equilateral at the substrate mesh (CDT-style), with the metric field dropped. The class is a superclass of bounded triangulations; simplicial constraints are not enforced, so finiteness of the superclass yields finiteness of every subclass.
An automorphism of a labeled complex $K$ is a relabeling of $K$ onto itself. The identity relabeling already shows $\mathrm{Aut}(K)$ is nonempty. Finiteness is the remaining ingredient so that the symmetry factor $\mu(K)=1/|\mathrm{Aut}(K)|$ is a genuine positive real at most one, and so that the path sum $Z=\sum_K \mu(K),w(K)$ is a finite sum with modulus bounds.
This discharges the count-finiteness content that the admissible-triangulation growth-base field had only postulated; sharper exponential-growth semantics for exact simplicial subclasses stay open.
proof idea
One-line instance wrapper. Apply Finite.of_injective to the map that sends a self-relabeling to its underlying triple of index bijections (on vertices, edges, and tetrahedra). Injectivity is Relabel.toEquivTriple_injective at $K'=K$. The codomain is a product of finite symmetric groups on the index sets of $K$, hence finite; an injective preimage of a finite type is finite.
why it matters
Module status tags finiteness (with nonemptiness) of $\mathrm{Aut}(K)$ as a proved tier item underwriting the whole measure package: $0<\mu(K)\le 1$, the bounds $|Z|\le\sum\mu$ and $|Z|\le\mathrm{card}$ of the bounded class, relabeling invariance of $\mu$ and of $Z$, and unitary well-definedness when $w=e^{iS}$. Without a finite automorphism group the symmetry weight is not a finite-group average.
Downstream gauge-preflight material sits on the same relabeling infrastructure (composite relabelings, equivalence of complexes). In the Recognition gravity program this is the honest scoped $Z_{\mathrm{RS}}$ statement: a finite combinatorial path sum with a proved symmetry factor, not an assumed weight. It does not close the open exponential-growth question for exact simplicial subclasses; it only needs the finite superclass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.