summable_zRSUVShell
plain-language theorem explainer
For every regulator strength ρ > 0 and every phase on exact complexity shells, the Gaussian-UV-regulated shell series is summable over n. Path-sum constructions in the Seven Gaps gravity stack cite this to justify the tsum that defines the regulated recognition path sum. The argument eventually dominates the shell modulus by a geometric series, using that the entropy exponent n log n is o(n²).
Claim. For every $\rho > 0$ and every real-valued phase on the exact complexity shells, the series $\sum_{n=0}^{\infty} z^{\mathrm{RS}}_{\mathrm{UV},n}(\rho,\mathrm{phase})$ is summable (absolutely, via a norm comparison).
background
This module builds the quotient-class path-sum configuration space as exact complexity shells: for each $n$, the exact path class is the disjoint union over shell signatures of labeled exact complexes modulo global relabeling. No size cap appears in the shell definition. The shell entropy bound states that the cardinality of the $n$-shell is at most $(n+1)^{12(n+1)}$.
The regulated shell term multiplies the shell sum of unitary class weights by the hand-inserted Gaussian UV factor $\exp(-\rho n^2)$. The phase is an arbitrary parameter on equivalence classes, not a derived physical action. The module is explicit that $\exp(-\rho n^2)$ is a mathematical regulator only, and that regulator removal $\rho\to 0^+$ remains open.
Summability is the Stage-2 gate that makes the full shell series a well-defined tsum rather than a formal expression. Upstream, the modulus bound on each shell term and the existence of a Gaussian domination threshold (entropy growth $n\log n = o(n^2)$) supply the comparison ingredients.
proof idea
Fix $\rho>0$. The geometric series $\sum r^n$ with $r=\exp(-\rho/2)\in(0,1)$ is summable. It remains to show that the shell term is eventually dominated in norm by $r^n$.
Invoke the Gaussian domination lemma: past some $N$, the entropy log-factor is absorbed so that $\exp(-\rho n^2)\cdot(n+1)^{12(n+1)}\le\exp(-(\rho/2)n^2)$. Then $\exp(-(\rho/2)n^2)\le r^n$ for $n\ge 1$, because $n\le n^2$ and the exponential is monotone. Chain with the shell modulus bound: $|z_n|\le\exp(-\rho n^2)\cdot(n+1)^{12(n+1)}$. Conclude by eventual norm comparison against the geometric series.
why it matters
This is the Stage-2c UV summability theorem of the exact-shell Gaussian-UV module. It grounds the uv_summability_proved flag in the module status structure and its grounding theorem.
Immediate parents: cutoff partial sums converge to the regulated path sum (one-line HasSum consequence); at zero phase the regulated sum has strictly positive real part (non-vacuity); and the regulator-removal no-go stack uses the same summability to lower-bound the real part by any single shell. Without this result the regulated path sum is not a defined complex number.
Framework placement: this is gravity-side analytic control of a combinatorial path sum, not a forcing-chain step (T0–T8). It does not touch continuum mesh refinement, physical action derivation, or $\rho\to 0^+$ removal; those stay openly red.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.