exactComplexityCutoff
plain-language theorem explainer
Exact-shell quotient path sum through complexity B: the sum of shell amplitudes over shells 0 through B for a phase on exact path classes. Gravity continuum-blocker and cap-shell bridge results cite it as the nonduplicating finite cutoff (each exact complex sits in one shell). Definitional Finset sum; equals the panel-locked Zcap at B+1 by a one-line shift.
Claim. Given a real phase on exact path classes at each shell complexity $n$ and a bound $B\in\mathbb{N}$, the exact complexity cutoff is $\sum_{n=0}^{B} A_n(\mathrm{phase})\in\mathbb{C}$, where $A_n$ is the exact-shell amplitude at shell $n$. Each exact complex occurs in one shell, so the sum does not double-count across caps.
background
Module Seven Gaps P2-a isolates analytic obligations for removing a complexity cutoff from the phased quotient path sum. Two APIs sit side by side. The fixed-cap side builds a sequence of finite quotient sums from a family of phase models; completeness of $\mathbb{C}$ makes convergence equivalent to the Cauchy criterion. The cap-free side uses exact path classes graded by shell complexity (largest of vertex, edge, and tetrahedron counts on a bounded complex).
The panel-locked partial sum $Z_{\mathrm{cap}}(\mathrm{phase},B)$ adds exact quotient shells over range B. An oscillatory-tail predicate quantifies late contiguous shell blocks uniformly; exact telescoping yields Cauchy of $Z_{\mathrm{cap}}$ iff that tail cancels. The present cutoff is the ordered sibling that includes shell $B$: sum of exact-shell amplitudes through $B$. Limits here only remove a complexity cutoff; they are not mesh refinement and claim nothing about continuum geometry or a derived measure.
proof idea
Pure definition: unfold to the Finset sum of exact-shell amplitudes over Finset.range (B + 1), i.e. shells $0,\ldots,B$. No lemmas. Downstream one-liners identify it with $Z_{\mathrm{cap}}$ at $B+1$ by rfl, and differences of two cutoffs with the intervening Ico shell block via Finset sum telescoping.
why it matters
Anchor of the nonduplicating exact-shell cutoff API inside the gravity seven-gaps stack. CapShellBridge uses it for the headline finite-sum reindexing: the phased capped quotient transported from any exact-shell phase equals this cutoff through shell $B$, and the disjoint-union carrier over shells up to $B$ sums to the same value. Gap2CutoffCompositionPackage records the definitional shift to $Z_{\mathrm{cap}}$ at $B+1$ and routes oscillatory-tail cancellation through completeness of $\mathbb{C}$ into ordered exact-shell tail cancellation.
CapShellCompatibility is the missing cross-API bridge: equality of the capped phased $Z_q$ sequence with this cutoff at every $B$. Under that bridge, convergence of the existing phased $Z_q$ sequence is equivalent to exact-shell tail cancellation. The zero phase supplies an explicit epsilon-one failure witness, so the criterion is discriminating. Framework role is local to complexity-cutoff removal in the path-sum ledger, not to T0–T8 forcing or continuum spacetime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.