FiniteWindow
plain-language theorem explainer
A finite window packages a finite carrier subset, its projected visible set, and the certified lifted and visible event pairs inside that window, with coverage and soundness axioms. Anyone assembling a projection-multiplicity certificate cites it as the window type. Pure structure definition: fields and three Prop constraints, no proof body.
Claim. Fix a classical extremal problem $P$ (visible type, binary relation, size and event-count readouts) and a lift $L$ (richer carrier, projection $L.\mathrm{project}$, carrier relation, energy). A finite window consists of finite sets $C\subset L.\mathrm{Carrier}$, $V\subset P.\mathrm{Visible}$, lifted events $E_L\subset C\times C$, and visible events $E_V\subset V\times V$ such that: every $x\in C$ has $L.\mathrm{project}(x)\in V$; every $(x,y)\in E_L$ satisfies the carrier relation and the projected pair satisfies $P$'s relation; and every lifted event projects into $E_V$.
background
The module isolates the abstract method behind the Erdős unit-distance miss: attack a classical extremal problem by lifting to a richer carrier, producing many hidden carrier events, then projecting 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 binary relation whose instances are counted, and two real-valued readouts (visible size and event count). A lift equips that problem with a carrier type, a projection map to the visible type, a carrier relation, and an energy functional on carrier points.
Upstream projection language (deterministic state to observed state; multiple states mapping to one observation) is the same pattern: multiplicity under projection is the resource the method exploits. Finite-window data is the concrete finite sample on which that multiplicity is certified.
proof idea
No proof: this is a structure definition. It bundles four Finset fields (carrier set, visible set, lifted events, visible events) and three axioms: projection covers the carrier set into the visible set; every lifted event is sound for both the carrier relation and the projected visible relation; every lifted event projects into the visible event Finset. Downstream certificates quantify over families of such windows.
why it matters
ProjectionMultiplicityCertificate is built on this type: it asks for a classical problem, a lift, a sequence of finite windows, and size/event-count sequences, then asserts a fixed polynomial gain of projected events over linear growth in visible size. The module's point is not to formalize any particular OpenAI/Sawin argument, but to name the failure mode so future classical problems can be checked for the same lift-return pattern.
In Recognition Science terms this is methodological scaffolding for counting under projection (related in spirit to deterministic project maps and event counts elsewhere in the monolith), not a forcing-chain step (T0–T8) or a physical constant claim. It closes the data shape needed before one can state a polynomial-gain certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.