ClassicalExtremalProblem
plain-language theorem explainer
A classical extremal problem is packaged as visible objects, a binary relation on them, and two real-valued readouts: size of a visible set and count of related pairs. Anyone formalizing lift-and-project attacks on extremal combinatorics (unit distance, Szemerédi–Trotter style) cites this carrier. It is a pure data structure: four fields, no proof obligations.
Claim. A classical extremal problem is a 4-tuple $(V, R, s, e)$ where $V$ is a type of visible objects, $R \subseteq V \times V$ is a relation whose instances are counted, $s$ assigns a real size to every finite subset of $V$, and $e$ assigns a real event count to every finite set of ordered pairs from $V$.
background
The module isolates the abstract method suggested by the Erdős unit-distance miss: attack a classical extremal problem by lifting it to a richer carrier, generating many hidden carrier events, then projecting those events back onto the visible surface. Visible-dimensional counting can lose when a high-rank carrier has many distinct events that collapse to one low-dimensional invariant.
This structure is the visible side of that story. It names only what the classical problem already exposes: the ground set of visible objects, the relation whose incidences matter, a size functional on finite visible sets, and an event-count functional on finite pair sets. No carrier, projection, or energy appears here; those live in the companion lift data.
Upstream imports are ambient Mathlib and scattered foundation names; none constrain the four fields. The definition is deliberately thin so later certificates can quantify over arbitrary classical surfaces.
proof idea
No proof. The declaration is a structure (data record) with four fields: a universe-polymorphic type of visible objects, a binary relation on that type, a size map from finite visible sets to reals, and an event-count map from finite pair sets to reals. Instantiation is by supplying those four components; there are no axioms or sorry obligations attached to the structure itself.
why it matters
This is the base type for the whole projection-multiplicity stack. Lift data is parameterized by a classical extremal problem and adds a richer carrier, a projection map, a carrier relation, and an energy. Finite windows sit over a fixed lift and record carrier sets, projected visible sets, and certified events. The projection-multiplicity certificate then packages a problem, a lift, a family of windows, and polynomial-gain bounds on visible size and event count.
In Recognition Science terms the structure is methodological scaffolding, not a forcing-chain step (T0–T8). It records how a classical miss can arise when low-dimensional invariants hide high multiplicity, so future RS-adjacent counting arguments can be checked for the same failure mode. Downstream, the certificate shape is exactly the lift-return proof pattern the module wants named and reusable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.