hasPhasedZqLimit_iff_exactShellTail_of_compatibility
plain-language theorem explainer
Under cap-to-shell sum compatibility, the phased capped quotient path sum converges as the complexity cutoff is removed if and only if exact-shell amplitudes cancel in every late contiguous block. Gravity and continuum-limit auditors cite this as the Gap-2 cutoff blocker certificate. The proof identifies the two finite-sum sequences by the compatibility hypothesis, then applies the exact-shell Cauchy/tail equivalence.
Claim. Fix a family $P$ of phase models at each complexity cap and a phase assignment on exact path classes of each shell. If the finite phased capped sums of $P$ equal the exact-shell cutoffs at every cap $B$, then the capped phased sequence has a complexity-cutoff limit in $\mathbb{C}$ if and only if every sufficiently late contiguous block of exact-shell amplitudes is arbitrarily small in norm.
background
Module P2-a isolates analytic obligations for removing the complexity cutoff from the phased quotient path sum. A CapPhaseFamily assigns a phase model at every cap $B$ with no cross-cap coherence. The existing finite sums form phasedZqSequence P; HasPhasedZqComplexityLimit asserts that this sequence tends to some $L\in\mathbb{C}$ at infinity. That is a cutoff-removal statement, not mesh refinement.
The cap-free side uses ExactPathClass n: combinatorially distinct exact complexes of complexity exactly $n$, with no bounded-complex cap type. Exact-shell cutoffs and amplitudes yield ExactShellTailCancellation: for every $\varepsilon>0$ there is $N$ so that every block of shells $(m,n]$ with $N\le m\le n$ has total amplitude norm less than $\varepsilon$. Completeness of $\mathbb{C}$ and exact telescoping already give Cauchy criteria on each API separately.
The missing bridge is CapShellCompatibility: equality of the two finite sums at every cap. The module doc states this is the smallest cross-API statement needed; current definitions do not supply it. Under that bridge alone, the two convergence notions coincide.
proof idea
Term-mode, four steps. From compatibility, sum_eq gives pointwise equality of phasedZqSequence P and exactComplexityCutoff phase; funext promotes that to sequence equality. Unfold HasPhasedZqComplexityLimit (existence of a limit of the phased sequence). Rewrite along the identified sequences. Finish by the already-proved equivalence hasExactComplexityCutoffLimit_iff_tailCancellation, which converts exact-shell cutoff convergence into ordered tail cancellation. No new analysis is done here; the certificate is pure transport across the compatibility bridge.
why it matters
This is the blocker certificate named in the module: once compatibility is supplied, desired convergence of phased $Z_q$ is exactly the ordered-tail cancellation obligation on exact shells, with no convergence assumed a priori. Downstream, gap2_cutoff_limit_blocker_certified in the full-theory ledger packages it as half of Pillar 2: a substrate-derived phase must make late exact-shell blocks small, and the capped $Z_q$ API must match the nonduplicating shell decomposition; zero phase fails cancellation.
The Gap-2 composition package uses it as a banked lemma: oscillatory tail plus banked compatibility yields the capped complexity-cutoff limit on the transported family. Locally, zeroPhase_compatibility_and_limit_impossible applies the iff to show a zero-phase capped family cannot both be compatible and converge. In the Seven Gaps gravity program this pins Gap 2's continuum/measure half to two exact obligations rather than an open analytic wish. It does not touch T5–T8 forcing, RCL, or the $\alpha$ band; it is ledger infrastructure for cutoff removal only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.