norm_zRSUVShell_le
plain-language theorem explainer
The Gaussian-regulated exact-shell path-sum term has complex modulus at most exp(-ρ n²) times the number of exact path classes of complexity n. Anyone bounding the UV-regularized RS path sum cites this modulus estimate. The proof separates the real regulator, applies the triangle inequality, and uses μ ≤ 1 with unit phases.
Claim. For every regulator strength $\rho \in \mathbb{R}$, every phase assignment on exact complexity shells, and every $n \in \mathbb{N}$, the complex modulus of the regulated shell term satisfies $\|Z^{\mathrm{UV}}_{\mathrm{shell}}(\rho,\mathrm{phase},n)\| \le e^{-\rho n^2}\,|\mathrm{ExactPathClass}(n)|$, where $\mathrm{ExactPathClass}(n)$ is the set of combinatorially distinct exact complexes of complexity exactly $n$.
background
This module builds the quotient-class path-sum configuration space into exact complexity shells with no size caps, then inserts a hand-chosen Gaussian UV regulator $\exp(-\rho n^2)$ and studies the resulting shell series. The honesty protocol is explicit: the regulator is mathematical, not derived physics; the phase is an arbitrary class function; regulator removal $\rho\to 0^+$ remains a named open.
An exact complexity shell $\mathrm{ExactPathClass}(n)$ is the disjoint union, over shell signatures of total complexity $n$, of the quotient of exact labeled complexes by global relabeling equivalence. The per-class measure is $\mu(c)=1/|\mathrm{Aut}(c)|$, proved positive and at most one. The regulated shell term is the real Gaussian factor times the finite sum over classes of $\mu(c),e^{i,\mathrm{phase}(n,c)}$.
Stage 1 already supplies finiteness of each shell and the entropy bound on its cardinality. The present result is the Stage-2 modulus bound (S2b) that feeds summability for every $\rho>0$.
proof idea
Unfold the shell term and factor the real Gaussian via multiplicativity of the complex norm; positivity of the exponential removes the absolute value. It remains to bound the finite class sum. Triangle inequality replaces the norm of the sum by the sum of norms. For each class, multiplicativity again splits $|\mu(c),e^{i\theta}|$; the complex exponential on the imaginary axis has norm one, and $\mu(c)\le 1$ with $\mu(c)>0$ yields a contribution at most $1$. The resulting constant sum equals the Fintype cardinality of the shell, rewritten as $\mathrm{Nat.card}$.
why it matters
This is the pure modulus bound (S2b) in the exact-shell UV program: regulator times shell cardinality, using only $\mu\le 1$ and unit phases. The immediate parent is norm_zRSUVShell_le_entropy, which composes it with the Stage-1 entropy estimate $\mathrm{card}(\mathrm{ExactPathClass},n)\le(n+1)^{12(n+1)}$ to get an explicit $n$-only majorant. That majorant is what makes the shell series summable for every $\rho>0$ and lets cutoff partial sums converge to the regulated path sum $Z_{\mathrm{RS}}^{\mathrm{uv}}$.
In the Seven Gaps ledger this closes a proved Stage-2 step without touching continuum claims. Regulator removal, mesh refinement, and any physical action remain open; the module flips no FullTheoryLedger continuum flag. The bound is the analytic gate between exact combinatorial shells and a well-defined regularized path sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.