zeroPhase_fails_both_removal_routes
plain-language theorem explainer
The zero phase on exact path classes fails both available complexity-cutoff removal routes: the unregulated exact-shell limit and the positive Gaussian regulator-removal limit. Gravity and path-sum workers cite this as the concrete discriminant against the trivial phase. The proof is a one-line pairing of two prior no-go lemmas. Neither conjunct is a mesh-refinement or physical-continuum claim.
Claim. The zero phase assignment on exact path classes admits neither an unregulated exact-shell complexity-cutoff limit in $\mathbb{C}$ nor a positive Gaussian ZRS regulator-removal limit.
background
This module isolates the analytic obligations for removing the complexity cutoff from the phased quotient path sum (Seven Gaps, P2-a). Two APIs sit side by side. The fixed-cap API builds a sequence of finite phased quotient sums; completeness of $\mathbb{C}$ makes existence of a limit equivalent to the Cauchy criterion. The cap-free exact-shell API sums exact quotient shells via $Z_{\mathrm{cap}}(\mathrm{phase}, B)$ and quantifies late shell blocks by an oscillatory tail. Exact telescoping yields Cauchy of the capped sequence iff the oscillatory-tail criterion holds.
HasExactComplexityCutoffLimit phase asserts existence of $L \in \mathbb{C}$ such that the exact-shell complexity cutoff tends to $L$ at infinity; the module doc stresses this is not mesh refinement. The companion route is positive Gaussian ZRS regulator removal (imported from RegulatorRemovalNoGo). The zero phase is the constant-zero assignment on exact path classes; the module notes it has an explicit $\varepsilon=1$ failure witness for tail cancellation.
All limits here only remove a complexity cutoff. They carry no claim about continuum geometry, observations, rates, derived measures, or the full-theory ledger.
proof idea
Term-mode pairing of two already-proved no-gos. The first conjunct is not_hasExactComplexityCutoffLimit_zeroPhase (zero phase fails the unregulated exact-shell cutoff limit). The second is RegulatorRemovalNoGo.not_hasZRSRegulatorRemoval_zeroPhase (zero phase fails positive Gaussian regulator removal). The proof is the pair constructor on those two lemmas; no new analysis is done here.
why it matters
Inside the Seven Gaps P2-a blocker, this packages the two independent failures of the trivial phase into a single conjunction. Downstream, zeroPhase_compatibility_and_limit_impossible uses the exact-shell half (via the compatibility bridge) as a concrete discriminant: a zero-phase capped family cannot both agree with the exact-shell decomposition and possess a complexity-cutoff limit.
The module still lacks the cross-API bridge CapShellCompatibility equating capped quotient sums with nonduplicating exact-shell cutoffs. Until that bridge exists, convergence of phased $Z_q$ is not formally identified with exact-shell tail cancellation. This theorem does not close that gap; it only records that zero phase is already ruled out on both removal routes that the current API exposes.
Framework-wise this is a gravity/path-sum obstruction, not a forcing-chain (T0–T8) step. It keeps the continuum-limit story honest: cutoff removal is analytic, not geometric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.