cube_sum_le_shellMass
plain-language theorem explainer
The sum of per-class measures over the single cube signature $(n,n,n)$ is at most the full shell mass at level $n$. Anyone deriving shell-mass divergence by restricting to the cube cites this comparison. The proof injects cube classes into the full path-class sum and uses positivity of every class measure.
Claim. For every natural number $n$, $$\sum_{[q]} \mu_{n,n,n}([q]) \le M_{\mathrm{shell}}(n),$$ where the sum runs over the quotient of exact complexes of signature $(n,n,n)$ by the exact setoid, $\mu$ is the per-class measure $1/|\mathrm{Aut}|$, and $M_{\mathrm{shell}}(n)$ is the sum of those measures over all exact path classes at level $n$.
background
This module is the kernel no-go for regulator removal at zero phase: the Gaussian-regulated quotient path sum has no $\rho\to 0^+$ limit when the phase is identically zero. The quantitative engine is shell mass. For each exact signature $(v,e,t)$, the Burnside/orbit-stabilizer identity equates the sum of per-class measures $1/|\mathrm{Aut}|$ over the quotient to the labeled count divided by the full relabeling volume $v!,e!,t!$.
Here classMu (equivalently classMuOn on a fixed signature) is that per-class measure on an exact path class; upstream records $0 < \mathrm{classMu},c$ for every class. The shell mass $M_{\mathrm{shell}}(n)$ is the sum of classMu over all exact path classes at level $n$. The cube signature $(n,n,n)$ is the single-signature restriction used to force divergence: labeled entropy on the cube beats the factorial gauge volume.
Local setting (module doc): positivity of every regulated term at zero phase lets one shell lower-bound the regulated sum; if shell mass is unbounded, regulator removal fails.
proof idea
Classical term-mode calc. First rewrite each cube-class measure classMuOn n n n q as classMu of the paired cube path class $\langle\mathrm{cubeSig},n,,q\rangle$ (definitional). Identify that sum with the image sum over the embedding $q\mapsto\langle\mathrm{cubeSig},n,,q\rangle$ via Finset.sum_image, using injectivity of the pairing (cases on equality of sigma pairs). The image is a subset of the full universe of exact path classes, so Finset.sum_le_sum_of_subset_of_nonneg with nonnegativity from (classMu_pos c).le lifts the partial sum to the full sum. The full sum is definitionally shellMass n.
why it matters
Feeds the sole downstream parent shellMass_lower, which upgrades the comparison to the quantitative bound $M_{\mathrm{shell}}(n)\ge n^{6n}/(n!)^3\ge n^{3n}$ (labeled cube entropy beats factorial gauge volume, using $n!\le n^n$). That lower bound is the divergence engine in the module headline: shellMass_unbounded, then single_shell_re_lower_bound, then the refutation $\neg\mathrm{HasZRSRegulatorRemoval},\mathrm{zeroPhase}$.
In the Seven Gaps gravity stack this closes the absolute/positive-term route to removing the UV regulator on the exact-shell gauge path sum. It does not touch oscillatory phases: the module explicitly leaves OscillatoryRemovalOpen open, since the lower-bound argument needs positivity destroyed by unit-phase cancellation. Framework role is local to the gravity UV/no-go chain rather than the T0–T8 forcing landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.