shellMass_lower
plain-language theorem explainer
For every natural number n, the total shell mass (sum of 1/|Aut| over exact-path classes) is at least n^(3n). Anyone citing the zero-phase regulator-removal no-go or the shell-mass divergence uses this bound. The proof compares labeled cube entropy n^(6n) against the gauge volume (n!)^3, then invokes the Burnside shell-mass identity and a cube-to-shell comparison.
Claim. For every natural number $n$, $n^{3n} \le M_n$, where $M_n$ is the shell mass: the sum of the per-class measures $1/|\mathrm{Aut}|$ over the quotient of exact complexes of signature $(n,n,n)$ by relabeling. Equivalently $M_n \ge n^{6n}/(n!)^3 \ge n^{3n}$.
background
This module sits in the Seven Gaps gravity stack and proves a kernel no-go: the Gaussian-regulated quotient path sum has no $\rho \to 0^+$ limit at zero phase. The mechanism is quantitative shell-mass divergence, not a soft incompleteness claim.
An exact complex of signature $(v,e,t)$ is a cap-free combinatorial complex with exactly $v$ vertices, $e$ edges, and $t$ tetrahedra. Relabelings act by bijections of the three index sets; the quotient carries the descended per-class measure $\mathrm{classMuOn}$, equal to $1/|\mathrm{Aut}|$ on each orbit. The shell mass $M_n$ sums those measures over all exact signatures of total complexity $n$ (or, for the lower bound, at least over the cube signature $(n,n,n)$).
Upstream, the Burnside/orbit-stabilizer identity equates the sum of per-class measures on a fixed signature to the labeled count divided by the full relabeling volume $v!,e!,t!$. The cardinality of exact complexes of signature $(n,n,n)$ is $n^{6n}$. Factorial growth $n! \le n^n$ then makes labeled entropy beat the gauge volume.
proof idea
Three elementary comparisons, then two named shell lemmas.
First, $n! \le n^n$ three times yields $(n!)^3 \le n^{3n}$. Second, the exact-complex card formula specializes to $|\mathrm{ExactComplex}(n,n,n)| = n^{6n}$. Third, rearrange in $\mathbb{R}_{>0}$ to get $n^{3n} \le n^{6n}/(n!)^3$.
The right-hand side is rewritten by the Burnside identity sum_classMuOn_eq_card_div_factorials as the sum of classMuOn over the quotient of the cube signature. That cube sum is at most the full shell mass by cube_sum_le_shellMass. Chaining these inequalities gives $n^{3n} \le M_n$.
why it matters
This is the quantitative engine under the headline divergence shellMass_unbounded: for every real threshold $C$ some shell has mass $> C$, proved by feeding $n = \max(1,\lceil C\rceil)$ into the $n^{3n}$ lower bound. The module status record flags shell-mass divergence as proved via this lemma.
Downstream continuum blockers reuse it directly. At zero phase the unregulated exact-shell amplitude equals the real shell mass, so $n^{3n}$ growth supplies one-shell blocks of norm $> 1$ past any tail threshold (zeroPhase_epsilon_one_failure, zeroPhase_not_exactShellTailCancellation). The shell-balance blocker also gets $M_n > 1$ for $n \ge 2$ from the same power.
In the Recognition gravity program this kills the absolute/positive-term route to regulator removal at zero phase: labeled entropy beats factorial gauge volume, so the regulated sum cannot settle. Oscillatory (nonzero-phase) removal remains openly unproved; positivity is essential here and does not transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.