oscillatoryTail_of_eventuallyAgrees
plain-language theorem explainer
If two exact-shell phase assignments agree from some complexity onward and one satisfies the uniform oscillatory-tail bound on contiguous shell-amplitude blocks, so does the other. Gravity/SevenGaps work cites this to transport the P2.4 tail obligation across eventual phase relabeling. The proof takes the max of the agreement and tail cutoffs, then rewrites the block sum by shell-amplitude congruence.
Claim. Let $\mathrm{phase}$ and $\psi$ assign real phases to exact path classes on each complexity shell. If there exists $N_0$ such that for all $n\ge N_0$ and all classes $c$ one has $\mathrm{phase}(n,c)=\psi(n,c)$, and if $\mathrm{phase}$ has the oscillatory-tail property (for every $\varepsilon>0$ some $N$ makes every contiguous block sum of exact-shell amplitudes from $m\ge N$ smaller than $\varepsilon$ in modulus), then $\psi$ has the oscillatory-tail property as well.
background
Module SevenGaps P2.4 isolates the missing phase-balance input for the continuum blocker: finite exact shells, positive class masses, and fixed-cap pairing do not force the uniform tail condition OscillatoryTail on unregulated shell amplitudes. Limits are in the complexity cutoff only, not mesh refinement.
An exact path class at complexity $n$ is a combinatorially distinct exact complex of that complexity (disjoint union over shell signatures of the quotient by global equivalence). The exact-shell amplitude of a phase assignment is the complex sum over those classes of class mass times $e^{i\cdot\mathrm{phase}}$.
Eventual agreement means the two phase maps coincide on every class from some shell $N_0$ onward. Oscillatory tail is the stronger uniform contiguous-block control that implies the weaker shell-local vanishing condition; the module shows finite-cap pairing and shell-constant phases cannot supply it.
proof idea
Unpack eventual agreement to a cutoff $N_0$. Fix $\varepsilon>0$ and unpack the oscillatory-tail hypothesis on phase to a cutoff $N$. Take $M=\max(N,N_0)$ as the witness for $\psi$.
For $m\ge M$ and $n>m$, the block sums of exact-shell amplitudes of $\psi$ and phase over $\mathrm{Ico},m,n$ agree: each shell index $k\ge m\ge N_0$ has identical phases on all classes, so exactShellAmplitude_congr equates the summands, and Finset.sum_congr lifts that to the block. Rewrite and apply the tail bound already known for phase on the same block (using $m\ge N$).
why it matters
One direction of tail transport under eventual phase agreement. Downstream, oscillatoryTail_congr_eventually packages both directions into an iff: eventual agreement preserves the uniform tail condition exactly.
In the Seven Gaps P2.4 program this keeps the phase obligation stable under late-shell relabeling. The module's point is that neither finite changes, shell-constant phases, nor fixed-cap pairing discharge OscillatoryTail; only genuine asymptotic intra-shell balance does. Transport lemmas ensure that obligation is about the asymptotic phase content, not a particular representative.
No full-theory flag moves; the result is local bookkeeping inside the gravity continuum-blocker stack, not a claim about geometric continuum limits or the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.