hasPhasedZqComplexityLimit_iff_cauchy
plain-language theorem explainer
For any family of phase models indexed by complexity caps, the finite phased quotient sums admit a complexity-cutoff limit in ℂ if and only if their cross-cap differences form a Cauchy sequence. Gravity and continuum-blocker arguments cite this as the exact analytic criterion for removing the cutoff. The proof is the standard completeness equivalence on ℂ, rewritten in the module's norm form of the Cauchy predicate.
Claim. Let $P$ assign a phase model to every complexity cap $B\in\mathbb{N}$. Write $Z_B$ for the finite phased quotient sum at cap $B$. Then there exists $L\in\mathbb{C}$ with $Z_B\to L$ as $B\to\infty$ if and only if for every $\varepsilon>0$ there is $N$ such that $m,n\ge N$ implies $\|Z_m-Z_n\|<\varepsilon$. No continuum geometry is assumed.
background
This module (Seven Gaps, P2-a) isolates the analytic obligations for removing the complexity cutoff from the phased quotient path sum. A CapPhaseFamily is only a phase choice at each cap $B$; it supplies no cross-cap coherence by itself. The associated sequence is the finite phased quotient sum at each cap.
HasPhasedZqComplexityLimit asserts existence of a limit of that sequence in $\mathbb{C}$ as the cap tends to infinity: removal of the complexity cap, not mesh refinement. PhasedZqCauchyCriterion is the matching $\varepsilon$-$N$ Cauchy obligation on cross-cap differences of the same sequence.
The module doc states the local setting cleanly: completeness of $\mathbb{C}$ gives an exact criterion that the sequence has a limit iff it is Cauchy. Parallel exact-shell machinery (Zcap, OscillatoryTail) later converts Cauchy into uniform late-block cancellation; this theorem is the capped-API half of that bridge.
proof idea
Bidirectional constructor on the two Props.
Forward: from a limit witness $\langle L,hL\rangle$, extract the Cauchy property of the phased sequence via Metric.cauchySeq_iff, then rephrase distances as norms with dist_eq_norm to match PhasedZqCauchyCriterion.
Reverse: the Cauchy criterion is exactly Metric.cauchySeq_iff for the phased sequence; completeness of $\mathbb{C}$ via cauchySeq_tendsto_of_complete produces the limit. No phase algebra or shell combinatorics enters.
why it matters
This is the headline iff of the phased-quotient continuum blocker: it converts "the cutoff can be removed" into a pure Cauchy obligation on existing finite sums, with no convergence or continuum interpretation smuggled in.
Downstream, zeroPhase_compatibility_and_limit_impossible uses it (via the compatibility bridge to exact-shell tails) to show a zero-phase family cannot both match the exact-shell decomposition and possess a complexity-cutoff limit. That is the concrete discriminant for any proposed CapShellCompatibility implementation.
In the Seven Gaps gravity program this pins Gap P2-a: cutoff removal is equivalent to late-shell cancellation a substrate-derived phase must supply. It does not itself force a phase; it states the analytic gate any such phase must pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.