Zcap_telescoping
plain-language theorem explainer
Exact-shell cutoffs telescope: the difference between two complexity cutoffs equals the sum of the intervening contiguous shell amplitudes. Anyone proving the Cauchy criterion for the phased quotient path sum cites this identity. The proof is a one-line appeal to the standard Finset Ico-sum telescoping lemma.
Claim. For any phase assignment on exact path classes and natural numbers $m \le n$, the difference of exact-shell cutoffs satisfies $Z_{\mathrm{cap}}(\mathrm{phase}, n) - Z_{\mathrm{cap}}(\mathrm{phase}, m) = \sum_{k=m}^{n-1} A_{\mathrm{shell}}(\mathrm{phase}, k)$, where $A_{\mathrm{shell}}$ is the exact-shell amplitude at complexity $k$.
background
This module (Seven Gaps, P2-a) isolates the analytic obligations for removing a complexity cutoff from the phased quotient path sum. Limits here are cutoff removal, not mesh refinement, and carry no continuum-geometry claim.
The panel-locked cutoff $Z_{\mathrm{cap}}(\mathrm{phase}, B)$ sums exact quotient shell amplitudes over shells with indices in $\mathrm{range}, B$ (complexities strictly below $B$). Each shell amplitude is the phased sum over the exact path class at that complexity. Contiguous blocks of shells are the natural increments of this partial-sum sequence.
The local goal is a pure complexity-cutoff Cauchy criterion: the cutoff sequence converges in $\mathbb{C}$ if and only if every sufficiently late contiguous shell block is uniformly small (the oscillatory-tail condition). Exact telescoping is the algebraic link between consecutive cutoffs and those blocks.
proof idea
One-line term proof. By definition $Z_{\mathrm{cap}}(\mathrm{phase}, B)$ is the Finset sum of shell amplitudes over $\mathrm{range}, B$. Mathlib's Finset.sum_Ico_eq_sub states that the sum over the half-open interval $[m,n)$ equals the difference of the two range-sums when $m \le n$. Applying that identity to exactShellAmplitude phase and taking the symmetric form yields the claimed telescoping equality.
why it matters
This is the C1 exact-telescoping step in the phased-quotient cutoff blocker. It feeds the C1 headline theorem cauchySeq_Zcap_iff_oscillatoryTail, which equates Cauchy-ness of the exact-shell cutoff sequence with the oscillatory-tail condition (uniform smallness of late contiguous shell blocks). That equivalence is the cancellation statement any substrate-derived phase must supply.
It is also used by zeroPhase_compatibility_and_limit_impossible, the discriminant showing that the zero phase cannot both match the exact-shell decomposition and admit a complexity-cutoff limit. Together these close the analytic half of P2-a: cutoff removal reduces to tail cancellation, with an explicit failure witness for the trivial phase. The remaining open bridge is CapShellCompatibility between capped triangulation classes and exact path classes; under that bridge, convergence of the existing phased $Z_q$ sequence is equivalent to this exact-shell criterion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.