oscillatoryTail_implies_shellAmplitudeVanishes
plain-language theorem explainer
Uniform late-block phase cancellation (an oscillatory tail) forces every individual exact-shell amplitude to tend to zero. Gravity and continuum-blocker arguments cite this as the weakest shell-local necessary condition implied by OscillatoryTail. The proof specializes the tail bound to one-shell blocks and rewrites via the one-shell identity.
Claim. Let $\mathrm{phase}$ assign a real phase to every exact path class at each complexity $n$. If $\mathrm{phase}$ has an oscillatory tail (uniform cancellation of contiguous late blocks), then the shell-local balance condition holds: for every $\varepsilon>0$ there exists $N$ such that for all $n\ge N$, $\|\mathrm{exactShellAmplitude}(\mathrm{phase},n)\|<\varepsilon$.
background
Module P2.4 isolates the missing phase obligation in the Zq continuum blocker. Carrier facts already give finite exact shells, positive class masses, and a fixed-cap pairing witness, but no substrate action that resolves phases inside every late shell. Limits here are complexity cutoffs, not mesh refinement.
ShellAmplitudeVanishes is the weakest shell-local necessary condition: individual late exact-shell amplitudes tend to zero in norm. It does not by itself control accumulation over long contiguous blocks. OscillatoryTail is the stronger uniform block-cancellation hypothesis on the same phase assignment.
A one-shell contiguous block equals the exact-shell amplitude (identity one_shell_block). The theorem records that any uniform oscillatory tail therefore forces the shell-local vanishing condition by restriction to those one-shell windows.
proof idea
Tactic proof, short. Fix $\varepsilon>0$ and unpack the oscillatory-tail witness to obtain a cutoff $N$ controlling all contiguous late blocks. Reuse that same $N$ for shell-amplitude vanishing. For each $n\ge N$, apply the tail bound on the one-shell window from $n$ to $n+1$ (using Nat.le_succ), then rewrite by one_shell_block so the block residual is exactly the exact-shell amplitude norm, which is therefore $<\varepsilon$.
why it matters
This is the necessary-balance step in the P2.4 shell-balance blocker: uniform tails require shell-local vanishing. It is packaged into p24_shell_balance_blocker_certificate, which certifies that finite-shell repairs and complexity-only phases cannot supply the missing premise.
Downstream, shellConstant_not_oscillatoryTail routes through the contrapositive path (constant-in-shell phases fail vanishing, hence fail the tail). The Gap2 bridge tickEquidistribution_implies_shellAmplitudeVanishes targets the same necessary condition from mass-balanced Fin-8 tick equidistribution, so this lemma marks the minimal shell-local obligation any richer eight-tick substrate must meet.
Framework context: eight-tick phase structure (T7) and the continuum/gravity blocker chain. The open content remains genuine asymptotic intra-shell balance from substrate structure; this theorem only forces the necessary local vanishing, not the full tail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.