instFiniteExactAut
plain-language theorem explainer
The automorphism group of an exact-size labeled complex (fixed vertex, edge, and tetrahedron counts) is finite. Anyone defining the per-class path-sum weight 1/|Aut| on exact complexity shells cites this. The proof injects Aut into the finite triple of index-set permutations via the relabeling-to-triple map.
Claim. For any exact combinatorial complex $K$ with fixed numbers of vertices, edges, and tetrahedra, the set of incidence-preserving relabelings of $K$ onto itself is finite.
background
This module builds exact complexity shells for the Recognition path sum: configurations are ExactComplex v e t, meaning exactly $v$ vertices, $e$ edges, and $t$ tetrahedra with abstract incidence maps and no size caps. Relabelings are bijections of the three index sets that commute with incidence; they are defined independently of any capped embedding.
An automorphism of a fixed labeled complex $K$ is a relabeling of $K$ onto itself. The module already records that this set is nonempty (the identity relabeling). Finiteness is the remaining structural fact needed before the class measure $1/|\mathrm{Aut}|$ is well-defined on exact path classes.
The ambient setting is Stage 1 of the seven-gaps program: shell structure for a Gaussian-UV-regularized path sum. The regulator and the action/phase are mathematical parameters, not derived physics; regulator removal remains an open named hypothesis.
proof idea
One-line instance: apply Finite.of_injective to the map sending each automorphism to its underlying triple of index permutations. Injectivity is supplied by ExactRelabel.toEquivTriple_injective at equal source and target $K$. The codomain is a product of finite symmetric groups on Fin v, Fin e, and Fin t, hence finite, so the domain is finite.
why it matters
Stage 1 of ExactShellGaugeUV needs finite automorphism groups so the per-class measure $\mathrm{classMu}=1/|\mathrm{Aut}|$ is a well-defined positive real at most 1, and so exact path classes can be treated as Fintypes with entropy bounds. Downstream, relabelSigmaEquiv in RegulatorRemovalNoGo uses this finiteness infrastructure when identifying the sigma of all relabelings out of a fixed base complex with the full relabeling triple group (the total torsor). That torsor is the combinatorial backbone for no-go and counting arguments around regulator removal. Nothing here closes the open HasZRSRegulatorRemoval flag or any continuum-limit ledger entry; it only locks the finite-group side of the exact-shell bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.