Z_RS_uv
plain-language theorem explainer
The Gaussian-UV-regularized recognition path sum at regulator strength ρ is the complex tsum over exact complexity shells of the regulated shell terms. Anyone working the Seven Gaps path-sum ledger or the regulator-removal no-go cites this as the target object of cutoff convergence and of the open ρ→0⁺ limit. The body is a one-line definition: sum the per-shell contributions zRSUVShell.
Claim. For regulator strength $\rho\in\mathbb{R}$ and any phase assignment on exact complexity shells (a real-valued function on combinatorial classes of exact complexes of complexity $n$), the regulated path sum is $Z_{\mathrm{RS}}^{\mathrm{uv}}(\rho,\mathrm{phase}):=\sum_{n=0}^{\infty} z_n(\rho,\mathrm{phase})\in\mathbb{C}$, where each $z_n$ is the Gaussian-regulated shell term $\mathrm{e}^{-\rho n^2}$ times the class-measure-weighted unitary sum over $\mathrm{ExactPathClass}\,n$.
background
This module builds the quotient-class path-sum configuration space as exact complexity shells with no size caps, then inserts a hand-chosen Gaussian UV factor $\mathrm{e}^{-\rho n^2}$ so the shell series converges for every $\rho>0$. Complexity of a complex is $\max(n_V,n_E,n_T)$; the exact shell $\mathrm{ExactPathClass},n$ is the disjoint union over shell signatures of labeled exact complexes modulo global relabeling equivalence. No $\mathrm{BoundedComplex}$ cap appears in the shell type.
The per-shell building block is $z_{\mathrm{RS}}^{\mathrm{UV}}(\rho,\mathrm{phase},n)=\mathrm{e}^{-\rho n^2}\sum_{c}\mu(c),\mathrm{e}^{i,\mathrm{phase}(n,c)}$, with class measure $\mu=1/|\mathrm{Aut}|$. The phase map is an arbitrary GlobalEquivalent-invariant real function on classes, not a derived physical action. Module honesty: the regulator is mathematical, not physics; regulator removal and continuum/mesh limits are explicitly not claimed here.
proof idea
Pure definition: $Z_{\mathrm{RS}}^{\mathrm{uv}}$ is the unconditional tsum of the already-defined shell terms zRSUVShell ρ phase n over $n:\mathbb{N}$. No tactic proof. Well-definedness as a genuine sum (rather than a formal series) is deferred to the companion summability theorem for $\rho>0$, which then feeds the cutoff-convergence statement that partial sums tend to this tsum.
why it matters
This is the Stage-2 target object of the exact-shell Gaussian-UV wave (S2d in the module ledger). Cutoff convergence (zRSUVCutoff_tendsto) identifies complexity-truncated partial sums with this tsum for $\rho>0$. Non-vacuity at zero phase (Z_RS_uv_zeroPhase_re_pos) shows the real part is strictly positive, so the regulated functional is not identically zero. The named open HasZRSRegulatorRemoval is literally existence of $\lim_{\rho\to 0^+} Z_{\mathrm{RS}}^{\mathrm{uv}}(\rho,\mathrm{phase})$; the status flag stays false. Downstream, the RegulatorRemovalNoGo headline proves that limit fails at zero phase because shell masses diverge. Class-pushforward status and the grounded exact-shell status theorem both reference this object when recording what is proved versus open. Nothing here flips continuum-limit or FullTheoryLedger flags: complexity cutoff is not mesh refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.