BeatsLinearBy
plain-language theorem explainer
Defines the asymptotic gain predicate: the projected event count E eventually dominates every linear multiple of the visible size N, specifically N^{1+δ} for a fixed positive exponent δ. Anyone packaging a lift-return argument for a classical extremal problem cites this as the target inequality. The body is a pure Filter.atTop eventuality, not a derived theorem.
Claim. For sequences $N,E:\mathbb{N}\to\mathbb{R}$ and a real $\delta$, the predicate holds when eventually (as $k\to\infty$) one has $N(k)>0$ and $N(k)^{1+\delta}\le E(k)$. In words: the projected event count beats linear growth in the visible size by the fixed exponent $\delta$.
background
The module isolates the abstract method behind the Erdős unit-distance miss: lift a classical extremal problem to a richer carrier, generate many hidden carrier events, then project them back onto the visible classical surface. Visible-dimensional counting can fail when many distinct high-rank events collapse to the same low-dimensional invariant.
BeatsLinearBy is the quantitative target of that method. $N$ is the visible size sequence (e.g. number of classical points or edges in a window); $E$ is the projected event count after the lift-return. The inequality $E\ge N^{1+\delta}$ with fixed $\delta>0$ is the polynomial gain that classical linear bounds miss.
Upstream counting and projection primitives (lattice edge sets, multiset event counts, deterministic observation maps) supply the concrete $N$ and $E$ that later certificates plug in; this definition only names the asymptotic comparison.
proof idea
Definition, not a proof. The body is the Filter predicate ∀ᶠ k in atTop, 0 < N k ∧ (N k)^(1+δ) ≤ E k, i.e. the conjunction of positivity of the visible size and the power-law lower bound on the event count, holding for all sufficiently large window indices. No lemmas are applied.
why it matters
This predicate is field 4 of a projection-multiplicity certificate and the conclusion of certificate_gives_polynomial_gain, which packages any such certificate into an existential statement: there exists δ>0 such that the visible size and event-count sequences beat linear growth by δ. The module's point is diagnostic: future classical problems should be checked for the same failure mode (high-rank carrier events projecting onto a low-dimensional invariant). It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure combinatorial scaffolding that later RS counting arguments can inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.