ProjectionMultiplicityCertificate
plain-language theorem explainer
A projection-multiplicity certificate packages a lift-return attack on a classical extremal problem: richer carrier, finite windows, matching size and event readouts, and a fixed polynomial gain of projected events over linear growth. Combinatorialists checking unit-distance-style bounds cite it when visible counting may be beaten by high-rank multiplicity. As a structure it only assembles those fields; the gain is the BeatsLinearBy witness.
Claim. A projection-multiplicity certificate consists of a classical extremal problem $P$ (visible type, binary relation, size and event-count functionals), lift data $L$ to a richer carrier with projection, a family of finite carrier windows indexed by $k\in\mathbb{N}$, sequences $N,E:\mathbb{N}\to\mathbb{R}$ for visible size and event count, and a fixed $\delta>0$ such that eventually $N(k)$ and $E(k)$ match $P$'s readouts on the windows, and eventually $0<N(k)$ with $N(k)^{1+\delta}\le E(k)$.
background
The module records the abstract method exposed by the Erdős unit-distance miss: lift a classical extremal problem to a richer carrier, produce many hidden carrier events, and project them back to the visible surface. Visible-dimensional counting can fail when many distinct high-rank events share one low-dimensional invariant.
A classical extremal problem supplies a visible type, a relation whose instances are counted, and two readouts (size of a finite visible set; event count on pairs). Lift data adds a carrier, a projection map, a carrier relation, and an energy. A finite window packages a finite carrier set, its projected visible set, lifted events, and visible events, with soundness that projection covers the carrier points and events project validly.
BeatsLinearBy asserts that eventually the event sequence dominates $N^{1+\delta}$ for fixed $\delta>0$.
proof idea
Structure definition, not a proved theorem. It bundles the four ingredients of the lift-return method named in the doc-comment: the classical problem, the lift to a richer carrier, a window family with eventually matching size and event sequences, a positive exponent $\delta$, and the BeatsLinearBy field witnessing that projected events grow at least like $N^{1+\delta}$. No tactics or upstream lemmas are applied; the fields are the certificate.
why it matters
This is the formal output shape of the projection-multiplicity method. Downstream, certificate_gives_polynomial_gain unpacks any certificate into an existential: there exists $\delta>0$ such that the visible size and event sequences beat linear growth by that exponent ("the lifted carrier gives a visible polynomial gain").
The module does not formalize the OpenAI/Sawin unit-distance proof. It names the failure mode so future classical problems are checked for the same pattern. In the Recognition Science mirror it sits in the mathematics layer as methodological scaffolding for extremal counting arguments; it does not itself invoke the forcing chain T0–T8, the J-cost, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.