eventuallyTickFiberMassBalanced_implies_exactShellTailCancellation
plain-language theorem explainer
Eventual equal mass across the eight tick fibers forces exact shell-tail cancellation for the tick-derived phase. Gap-2 residual and oscillatory-tail work cites this as the eventual-balance repair of all-shell balance. Proof takes the balance threshold N, zeros every late shell amplitude by the per-shell mass-balance lemma, then collapses contiguous block sums to zero in norm.
Claim. Let $\tau$ assign each exact path class at shell $n$ a tick in $\{0,\ldots,7\}$. If there exists $N$ such that for all shells $n\ge N$ the eight tick-fiber masses are equal, then the phase derived from $\tau$ has exact shell-tail cancellation: for every $\varepsilon>0$, every contiguous block sum of shell amplitudes beyond a large enough index has complex norm $<\varepsilon$.
background
The module hardens the R4 residual in the Gap-2 tick-phase story after a cross-family correction to the R2 receipt. The eight-tick octave (period $2^3$) labels fibers by $\mathrm{Fin},8$; a tick assignment $\tau$ sends each exact path class at shell $n$ to one fiber. Tick-fiber mass is the total class measure sitting in a given fiber at that shell.
All-shell mass balance is impossible: shell $0$ is a singleton class, so mass concentrates in one fiber for every $\tau$. The honest repair is eventual balance: equal fiber masses from some shell $N$ onward, with a possibly unbalanced finite head. Exact shell-tail cancellation only constrains late contiguous blocks of shell amplitudes, so that head is irrelevant to the oscillatory-tail lift.
The local setting is Wave C1 R4: identically zero late amplitudes make every late block sum vanish with no extra estimate, correcting the R2 claim that per-shell equidistribution alone cannot lift to contiguous-block cancellation.
proof idea
Unpack eventual balance to a threshold $N$ and a hypothesis that every shell $k\ge N$ has equal tick-fiber masses. For given $\varepsilon>0$, return that same $N$. On any contiguous index block with lower end $\ge N$, each shell amplitude of the tick-derived phase vanishes by the sibling lemma that mass balance at a shell forces the exact shell amplitude to zero. The finite sum of those amplitudes is therefore zero by the zero-sum lemma for vanishing summands; its complex norm is zero, hence $<\varepsilon$.
why it matters
This is clause (c) of the module's R4 hardening: eventual mass balance kills all late amplitudes, so the finite head does not obstruct OscillatoryTail. It sits beside the all-shell bridge (identically zero amplitudes imply tail cancellation) and the finite-head impossibility (no globally balanced $\tau$). Framework landmark: the eight-tick octave (T7) as the fiber index set.
No downstream consumers are wired yet (used_by empty). The R4 residual itself stays open: existence of a substrate phase escaping the dead classes with oscillatory tail. The sharper terminal candidate SignatureFin8OscillatoryTailBlocker is defined in-module but neither proved nor assumed. The declaration does not flip gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.