certificate_gives_polynomial_gain
plain-language theorem explainer
A projection-multiplicity certificate yields a fixed positive exponent by which the projected event count eventually outgrows any linear function of the visible size. Extremal combinatorialists packaging a lift-return argument would cite this as the formal payoff of the method. The proof is a one-line packaging of the certificate's stored gain and positivity fields.
Claim. Given a projection-multiplicity certificate $C$, there exists a real $\delta > 0$ such that the projected event count of $C$ eventually beats linear growth in the visible size by that fixed exponent: for all sufficiently large window indices $k$, writing $N(k)$ for visible size and $E(k)$ for event count, one has $0 < N(k)$ and $N(k)^{1+\delta} \le E(k)$.
background
The module isolates the abstract method suggested by the Erdős unit-distance miss: lift a classical extremal problem to a richer carrier, produce many hidden carrier events inside finite windows, then project those events back to the visible classical surface. Visible-dimensional counting can fail when a high-rank carrier has many distinct events that share one low-dimensional invariant.
A classical extremal problem supplies a visible universe, a size function, and a relation to maximize. Lift data choose a carrier and a projection from carrier events to visible events. Finite windows cut the carrier down to finite sets whose projections are the visible sets under study.
The predicate that the projected count beats linear growth by a fixed exponent $\delta$ asserts that, eventually along the window index, the visible size $N$ is positive and $N^{1+\delta}$ is at most the event count $E$. A projection-multiplicity certificate packages the problem, the lift, a window family, the size and count functions, a positive $\delta$, a size-matching axiom, and a stored polynomial-gain proof of that predicate.
proof idea
One-line term proof. The certificate already stores a real field delta, a positivity proof delta_pos, and a field polynomial_gain inhabiting the beats-linear predicate on the certificate's own visible-size and event-count functions. The term is the existential triple of those three fields; no further rewriting or external lemmas are applied.
why it matters
This is the formal output clause of the projection-multiplicity method: once a certificate is assembled, the lifted carrier is guaranteed to produce a visible polynomial gain. The module's point is not to formalize any particular OpenAI/Sawin-style unit-distance argument, but to name the failure mode so future classical problems are checked for the same pattern (fiber multiplicity controlling the event count rather than visible dimension alone).
No downstream consumers are wired yet (used_by is empty). The declaration sits as the theorem-shaped interface that any concrete certificate instance must discharge. Within Recognition Science it is pure mathematical scaffolding for extremal counting, not a step on the T0–T8 forcing chain, the RCL, or the mass ladder; its value is methodological hygiene for later combinatorial lifts that may feed physics-facing counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.