shellMass_pos
plain-language theorem explainer
Every exact complexity shell has strictly positive total measure: the sum of per-class measures over the shell is positive. Non-vacuity proofs for the Gaussian-UV regulated path sum, single-shell lower bounds, and continuum/tail blockers cite this. The proof is a one-line Finset sum-positivity argument from per-class positivity and a nonempty shell.
Claim. For every natural number $n$, the total shell measure $\sum_{c}\mu(c)$ over the exact complexity shell of level $n$ is strictly positive: $0 < \mathrm{shellMass}(n)$.
background
This module packages the quotient-class path-sum configuration space into exact complexity shells (no size caps) and studies the shell-resummed path sum with a hand-inserted Gaussian UV factor $\exp(-\rho n^2)$. Honesty tags: the regulator is mathematical, not derived physics; the phase/action is a free parameter on classes; regulator removal $\rho\to 0^+$ stays a named open; nothing here is a physical continuum limit.
The total shell measure is the finite sum of per-class measures over the exact path classes at complexity $n$. Each class measure is $1/|\mathrm{Aut}|$ on the quotient, already proved strictly positive. Shells are inhabited (witness: $n$ isolated vertices), so the index set of the sum is a nonempty finite type. Upstream positivity of the class measure is the only nontrivial input.
proof idea
One-line term proof. Apply Finset.sum_pos to the sum defining the shell measure: the summand is the per-class measure, which is positive on every class by the upstream theorem that every class measure is strictly positive, and the universe of the finite type of exact path classes at level $n$ is nonempty. No further algebraic reduction.
why it matters
Stage-2 non-vacuity for the regulated theory rests on this fact. At zero phase each shell term is $\exp(-\rho n^2)$ times the shell measure, so positivity of the measure yields strictly positive real part for every shell term and, via the $n=0$ term, for the full regulated path sum. Downstream single-shell lower bounds use the same product as a floor under the real part of the regulated sum.
Continuum and balance blockers also depend on it: the norm of a shell-constant amplitude equals the shell measure only after absolute value can drop via positivity; zero-phase tail-cancellation and epsilon-one failure arguments need positive shell masses that grow at least like $n^{3n}$. The result does not touch regulator removal or any FullTheoryLedger continuum flag; those remain open or red by module protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.