Mathematics Projection Multiplicity Method

The projection multiplicity method

The projection multiplicity method is a way of attacking a classical extremal problem: a setup with visible objects, a relation between them, and two numerical readouts, the visible size and the event count. The method begins with a suspicion. A problem may look like its answer is controlled by the dimension of the visible objects, but the true count may be driven by something richer underneath. The method names that hidden structure and turns it into a formal certificate.

The idea comes from the Erdős unit-distance miss. A classical extremal problem can be lifted to a richer carrier: a new space with its own relation and its own energy function. A finite window in that carrier projects back to the visible surface. The key move is that many distinct carrier events can land on the same visible invariant. When that happens, the visible event count can beat linear growth by a fixed exponent, a polynomial gain that visible-dimensional counting alone would not predict.

The module records the abstract shape of the lift-return proof. A projection-multiplicity certificate has four parts: choose a richer carrier, choose finite windows in it, certify that carrier events project to valid visible events, and prove a fixed polynomial gain in the visible event count. The formal theorem certificate_gives_polynomial_gain states that any certificate yields a positive exponent δ such that the event count grows at least as fast as the visible size raised to 1+δ. That is the punchline: the method does not merely suggest a gain, it proves one.

In Recognition Science, the method is a diagnostic tool. A problem should be checked for projection multiplicity when its visible relation is the projection of a carrier relation and the event count is controlled by fiber multiplicity rather than by visible dimension alone. The module defines a candidate predicate with four tests: a hidden carrier exists, the visible relation is projected, fibers can grow, and the carrier geometry stays controlled. Only when all four hold is a full attack worth starting.

The point is not to formalize the OpenAI/Sawin proof of the unit-distance problem. The point is to name the failure mode so future problems are checked for it. The method gives a plain lesson: when counting events, ask whether a high-rank carrier might be projecting many events onto the same low-dimensional invariant. If so, the visible dimension is not the whole story.

/-- A classical extremal problem consists of visible objects, a relation whose
instances are counted, and two numerical readouts: visible size and event count. -/
structure ClassicalExtremalProblem where
  Visible : Type u
  relation : Visible → Visible → Prop
  size : Finset Visible → ℝ
  eventCount : Finset (Visible × Visible) → ℝ

/-- The formal output of the method: the lifted carrier gives a visible
polynomial gain. -/
theorem certificate_gives_polynomial_gain
    (C : ProjectionMultiplicityCertificate.{u, v}) :
    ∃ δ : ℝ, 0 < δ ∧ BeatsLinearBy C.visibleSize C.eventCount δ :=
  ⟨C.delta, C.delta_pos, C.polynomial_gain⟩

/-- Diagnostic predicate for the rule we missed.  A problem should be checked
for projection multiplicity when its visible relation can be expressed as the
projection of a carrier relation and the event count is controlled by fiber
multiplicity rather than by visible dimension alone. -/
structure ProjectionMultiplicityCandidate where
  has_hidden_carrier : Prop
  visible_relation_is_projected : Prop
  fibers_can_grow : Prop
  carrier_geometry_stays_controlled : Prop

What this page does not claim

The module does not formalize the OpenAI/Sawin proof of the Erdős unit-distance problem. The method does not prove that any particular classical problem has a hidden carrier; it only names the conditions under which a check is warranted. The polynomial gain is a lower bound, not an exact count of the visible events.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/ProjectionMultiplicityMethod.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: