zeroPhase_not_exactShellTailCancellation
plain-language theorem explainer
Zero phase fails the exact-shell ordered-tail cancellation criterion: late one-shell blocks already have norm greater than one. Anyone arguing that a substrate phase must supply oscillatory cancellation for complexity-cutoff removal will cite this non-vacuity witness. The proof takes ε = 1, isolates a single late shell, and uses the shell-mass lower bound growing at least like n^(3n).
Claim. The zero phase map does not satisfy exact-shell tail cancellation: it is not the case that for every $\varepsilon > 0$ there exists $N$ such that every contiguous block of exact-shell amplitudes with indices past $N$ has complex norm strictly less than $\varepsilon$.
background
This module (Seven Gaps, P2-a) isolates analytic obligations for removing a complexity cutoff from the phased quotient path sum. Completeness of $\mathbb{C}$ makes Cauchy equivalent to existence of a limit for the capped sequence. On the exact-shell side, $Z_{\mathrm{cap}}(\mathrm{phase}, B)$ sums shells in range B, and the panel-locked OscillatoryTail quantifies every late contiguous block. Exact telescoping yields Cauchy iff oscillatory tail cancellation.
ExactShellTailCancellation phase is that cancellation statement: for every $\varepsilon > 0$ there is $N$ so that whenever $N \le m \le n$, the norm of the sum of exactShellAmplitude phase over the half-open index block $(m,n]$ is $< \varepsilon$. At zero phase the shell term collapses to the real positive shell mass: $\mathrm{shellMass}, n = \sum_c \mu(c)$ over exact path classes of length $n$, and every shell has strictly positive measure.
Upstream, shellMass_pos and the regulator-removal lower bound shellMass_lower supply the growth $\mathrm{shellMass}, n \ge n^{3n}$ (up to the concrete inequality used in the proof). The module stresses that these limits only remove a complexity cutoff; they make no continuum-geometry or observation claim.
proof idea
Assume tail cancellation at zero phase and instantiate at $\varepsilon = 1$ to obtain a threshold $N$. Set $k = \max(2,N)$ and consider the single-shell block from $k$ to $k+1$. The Ico sum identity reduces that block to the lone term exactShellAmplitude zeroPhase (k+1).
Rewrite that amplitude via the zero-phase formula: it is the real shell mass, whose absolute value is the mass itself by positivity. The cancellation hypothesis then forces $\mathrm{shellMass}(k+1) < 1$. But shellMass_lower plus $k \ge 2$ give $1 < \mathrm{shellMass}(k+1)$ (via the comparison $k+1 \le (k+1)^{3(k+1)}$ cast to $\mathbb{R}$). linarith closes the contradiction.
why it matters
This is the explicit epsilon-one non-vacuity witness that the zero phase cannot supply the cancellation a substrate-derived phase must provide for cutoff removal. Downstream, not_hasExactComplexityCutoffLimit_zeroPhase rewrites the exact complexity-cutoff limit through the tail-cancellation iff and applies this theorem directly. The stronger discriminant zeroPhase_compatibility_and_limit_impossible then shows a zero-phase capped family cannot both agree with the exact-shell decomposition and possess a phased $Z_q$ complexity-cutoff limit.
In the Seven Gaps gravity program this blocks the trivial phase choice on the phased-quotient path: without genuine oscillation the ordered shell masses grow too fast for Cauchy. It does not yet close the missing CapShellCompatibility bridge between capped triangulation classes and exact path classes; it only shows that whatever fills that bridge cannot be zero phase if a limit is claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.