zRSUVShell_zeroPhase_eq
plain-language theorem explainer
At vanishing phase, each Gaussian-UV shell contribution collapses to the real scalar exp(-ρ n²) times the shell mass. Anyone proving non-vacuity or single-shell lower bounds for the regulated RS path sum cites this identity. The proof unfolds the shell sum and kills every complex exponential by exp(0)=1 and 0·z=0.
Claim. For every regulator strength $\rho\in\mathbb{R}$ and every complexity level $n\in\mathbb{N}$, the UV-regulated shell term at the zero phase equals the complexification of the real number $e^{-\rho n^{2}}\cdot m(n)$, where $m(n)$ is the shell mass (sum of class measures $1/|\mathrm{Aut}|$ over the exact complexity-$n$ path classes).
background
This module builds the Recognition Science path sum on exact complexity shells: equivalence classes of labeled complexes under global relabeling, with no size caps in the shell definition. Each shell $n$ carries a finite set of classes; the class measure is $1/|\mathrm{Aut}|$, and the shell mass $m(n)$ is the sum of those measures. The UV-regulated shell term multiplies each class weight by a Gaussian $e^{-\rho n^{2}}$ and a unitary phase factor coming from an arbitrary GlobalEquivalent-invariant action on classes.
The honesty protocol is binding: the Gaussian is a hand-inserted mathematical regulator, not derived physics; the phase/action is a free parameter; regulator removal $\rho\to 0^{+}$ remains a named open (HasZRSRegulatorRemoval, flag false). Nothing here is a continuum or mesh-refinement limit.
Zero phase means the action contribution is identically zero, so every class weight is pure real. The theorem records the resulting closed form of the shell term.
proof idea
Unfold the definitions of the regulated shell term, the zero phase map, and shell mass. Rewrite the complexification of a real product and of a real finite sum. Congruence on the outer product leaves a Finset sum; pointwise, each summand has phase factor $e^{i\cdot 0}=1$ and the imaginary part of the phase input is zero, so mul_zero, Complex.exp_zero, and mul_one reduce every class contribution to its real class measure. The sum of those measures is exactly the shell mass, yielding $e^{-\rho n^{2}}\cdot m(n)$ as a complex number.
why it matters
This identity is the algebraic gateway from the general complex shell term to the real nonnegative regime used throughout Stage 2 of the module. Downstream, zRSUVShell_zeroPhase_re_pos rewrites with it and applies positivity of the exponential and of shell mass to get a strictly positive real part on every shell. That feeds Z_RS_uv_zeroPhase_re_pos (S2e non-vacuity): the regulated path sum at zero phase is not the zero functional, because all terms are nonnegative real and the $n=0$ term is positive. The same rewrite supplies single_shell_re_lower_bound in the regulator-removal no-go module: any single shell bounds $\mathrm{Re},Z_{\mathrm{RS}}^{\mathrm{uv}}$ from below by $e^{-\rho n_0^{2}} m(n_0)$.
Within the Seven Gaps program this is pure Stage-2 bookkeeping for the Gaussian-regularized path sum. It does not touch the forcing chain (T5–T8), RCL, or continuum flags; those stay red by the module’s own disclosures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.