LiftData
plain-language theorem explainer
A lift packages a classical extremal problem on a richer carrier type together with a projection back to the visible surface, a carrier-level relation, and a real-valued energy. Anyone formalizing projection-multiplicity arguments (Erdős-type unit-distance lifts, hidden-event counting) cites this bundle. It is a pure structure definition with no proof obligations.
Claim. Given a classical extremal problem $P$ (visible type, pairwise relation, size and event-count readouts), a lift consists of a carrier type $C$, a projection $\pi: C \to P.{\rm Visible}$, a binary relation $R$ on $C$, and an energy functional $E: C \to \mathbb{R}$.
background
The module isolates the abstract method behind the Erdős unit-distance miss: attack a classical extremal problem by lifting it to a richer carrier, generating many hidden carrier events, and projecting those events back onto the low-dimensional visible surface. Visible-dimensional counting can then be beaten when many distinct carrier events share one projected invariant.
A classical extremal problem supplies the visible type, the relation whose instances are counted, and two numerical readouts (visible size and event count). The lift is the complementary data: the carrier, the projection map, the carrier relation, and an energy on the carrier. Related foundation material treats projection of deterministic states to observations (many states, one observation) as the source of apparent randomness; here the same pattern is named for extremal combinatorics rather than measurement.
proof idea
No proof. The declaration is a structure bundling four fields over a fixed classical extremal problem: the carrier type, the projection into the visible type, the carrier-level relation, and a real energy. Downstream structures (finite windows, certificates) inhabit this interface.
why it matters
Lift data is the first non-classical ingredient in the projection-multiplicity method. Finite windows are typed over a lift: they carry a finite carrier set, its projected visible set, and certified lifted versus visible events. The projection-multiplicity certificate then packages a problem, a lift, a family of windows, and size/event-count sequences, and is the abstract shape of the lift-return argument (richer carrier, finite windows, projection of carrier events to valid visible events, fixed polynomial gain).
The module deliberately does not formalize any particular OpenAI/Sawin-style proof. It names the failure mode so future classical problems can be checked for the same pattern: high-rank carriers with many events collapsing under projection. In the broader Recognition setting this echoes deterministic projection (many microstates, one observation) and high-rank algebraic carriers (e.g. Clifford/8-tick structure), without claiming a direct identification here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.