exactComplexityCutoff_sub
plain-language theorem explainer
The difference of two exact-shell complexity cutoffs equals the sum of intervening ordered shell amplitudes. Gravity and continuum-blocker arguments cite it to turn cutoff limits into tail-cancellation statements. The proof is a one-line appeal to the standard Ico telescoping identity on finite sums, after shifting the inequality by one.
Claim. For any phase assignment on exact path classes and naturals $m \le n$, the difference of exact-shell complexity cutoffs at $n$ and $m$ equals the sum of exact shell amplitudes over the half-open index interval from $m+1$ to $n+1$.
background
Module P2-a isolates analytic obligations for removing a complexity cutoff from the phased quotient path sum. Two APIs sit side by side: a fixed-cap family of finite quotient sums, and a cap-free exact-shell decomposition. Completeness of $\mathbb{C}$ makes Cauchy the exact convergence criterion for the capped sequence; the exact-shell side packages the same idea as ordered shell blocks and an oscillatory tail.
The exact-shell cutoff at level $N$ is the partial sum of shell amplitudes through $N$. Each shell amplitude is the contribution of the nonduplicating exact path classes at that complexity. The present identity is the elementary telescoping step that converts a difference of two such cutoffs into a contiguous block sum.
The local setting explicitly disclaims mesh refinement, continuum geometry, rates, and full-theory ledger claims: only cutoff removal is at stake.
proof idea
Term-mode one-liner. Apply the Mathlib identity that a sum over Finset.Ico a b equals the difference of the cumulative sums at $b$ and $a$, specialized to the exact shell amplitude sequence. The hypothesis $m \le n$ is lifted to $m+1 \le n+1$ by successor monotonicity, then the equality is symmetrized so the cutoff difference appears on the left.
why it matters
Feeds the headline ordered-tail equivalence: the unregulated exact-shell cutoff has a limit if and only if late shell blocks cancel in norm. That parent theorem is the analytic premise a substrate-derived oscillatory phase must prove before the complexity cutoff can be dropped from the phased quotient path sum.
In the Seven Gaps gravity stack this is the panel-locked telescoping step between exact cutoffs and ExactShellTailCancellation. Under the still-missing cross-API bridge that equates capped Zq sums with exact-shell sums, the same cancellation becomes the continuum-blocker criterion for the existing phased sequence. It is discriminating: the zero phase has an explicit epsilon-one failure witness, so the identity is not vacuous scaffolding.
No forcing-chain landmark (T5–T8, RCL, eight-tick) is invoked here; the lemma is pure finite-sum bookkeeping inside the gravity cutoff-removal API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.