eventuallyZeroPhase_not_oscillatoryTail
plain-language theorem explainer
Finite-cap phase repairs cannot produce a uniform oscillatory tail. Anyone closing the P2.4 shell-balance gap cites this: a phase that agrees with zero outside finitely many exact shells fails OscillatoryTail. The argument transfers the tail property along eventual agreement, then applies the zero-phase obstruction.
Claim. Let $\mathrm{phase}$ assign a real number to each exact path class at every complexity $n$. If $\mathrm{phase}$ eventually agrees with the zero phase (i.e., differs from zero on only finitely many exact shells), then $\mathrm{phase}$ does not satisfy the uniform oscillatory-tail condition on late contiguous blocks.
background
Module P2.4 isolates the phase obligation inside OscillatoryTail without assuming cancellation. Carrier facts already give finite exact shells, positive class masses, large shell mass, and a fixed-cap pairing witness; they do not supply a substrate action that balances phases inside every late shell.
EventuallyZeroPhase is the abstract shape of any finite-cap repair: the phase eventually agrees with the zero phase, so only finitely many shells are touched. OscillatoryTail is the uniform late-block control needed for the continuum blocker; a weaker shell-local necessary condition is that every individual late shell amplitude tends to zero.
The local setting is complexity cutoffs only (not mesh refinement, not a geometric continuum claim). The theorem says finite support cannot manufacture the required asymptotic intra-shell balance.
proof idea
Term-mode reductio. Assume the phase has an oscillatory tail. Eventual agreement with the zero phase, via the congruence lemma for oscillatory tails under eventual agreement, pushes the tail property onto the zero phase. The known zero-phase obstruction then yields a contradiction. No shell arithmetic is recomputed here; the work is pure transfer plus the zero baseline.
why it matters
This is the finite-cap no-go half of the P2.4 shell-balance blocker. It feeds the certified package theorem that packages three facts: oscillatory tails force shell-amplitude vanishing; eventually-zero phases cannot be tails; complexity-only (shell-constant) phases cannot be tails either. Downstream, the fixed-cap support lemma reduces to this by exhibiting eventual zero beyond the cap, and the Gap-2 composition package re-exports it as a decoy blocker.
In the Seven Gaps gravity line, the point is sharp: a finite-cap pairing certificate cannot be promoted to the uniform tail condition merely by zero-extension. The remaining missing input is genuine asymptotic intra-shell phase balance from richer substrate structure. No full-theory flag moves; the result only certifies what finite repairs cannot do.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.