EventuallyAgrees
plain-language theorem explainer
Two exact-shell phase assignments eventually agree when they coincide on every class from some complexity cutoff onward. Gravity and continuum-blocker arguments cite this as the congruence relation that transports the oscillatory-tail condition and defines finite-support phase repairs. The body is a plain existential Prop over a tail of shells.
Claim. Two families of exact-shell phases $\mathrm{phase},\psi$ (each assigning a real to every exact path class of complexity $n$) eventually agree if there exists $N\in\mathbb{N}$ such that for all $n\ge N$ and every exact path class $c$ of complexity $n$, $\mathrm{phase}(n,c)=\psi(n,c)$.
background
The module isolates the missing phase-balance input for the Seven Gaps P2.4 continuum blocker. Carrier facts already give finite exact shells, positive class masses, and large shell mass, but no substrate action that fixes phases inside every late shell. Limits here are complexity cutoffs, not mesh refinement.
An exact path class at complexity $n$ is a combinatorially distinct exact complex of that complexity: the disjoint union, over shell signatures, of the quotient of the exact labeled class by global equivalence. No bounded-cap type appears. Phase data are arbitrary real assignments on those classes, shell by shell.
Eventual agreement is the natural tail congruence on such assignments. It is the abstract shape used both to move the uniform oscillatory-tail condition between phases and to package finite-cap repairs as phases that match the zero phase from some shell onward.
proof idea
Definitional: the Prop is the existential statement that some cutoff $N$ forces pointwise equality of the two phase maps on every exact path class in every shell $n\ge N$. No lemmas are applied; the body is the predicate itself.
why it matters
This predicate is the congruence that lets the module separate genuine asymptotic intra-shell balance from finite or shell-constant phase tricks. Downstream, EventuallyZeroPhase is exactly eventual agreement with the zero phase, and the finite-cap no-go theorem uses that shape to show finite-support repairs cannot meet the uniform oscillatory-tail condition. The one-sided and biconditional transport theorems move OscillatoryTail along eventual agreement, so the tail property is well-defined up to finite shell edits.
In the Recognition gravity stack this sits under the exact-shell UV picture tied to the eight-tick forcing (period $2^3$ at $D=3$). It does not supply the missing balance; it only names the relation under which balance, or its failure, is stable. The open P2.4 demand remains genuine asymptotic cancellation inside late shells, at least shell-amplitude vanishing and ideally full oscillatory-tail control.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.