EventuallyZeroPhase
plain-language theorem explainer
A phase on exact complexity shells is eventually zero-phase when it coincides with the identically zero assignment from some shell onward. That is the abstract shape of any finite-cap phase repair: only finitely many shells may carry nonzero phases. Gravity and continuum-blocker arguments cite it to state the finite-cap no-go. The body is a one-line alias of eventual agreement with the zero phase.
Claim. A phase assignment $\varphi$, sending each exact path class of complexity $n$ to a real number, is eventually zero-phase if there exists $N\in\mathbb{N}$ such that for every $n\ge N$ and every exact path class $c$ of complexity $n$, one has $\varphi_n(c)=0$.
background
Module P2.4 isolates the phase obligation in the oscillatory-tail condition for the exact-shell continuum blocker, without assuming cancellation. Carrier facts give finite exact shells, positive class masses, and large shell mass, but no substrate action that resolves phases inside every late shell.
An exact path class of complexity $n$ is a combinatorially distinct exact complex at that shell: a disjoint union over shell signatures of the quotient of the exact labeled class by global equivalence. No bounded-complex cap type appears. The zero phase is the constant assignment $S\equiv 0$ on every class.
Eventual agreement of two phases means they coincide on all classes from some shell $N$ onward. Eventually zero-phase is that relation specialized to the zero phase, so the phase differs from zero on only finitely many shells.
proof idea
Pure definitional abbreviation: the predicate is defined as eventual agreement of the given phase with the zero phase. No tactics or lemmas are invoked; the mathematical content is entirely that of the eventual-agreement relation applied to the constant-zero assignment.
why it matters
This is the exact abstract shape of any finite-cap phase repair in the Seven Gaps ledger. Downstream, the finite-cap no-go theorem states that no eventually zero-phase assignment can satisfy the uniform oscillatory-tail condition: if the phase is zero from some shell on, the tail fails. That no-go is packaged into the P2.4 shell-balance blocker certificate and into the FullTheoryLedger pillar-2 certification, which records that the remaining oscillatory-tail obligation is sharp: tails force per-shell amplitude vanishing, so neither finite-cap (eventually zero) repairs nor shell-constant phases work. Any closing phase must rebalance every late shell. The module stresses that limits are in the complexity cutoff, not mesh refinement, and no full-theory flag is changed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.