classMuOn
plain-language theorem explainer
On each fixed signature (v,e,t), the discrete-gravity measure μ(K)=1/|Aut K| descends to a well-defined real-valued function on global-equivalence classes of exact complexes. Anyone working the shell-resummed path sum or the regulator-removal no-go cites this as the per-class weight. The definition is a one-line Quotient.lift of exactMu, justified by exactMu_congr.
Claim. For fixed $v,e,t\in\mathbb{N}$, the map sending an exact labeled complex $K$ to $\mu(K)=1/|\mathrm{Aut}\,K|$ is constant on global-equivalence classes, hence induces a well-defined function $\overline{\mu}:\mathrm{ExactComplex}(v,e,t)/\sim\to\mathbb{R}$ on the quotient.
background
This module builds exact complexity shells for the Recognition Science path-sum configuration space: complexes with fixed vertex/edge/triangle counts $(v,e,t)$, no size caps, quotiented by global relabeling. The module is explicit that the Gaussian UV factor $\exp(-\rho n^2)$ is a hand-inserted mathematical regulator, not derived physics, and that $\rho\to 0^+$ remains open.
Upstream, exactMu assigns to each labeled exact complex the standard discrete-gravity weight $\mu(K)=1/|\mathrm{Aut},K|$. The theorem exactMu_congr states that this weight is invariant under GlobalEquivalent (via the induced automorphism-group isomorphism). The setoid exactSetoid v e t packages that equivalence relation on ExactComplex v e t.
Once invariance is in hand, the natural next object is the function on classes rather than on labeled representatives. That is exactly what this definition supplies: the per-class measure used by every shell mass and regulated path-sum term that follows.
proof idea
One-line definitional wrapper: Quotient.lift exactMu applied to the proof that equal classes have equal measure. The lift hypothesis is discharged by exactMu_congr, which rewrites $\mathrm{card}(\mathrm{Aut},K)$ under the automorphism congruence induced by a global relabeling. No further arithmetic is needed; well-definedness is pure setoid descent.
why it matters
Stage 2 of the exact-shell program needs a class-level measure before any shell sum or UV series can be stated. This definition is that measure on a fixed signature; the sibling classMu specializes it to an ExactPathClass n element via the signature projections.
Downstream it is the weight in the shell-mass identity used by regulatorRemovalNoGoStatus_grounded (sum of class measures equals labeled count over $v!,e!,t!$), in the cube lower bound cube_sum_le_shellMass, and in the representative evaluation classMuOn_out. The CapShellBridge theorem classMu_capToShell ties it to the older capped triangulation measure, so capped and exact-shell bookkeeping agree on classes.
Within the Seven Gaps honesty protocol this object is fully proved infrastructure; it does not touch continuum limits, physical actions, or the still-open regulator-removal flag. It simply makes the discrete path-sum weight live on the correct quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.