not_hasExactComplexityCutoffLimit_zeroPhase
plain-language theorem explainer
The zero phase assignment on exact path classes admits no unregulated exact-shell complexity-cutoff limit in ℂ. Gravity and path-sum workers cite it as the concrete negative witness that the trivial phase fails the cutoff-removal criterion. The proof rewrites the limit predicate to oscillatory tail cancellation and applies the known zero-phase failure of that cancellation.
Claim. Let the zero phase send every exact path class to $0$. Then there is no $L \in \mathbb{C}$ such that the exact-shell complexity-cutoff partial sums (capped at shell index $B$, as $B \to \infty$) tend to $L$. Equivalently, the unregulated exact-shell cutoff limit does not exist for the zero phase.
background
This module (Seven Gaps, P2-a) isolates analytic obligations for removing a complexity cutoff from the phased quotient path sum. Limits here only drop that cutoff; they are not mesh refinement and make no continuum-geometry claim.
The exact-shell API builds partial sums $Z_{\mathrm{cap}}(\mathrm{phase}, B)$ over shells in $\mathrm{range}, B$. Completeness of $\mathbb{C}$ equates existence of a limit to the Cauchy property. Exact telescoping further equates that Cauchy property to an oscillatory-tail statement: every sufficiently late contiguous block of exact shell amplitudes is arbitrarily small.
HasExactComplexityCutoffLimit packages existence of such an unregulated limit for a phase model on exact path classes. The zero phase is the constant-zero assignment. Module text records that this phase supplies an explicit $\varepsilon=1$ failure witness for tail cancellation, so the limit route is blocked at the cancellation step.
proof idea
One-line term proof. Rewrite the target via the equivalence between existence of the exact-shell complexity-cutoff limit and the oscillatory tail-cancellation criterion. Discharge the rewritten goal by the already-proved fact that the zero phase fails exact-shell tail cancellation.
why it matters
In the Seven Gaps gravity stack this is the negative half of the zero-phase discriminant for cutoff removal. It feeds zeroPhase_fails_both_removal_routes, which packages failure of both available routes (unregulated exact-shell cutoff and positive Gaussian regulator removal). It also supports zeroPhase_compatibility_and_limit_impossible: under any bridge equating capped quotient sums to exact-shell sums, a zero-phase family cannot be both shell-compatible and convergent.
The result is deliberately discriminating rather than constructive. A substrate-derived phase must supply genuine late-block cancellation; the trivial phase does not. That sharpens P2-a without claiming continuum gravity, a rate, or a derived measure. Framework-wise it sits in the gravity analysis layer that polices which phase models can even pose a continuum limit question, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.