hasExactComplexityCutoffLimit_iff_tailCancellation
plain-language theorem explainer
The unregulated exact-shell complexity cutoff converges in ℂ if and only if late contiguous blocks of exact shell amplitudes cancel in norm. Gravity and continuum-blocker arguments cite this as the ordered-tail form of the cutoff-removal premise. The proof equates the limit to the Cauchy criterion via telescoping differences of cutoffs and completeness of ℂ.
Claim. For any real phase assignment on exact path classes, the sequence of unregulated exact-shell complexity cutoffs has a limit in $\mathbb{C}$ if and only if for every $\varepsilon>0$ there exists $N$ such that whenever $N\le m\le n$, the norm of the sum of exact shell amplitudes over the ordered block $(m,n]$ is strictly less than $\varepsilon$.
background
This module (Seven Gaps, P2-a) isolates analytic obligations for removing a complexity cutoff from phased quotient path sums. Limits here are cutoff removal only: not mesh refinement, continuum geometry, or a derived measure.
HasExactComplexityCutoffLimit phase asserts existence of $L\in\mathbb{C}$ with the exact-shell cutoff sequence tending to $L$ at infinity. ExactShellTailCancellation phase is the uniform tail condition: every late contiguous block of exact shell amplitudes is small in norm (blocks written as Ico (m+1) (n+1) for the interval $(m,n]$).
The fixed-cap side already has Cauchy $\leftrightarrow$ oscillatory tail via telescoping of $Z_{\mathrm{cap}}$. The present statement is the parallel ordered-tail IFF on the unregulated exact-shell API. Completeness of $\mathbb{C}$ turns Cauchy into existence of a limit; the difference of two cutoffs is exactly the intervening ordered shell block.
proof idea
Both directions are pure metric Cauchy bookkeeping.
Forward: from a limit, the cutoff sequence is Cauchy. Unpack Metric.cauchySeq_iff, pick $N$ for $\varepsilon$, and for $N\le m\le n$ rewrite the distance of cutoffs as the norm of the intervening shell block via exactComplexityCutoff_sub (and norm_sub_rev).
Reverse: from tail cancellation, build CauchySeq on the cutoff sequence. For any pair $m,n\ge N$, case on le_total m n; each order reduces the distance to a tail block norm controlled by the hypothesis. Conclude existence of the limit by cauchySeq_tendsto_of_complete.
why it matters
Headline IFF for the ordered-tail form of cutoff removal: a substrate-derived oscillatory phase must supply exactly this cancellation if the unregulated exact-shell quotient is to converge.
Downstream, not_hasExactComplexityCutoffLimit_zeroPhase rewrites through this IFF and the zero-phase failure witness, so zero phase is ruled out without assuming any desired limit. hasPhasedZqLimit_iff_exactShellTail_of_compatibility composes it with cap-to-shell compatibility to certify that phased $Z_q$ convergence is equivalent to exact-shell tail cancellation. zeroPhase_compatibility_and_limit_impossible uses that bridge as a discriminant against trivial phase models. The Gap2 package equates banked OscillatoryTail with this ordered cancellation via the same Cauchy/completeness spine.
In the Seven Gaps gravity stack this is the analytic premise a recognition-derived phase must prove; it does not itself force the eight-tick octave or $D=3$, but it is the blocker those structures must clear when removing complexity cutoffs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.