Aut
plain-language theorem explainer
Automorphisms of a bounded combinatorial complex are the self-relabelings: bijections of vertex, edge, and tetrahedron indices that commute with incidence. Anyone writing the path-sum measure μ(K)=1/|Aut K| cites this type. It is a one-line abbreviation of the existing Relabel structure at equal arguments, so finiteness and nonemptiness inherit from the ambient relabeling theory.
Claim. For a size bound $B\in\mathbb{N}$ and a bounded complex $K$ (at most $B$ vertices, edges, and tetrahedra, with incidence maps), write $\mathrm{Aut}(K)$ for the set of relabeling isomorphisms from $K$ to itself: triples of bijections on the vertex, edge, and tetrahedron index sets that intertwine the edge-endpoint and tetrahedron-vertex maps.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of combinatorial triangulations. The substrate fixes edge length at the minimum mesh, so configurations are equilateral and CDT-style: all geometry sits in incidence data.
A BoundedComplex B packages counts $n_V,n_E,n_T\le B$ together with maps edgeVerts : Fin n_E → Fin n_V × Fin n_V and tetVerts : Fin n_T → Fin 4 → Fin n_V. It mirrors the incidence shape of a 3D Regge triangulation with the metric field dropped and an explicit size cap. It contains all bounded triangulations and also non-simplicial incidence data; finiteness of the superclass still yields finiteness of every subclass.
A Relabel K K' is a triple of equivalences on the three index sets that commute with those incidence maps. The module proves that relabeling is a genuine equivalence relation and that the quotient of labeled complexes is finite. Automorphisms are the diagonal case used to define the symmetry factor in the measure.
proof idea
Definitional abbreviation only: Aut K is literally Relabel K K. No separate construction. Immediately afterward the file installs Nonempty (Aut K) by the identity relabeling Relabel.refl K. Finiteness is proved later by injecting automorphisms into the finite product of permutations of the three index sets (the theorem tagged just below the abbrev).
why it matters
Module doc lists Aut among the THEOREM-tier ingredients of the path-sum measure: Aut is finite and nonempty, so $\mu(K)=1/|\mathrm{Aut},K|$ satisfies $0<\mu(K)\le 1$ and is relabeling-invariant. The finite weighted sum $Z B w=\sum_K \mu(K),w(K)$ then inherits modulus bounds and invariance under equivalence-preserving bijections; the unitary weights $w=e^{iS}$ give the honest scoped $Z_{\mathrm{RS}}$.
This closes the symmetry-factor half of the count-finiteness content previously postulated in PathSumUVBound.AdmissibleTriangulationFamily.growthBase. Sharper exponential-growth semantics for exact simplicial subclasses remain open. Downstream, the same Aut pattern appears in cost-algebra classification of $J$-automorphisms and in gauge-from-cube order counts, but those uses are structural analogies rather than direct imports of this gravity definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.