shellMass_unbounded
plain-language theorem explainer
Shell masses diverge: for every real threshold C there is some shell index n with total 1/|Aut| mass strictly above C. Gravity and path-sum analysts cite this as the quantitative engine of the zero-phase regulator-removal no-go. The proof picks n large enough that the elementary lower bound n^(3n) already exceeds C.
Claim. For every real number $C$ there exists a natural number $n$ such that the shell mass $M_n := \sum_{[\sigma]} 1/|\mathrm{Aut}(\sigma)|$ satisfies $C < M_n$.
background
This module sits in the Seven Gaps gravity campaign and targets the Gaussian-regulated quotient path sum $Z_{\mathrm{RS},\mathrm{uv}}$ of ExactShellGaugeUV. At zero phase the regulated terms are real and nonnegative, so absolute divergence of shell masses blocks any $\rho\to 0^+$ limit.
Shell mass $M_n$ is the sum of per-class measures $1/|\mathrm{Aut}|$ over the exact-complex quotient at shell level $n$. By the Burnside/orbit-stabilizer identity, that sum equals the labeled count divided by the full relabeling gauge volume $v!,e!,t!$. Restricting to the diagonal signature $(n,n,n)$ and using $n!\le n^n$ yields the elementary lower bound $M_n\ge n^{3n}$ (via shellMass_lower).
The local setting is deliberately narrow: positivity at zero phase makes a single diverging shell enough to kill regulator removal. Oscillatory nonzero phases remain open; cancellation could in principle restore a limit.
proof idea
Tactic proof, short and elementary. Apply exists_nat_gt C to obtain $m>C$, then set $n=\max(1,m)$ so $n\ge 1$ and $n\ge m$. Invoke the lower bound shellMass_lower n: $n^{3n}\le M_n$. Separately, Nat.le_self_pow gives $n\le n^{3n}$ for $n\ge 1$; cast to $\mathbb{R}$. Chain $C<m\le n\le n^{3n}\le M_n$ by linarith. No Burnside or path-sum machinery is needed at this step; only the pre-proved polynomial lower bound on shell mass.
why it matters
This is the quantitative divergence step that feeds the headline kernel no-go not_hasZRSRegulatorRemoval_zeroPhase: any putative limit $L$ is beaten by a single shell of mass $>L.\mathrm{re}+2$ whose regulated contribution tends to its full mass as $\rho\to 0^+$. The status structure RegulatorRemovalNoGoStatus records shell_mass_divergence_proved, and regulatorRemovalNoGoStatus_grounded ties that flag to this theorem.
In the Recognition Science gravity program this closes the absolute/positive-term route to removing the UV regulator on the exact-shell quotient sum. It does not touch the eight-tick octave, $J$-cost uniqueness, or the $\phi$-ladder mass formula; those live upstream of the path-sum construction. The honest open boundary remains oscillatory removal at nonzero phase (OscillatoryRemovalOpen), which positivity cannot address.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.