oscillatoryTail_congr_eventually
plain-language theorem explainer
Eventual agreement of two exact-shell phase maps preserves the uniform oscillatory-tail condition in both directions. Seven-Gaps gravity workers cite this when moving the continuum-blocker tail property across finite phase repairs. The proof unpacks the agreement witness and applies the one-sided transfer lemma twice, once each way via equality symmetry.
Claim. Let $\mathrm{phase}$ and $\psi$ assign real phases to exact path classes of each complexity $n$. If there exists $N$ such that $\mathrm{phase}_n(c)=\psi_n(c)$ for all $n\ge N$ and all classes $c$, then $\mathrm{phase}$ satisfies the uniform oscillatory-tail condition if and only if $\psi$ does.
background
Module P2.4 isolates the missing phase-balance input in the $Z_q$ continuum blocker. The target property is the uniform oscillatory tail: late contiguous blocks of exact-shell amplitudes must vanish uniformly as the complexity cutoff tends to infinity. Limits here are complexity cutoffs only, not mesh refinement or geometric continuum claims.
Exact path classes are the combinatorial exact complexes of fixed complexity $n$ (disjoint union over shell signatures of labeled classes modulo global equivalence); no bounded-cap type appears. An eventual-agreement hypothesis says two phase maps on those classes coincide from some shell $N$ onward.
The one-sided sibling already transfers the tail property when the second phase eventually matches the first. This theorem packages both directions. Downstream, the finite-cap no-go needs exactly that congruence: zero phase fails the tail, so any phase that is eventually zero also fails.
proof idea
Unpack eventual agreement to a cutoff $N_0$ and a pointwise equality on all later shells. Split the biconditional. Forward: feed $\langle N_0, h_{N_0}\rangle$ into the one-sided lemma oscillatoryTail_of_eventuallyAgrees. Reverse: reuse the same cutoff with the symmetrized equality $h_{N_0}(\ldots).symm$, again via that one-sided lemma. Pure term-mode, no new analysis.
why it matters
Parent use is eventuallyZeroPhase_not_oscillatoryTail, the finite-cap no-go: no phase modification supported on only finitely many exact shells can satisfy the uniform oscillatory-tail condition. That argument reduces a finitely supported repair to the zero phase via this congruence, then quotes that zero fails the tail.
In the Seven Gaps ledger this seals that finite-cap pairing certificates and mere relabeling cannot discharge P2.4. The module already shows shell-constant phases fail (shell amplitude norm equals the diverging positive shell mass). What remains is genuine asymptotic intra-shell balance, at least shell-amplitude vanishing and in fact the stronger contiguous-block control. Framework context is the gravity side of the forcing chain (eight-tick structure in the ambient stack), not a new T5–T8 step; no full-theory flag moves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.