ExactShellTailCancellation
plain-language theorem explainer
Exact shell tail cancellation is the ordered Cauchy criterion on late contiguous blocks of exact-shell amplitudes for a phase on complexity shells. Anyone proving that a substrate-derived phase removes the complexity cutoff from the phased quotient path sum cites it. The declaration is a Prop definition: for every ε>0 some N makes every block sum over shells (m,n] with N≤m≤n smaller than ε in norm.
Claim. A real phase on exact complexity shells (combinatorially distinct exact complexes of complexity exactly $n$) has exact shell tail cancellation when, for every $\varepsilon>0$, there exists $N$ such that for all $m,n$ with $N\le m\le n$, the norm of the sum of exact-shell amplitudes over shells $k\in(m,n]$ is strictly less than $\varepsilon$.
background
Module P2-a isolates analytic obligations for removing the 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 existence of a limit equivalent to the Cauchy property. The cap-free side uses the exact complexity shell: for each $n$, the type of combinatorially distinct exact complexes of complexity exactly $n$ (disjoint union over shell signatures of the quotient of the exact labeled class by global equivalence), with no bounded-complex cap in the definition.
Panel-locked $Z_{\mathrm{cap}}$ sums exact quotient shells in range B. Oscillatory tail uniformly quantifies every sufficiently late contiguous shell block. Exact telescoping yields Cauchy of $Z_{\mathrm{cap}}$ iff oscillatory tail. The present predicate is the ordered form of that cancellation: late blocks of exact-shell amplitudes must be small. The interval $(m,n]$ is coded as the half-open integer interval from $m+1$ to $n+1$.
Limits here only remove a complexity cutoff. They are not mesh refinement and carry no continuum-geometry, observation, rate, measure, or full-ledger claim.
proof idea
Definitional Prop, not a proved theorem. The body is the standard $\varepsilon$-$N$ tail statement: universal quantification over positive $\varepsilon$, existential $N$, then universal $m\le n$ past $N$, requiring the complex (or real) norm of the finite sum of exactShellAmplitude phase k over $k\in\mathrm{Ico}(m+1,n+1)$ to be $<\varepsilon$. No tactics or upstream lemmas fire at the definition site; equivalence to the unordered oscillatory-tail predicate is proved downstream via the banked $Z_{\mathrm{cap}}$ Cauchy criterion, completeness, and the ordered-tail IFF.
why it matters
This is the panel-facing cancellation obligation a substrate-derived phase must meet to drop the complexity cutoff. Downstream, oscillatoryTail_iff_exactShellTailCancellation identifies it with oscillatory tail; the composition package then lifts oscillatory tail (hence this predicate) to a phased $Z_q$ complexity limit on the canonical transported cap-phase family, under cap-shell compatibility. The full-theory ledger certifies the Pillar 2 cutoff-limit blocker as the conjunction of that Cauchy/oscillatory equivalence, the explicit failure of zero phase, and the compatibility bridge.
Tick-phase substrate work feeds the same node: eventual tick-fiber mass balance implies this cancellation, and equidistribution bridges force shell-amplitude vanishing for tick-derived phases. In the seven-gaps gravity program this is discriminating analytic content, not scaffolding: zero phase has an explicit $\varepsilon=1$ failure witness. It does not itself invoke T5–T8 or the RCL; it is the cutoff-removal half of gap-2 continuum-and-measure bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.