ExactAut
plain-language theorem explainer
Automorphisms of an exact-size labeled complex are the self-relabelings that preserve incidence. Anyone counting orbit sizes or writing the discrete-gravity weight 1/|Aut| cites this type. It is a one-line abbreviation of the existing relabeling structure applied to a pair (K,K).
Claim. For an exact combinatorial complex $K$ with fixed vertex, edge, and tetrahedron counts, write $\mathrm{Aut}(K)$ for the set of incidence-preserving bijections of those three index sets that carry $K$ to itself (i.e., relabeling isomorphisms $K\to K$).
background
This module builds the configuration space of the RS path sum as exact complexity shells: complexes with prescribed counts $(v,e,t)$ and no size caps. An ExactComplex is abstract incidence data only: maps sending each edge index to a pair of vertices and each tetrahedron index to four vertices.
A relabeling between two such complexes of the same signature is a triple of bijections on the vertex, edge, and tet index sets that intertwine those incidence maps. The module defines that structure independently of the older capped Relabel, so cross-cap identification never arises.
The local goal is Stage 1 of the seven-gaps program: make exact shells into genuine setoids, prove they are finite types with an entropy bound, and equip each labeled complex with the standard discrete-gravity symmetry factor $\mu=1/|\mathrm{Aut}|$ before inserting the hand-chosen Gaussian UV regulator.
proof idea
One-line abbreviation: the automorphism type is literally the relabeling type specialized to the diagonal pair $(K,K)$. No new data or proof obligations. The companion instance that the type is nonempty is the identity relabeling (reflexivity of exact relabeling).
why it matters
This is the carrier type for every exact-shell symmetry factor in the module. Downstream, exactMu is defined as $1/|\mathrm{Aut}(K)|$, and positivity/upper bounds on that measure feed the modulus estimate on each regulated shell term and the summability of the UV path sum for every $\rho>0$.
On the bridge side, CapShellBridge proves that forgetting a size cap preserves automorphism cardinality: $\mathrm{card}(\mathrm{Aut},K)=\mathrm{card}(\mathrm{ExactAut}(\mathrm{toExact},K))$, and the quotient-level shell automorphism count is defined by evaluating this type on a representative. Without a clean exact automorphism type, the capped and cap-free measures would not match.
Framework role is bookkeeping for the discrete path-sum measure, not a forcing-chain step. Regulator removal and continuum limits remain explicitly open; this definition does not touch those flags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.