exactMu
plain-language theorem explainer
Defines the symmetry-factor measure on an exact-size labeled complex as the reciprocal of its automorphism group order: μ(K)=1/|Aut K|. Discrete-gravity and path-sum workers cite it as the standard Burnside weight on labeled configurations. The body is a one-line reciprocal of the finite automorphism cardinality.
Claim. For an exact-size combinatorial complex $K$ with fixed vertex, edge, and tetrahedron counts, the symmetry-factor measure is $\mu(K) := 1/|\mathrm{Aut}(K)|$, where $\mathrm{Aut}(K)$ is the group of incidence-preserving relabelings of $K$ onto itself.
background
This module builds exact complexity shells for the Recognition Science path sum: configurations with fixed counts $(v,e,t)$ and no size caps, then Gaussian-UV-regularized shell sums. An exact complex carries incidence maps for edges and tetrahedra on finite index sets; there is no embedding into a capped class, so cross-cap identification issues do not arise.
The automorphism group is the set of exact relabelings of $K$ onto itself (bijections of vertex/edge/tet indices commuting with incidence). It is always nonempty (identity) and finite. The measure $\mu(K)=1/|\mathrm{Aut} K|$ is the standard discrete-gravity symmetry factor: each labeled representative is weighted by the reciprocal of its stabilizer so that the weight descends to the unlabeled class.
The module is explicit that the UV factor $\exp(-\rho n^2)$ is a mathematical regulator, the phase is a free class-invariant parameter, and regulator removal ($\rho\to 0^+$) remains an open named hypothesis.
proof idea
Pure definition: cast the finite cardinality of the automorphism type to $\mathbb{R}$ and take the reciprocal. No lemmas are applied at the definition site; positivity, the bound $\mu\le 1$, and global-equivalence invariance are proved immediately downstream by unfolding and using that $|\mathrm{Aut} K|\ge 1$.
why it matters
Stage-2 building block for the shell-resummed path sum: the per-class measure is obtained by lifting this labeled weight through the exact setoid (classMuOn), using congruence under global equivalence. Downstream, it matches the capped representative measure under cap-forgetting (mu_eq_exactMu_toExact, classMu_capToShell), feeds positivity and unit bounds (exactMu_pos, exactMu_le_one), and appears in fiber-parity and regulator-removal no-go arguments that control shell automorphism counts.
Within the Seven Gaps program this is the exact-shell analogue of the capped path-sum measure. It does not close continuum or regulator-removal flags; those stay open by module policy. It is the discrete-gravity convention that makes the Gaussian-regularized shell series well-defined for every $\rho>0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.