zeroPhase
plain-language theorem explainer
The constant zero action on exact complexity shells: every equivalence class of labeled complexes of complexity n is assigned phase S = 0. Downstream UV-summability, non-vacuity, and regulator-removal no-go theorems cite it as the canonical test phase. The body is the constant function returning 0.
Claim. The zero phase is the function that assigns to every natural number $n$ and every exact complexity shell class of complexity $n$ the real value $0$. Equivalently, $S \equiv 0$ on all classes.
background
This module builds the quotient-class path-sum configuration space as exact complexity shells (no size caps) and studies the shell-resummed path sum with a hand-inserted Gaussian UV regulator $\exp(-\rho n^2)$. The action/phase on classes is an arbitrary parameter: any GlobalEquivalent-invariant real function on labeled complexes. Nothing here derives a physical continuum limit or a physical action.
An exact complexity shell ExactPathClass n is the set of combinatorially distinct exact complexes of complexity exactly $n$: a disjoint union over shell signatures of the quotient of the exact labeled class by global equivalence. No bounded-complex cap type appears in that definition.
The regulated shell amplitude is built from a per-class measure (essentially $1/|\mathrm{Aut}|$) times a unitary weight $e^{iS}$. Setting $S \equiv 0$ collapses the weight to $1$, so each shell term becomes a positive real multiple of the shell mass times the Gaussian factor.
proof idea
Pure definition: the constant function fun _ _ => 0. No lemmas, no tactics. Downstream proofs unfold this definition and reduce complex shell terms to real multiples of shellMass n via Complex.ofReal.
why it matters
Zero phase is the canonical test phase for Stage 2 of the exact-shell UV story. It feeds zRSUVShell_zeroPhase_eq (shell term equals $\exp(-\rho n^2)\cdot\mathrm{shellMass},n$), the positivity theorems zRSUVShell_zeroPhase_re_pos and Z_RS_uv_zeroPhase_re_pos (regulated sum has strictly positive real part for every $\rho>0$, so the theory is non-vacuous), and the grounding theorem exactShellGaugeUVStatus_grounded.
It is also the headline counterexample for regulator removal: not_hasZRSRegulatorRemoval_zeroPhase proves there is no $\rho\to 0^+$ limit at zero phase, because shell masses diverge and a single late shell beats any putative limit. The FullTheoryLedger blocker gap2_cutoff_limit_blocker_certified records that zero phase fails the oscillatory-tail cancellation condition required for cutoff-limit convergence. Per the module honesty protocol, regulator removal stays a named open (HasZRSRegulatorRemoval false); this definition supplies the concrete phase that makes the no-go sharp.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.