exactShellTailCancellation_of_identically_zero_amplitudes
plain-language theorem explainer
Identically zero exact-shell amplitudes imply full exact shell-tail cancellation for any phase on exact path classes. Gravity residual auditors cite it as the honest lift from pointwise vanishing to contiguous-block cancellation (stronger than mere asymptotic smallness). The proof picks threshold zero, rewrites every block sum via the zero-amplitude sum lemma, and applies norm-zero.
Claim. Let a phase assign a real to every exact path class at each shell index $n\in\mathbb{N}$. If the exact shell amplitude of that phase is $0$ at every $n$, then the phase satisfies exact shell-tail cancellation: for every $\varepsilon>0$ there exists a threshold $N$ such that every contiguous block sum of shell amplitudes past $N$ has norm strictly less than $\varepsilon$.
background
This module hardens the R4 residual in the Gap-2 tick-phase story after a cross-family correction to the R2 receipt. The local objects are a phase on exact path classes, the exact shell amplitude built from that phase, and ExactShellTailCancellation: an $\varepsilon$-$N$ statement that contiguous block sums of those amplitudes become arbitrarily small in the tail (and thereby feed OscillatoryTail).
The R2 assessment correctly said that asymptotic shell-amplitude vanishing (late shells merely small) does not by itself give contiguous-block cancellation. The module docstring records the divergence: that objection fails for identically zero amplitudes. Under all-shell tick-fiber mass balance every shell amplitude is definitionally zero, so every contiguous block sum is zero with no extra estimate.
Upstream ingredients used here are elementary: the sibling sum lemma that a Finset sum of zero amplitudes is zero, and the GoldenInt fact that the norm of zero is zero. Eight-tick phase and shell-scale defs sit in the broader substrate but are not invoked in this particular lift.
proof idea
Term-mode proof of the $\varepsilon$-$N$ property. Fix $\varepsilon>0$. Choose threshold $N=0$ (identically zero amplitudes cancel from the first shell). For any $m,n$ in the tail range, the amplitudes on the half-open index interval $\mathrm{Ico}(m+1,n+1)$ are zero by the global hypothesis. Rewrite the block sum with the sibling lemma sum_amp_eq_zero_of_amps_zero, then norm_zero, and discharge the $\varepsilon$ inequality. No estimate or equidistribution argument is required.
why it matters
Closes bridge (a) in the module plan: identically zero amplitudes (as produced by all-shell TickFiberMassBalanced) lift definitionally to ExactShellTailCancellation and thence toward OscillatoryTail. It is the honest extra hypothesis beyond the asymptotic vanishing Prop named in the doc-comment, and it corrects the R2 claim that per-shell vanishing never yields block cancellation.
No downstream consumers are wired yet (used_by is empty). The sibling tickFiberMassBalanced_implies_exactShellTailCancellation is the natural parent path once mass balance is assumed. What stays open is the R4 residual itself: existence of a substrate phase escaping the dead classes with OscillatoryTail, and the sharper defined-but-unproved SignatureFin8OscillatoryTailBlocker. Does not flip gap2_continuum_and_measure. Framework contact is the eight-tick octave (T7) substrate for the phase, not a new forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.