HasExactComplexityCutoffLimit
plain-language theorem explainer
Names the proposition that the unregulated exact-shell complexity-cutoff sequence admits a complex limit at infinity, for a given phase on exact path classes. Gravity and Seven-Gaps authors cite it when stating cutoff-removal obligations for the phased quotient path sum. It is a one-line definitional wrapper around Filter.Tendsto of the exact-shell cutoff sequence, not a mesh-refinement claim.
Claim. For a phase assignment $\mathrm{phase}$ on exact path classes of each complexity $n$, the unregulated exact-shell complexity-cutoff limit exists when there is some $L \in \mathbb{C}$ such that the exact-shell cutoff sequence (built from $\mathrm{phase}$) tends to $L$ as the complexity cutoff tends to infinity.
background
Module P2-a isolates analytic obligations for removing the complexity cutoff from the phased quotient path sum. Two APIs appear: a fixed-cap family of finite quotient sums, and a cap-free exact-shell decomposition. The exact shell at complexity $n$ is ExactPathClass n: combinatorially distinct exact complexes of complexity exactly $n$, formed as a disjoint union over shell signatures of quotients by global equivalence, with no bounded-complex cap type in the definition.
The exact-shell cutoff sequence sums phased exact shells up through successive complexities. Completeness of $\mathbb{C}$ makes existence of a limit equivalent to the Cauchy criterion, and exact telescoping identifies that criterion with uniform smallness of late contiguous shell blocks (oscillatory tail cancellation). All limits in this module remove a complexity cutoff only; they carry no continuum-geometry or mesh-refinement content.
proof idea
Definitional, not a proved theorem. The body is the standard existence statement $\exists L:\mathbb{C}$ such that exactComplexityCutoff phase tends to $L$ along atTop in the neighborhood filter. No lemmas are applied; downstream theorems unpack this Prop via the Cauchy criterion and the banked tail-cancellation IFF.
why it matters
This Prop is the unregulated exact-shell side of the cutoff-removal obligation in Seven Gaps P2-a. The headline IFF hasExactComplexityCutoffLimit_iff_tailCancellation equates it with ordered exact-shell tail cancellation: the analytic premise a substrate-derived oscillatory phase must prove. Downstream, not_hasExactComplexityCutoffLimit_zeroPhase and zeroPhase_fails_both_removal_routes use it to show the zero phase fails both available removal routes (unregulated cutoff and positive Gaussian regulator removal). The Gap2 package further identifies oscillatory tail with ordered exact-shell tail cancellation via the banked Zcap Cauchy criterion. It sits in the gravity Seven-Gaps stack that blocks naive continuum limits without genuine phase cancellation; it is not itself a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.