classMu
plain-language theorem explainer
Assigns to each exact complexity-shell class the real weight 1/|Aut|, obtained by lifting the labeled automorphism measure through the global-equivalence quotient. Gravity path-sum and shell-bridge arguments cite it as the canonical class measure. The body is a one-line projection onto the already-lifted quotient measure classMuOn.
Claim. For each natural number $n$ and each exact complexity-shell class $c$ of complexity $n$, $\mathrm{class}\mu(c)\in\mathbb{R}$ is the per-class measure on that shell element: the value of the quotient-lifted labeled measure $1/|\mathrm{Aut}|$ at the signature and quotient component of $c$.
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells (no size caps in the shell definition) and studies the shell-resummed path sum with a hand-inserted Gaussian UV regulator $\exp(-\rho n^2)$. Honesty constraints: the regulator is mathematical, not derived physics; the phase is a free class function; regulator removal $\rho\to 0^+$ remains a named open.
An exact complexity shell at level $n$ is the disjoint union, over shell signatures $(v,e,t)$ with complexity $n$, of the quotient of labeled exact complexes by global relabeling equivalence. The labeled measure $\mathrm{exact}\mu$ is $1/|\mathrm{Aut}|$ on a representative; classMuOn is its descent to that quotient via Quotient.lift and the congruence exactMu_congr.
classMu simply packages that descended measure on a full shell element: read off the signature counts from the first component of $c$ and evaluate the lifted measure on the second (quotient) component.
proof idea
One-line definitional wrapper. Unpack the shell element $c$ as a dependent pair (signature, quotient class), extract vertex/edge/tetrahedron counts via the signature projections, and apply the already-constructed quotient measure classMuOn at those counts to the class component. No new proof obligations: well-definedness was discharged when classMuOn lifted exactMu through exactMu_congr.
why it matters
Stage-2 of the exact-shell program needs a canonical positive class weight bounded by 1 so that regulated shell terms admit a modulus bound by regulator times shell cardinality. This definition is that weight.
Immediate parents: positivity and the unit upper bound (classMu_pos, classMu_le_one); the regulated shell term and its norm bound (zRSUVShell, norm_zRSUVShell_le); shell mass. On the bridge side it feeds measure preservation under cap-to-shell transport (classMu_capToShell) and the headline finite-sum reindexings that equate capped phased sums with exact-shell cutoffs (sum_shellsUpTo_eq_exactComplexityCutoff, phasedZq_eq_exactComplexityCutoff).
It does not touch continuum limits, physical actions, or regulator removal: those stay open or RED per the module protocol. Within the gravity seven-gaps ledger it is pure scaffolding for the UV-regularized shell series, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.