shellMass
plain-language theorem explainer
Shell mass at complexity n is the total measure of that exact complexity shell: the sum of the per-class measures μ over all exact path classes of complexity n. Gravity and path-sum authors cite it as the real weight that multiplies the Gaussian UV factor exp(−ρ n²) in the regulated shell term. The body is a plain finite sum over the Fintype of exact path classes.
Claim. For each natural number $n$, the shell mass is $\sum_{c}\mu(c)$, summed over all exact path classes of complexity $n$, where $\mu(c)=1/|\mathrm{Aut}(c)|$ is the per-class measure.
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells with no size caps in the shell definition, then studies the shell-resummed path sum with a hand-inserted Gaussian UV regulator $\exp(-\rho n^2)$. Honesty tags in the module doc stress that the regulator is mathematical, not derived physics, and that regulator removal ($\rho\to 0^+$) remains a named open.
An exact path class of complexity $n$ is a GlobalEquivalent-class of labeled complexes whose complexity (vertex/edge/triangle counts in the exact-complex sense) equals $n$. The shell is a Fintype. The per-class measure $\mu$ is $1/|\mathrm{Aut}|$ on each class: well-defined on classes, positive, and at most one. Shell mass simply totals those measures.
Local Stage-1 facts already in place include relabeling invariance of complexity, the exact setoid, finiteness of each shell, a polynomial-exponential card bound, and that every shell is inhabited (witness: $n$ isolated vertices).
proof idea
Definition, not a proof. The body is the Finset/Fintype sum of the per-class measure over univ of exact path classes of complexity $n$. No lemmas are applied beyond the ambient Fintype instance and the definition of the class measure.
why it matters
Shell mass is the real scalar that makes the zero-phase regulated shell term concrete: that term equals $\exp(-\rho n^2)\cdot$ shell mass, and positivity of shell mass (every shell inhabited, each $\mu>0$) feeds the non-vacuity theorem that the regulated path sum has strictly positive real part for every $\rho>0$.
Downstream, the RegulatorRemovalNoGo development uses shell mass as a lower bound target (cube-signature partial sums sit under full shell mass) and as the diverging weight in the headline kernel no-go: at zero phase there is no $\rho\to 0^+$ limit, because shell masses are unbounded and a single heavy shell defeats any putative finite limit. Grounding theorems tie status flags to these identities. Nothing here closes continuum-limit or FullTheoryLedger flags; it supplies the measure bookkeeping those no-gos and Stage-2 summability rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.