IndisputableMonolith.Mathematics.ProjectionMultiplicityMethod

   1import Mathlib
   2
   3/-!
   4# Projection Multiplicity Method
   5
   6This module records the abstract method exposed by the Erdős unit-distance
   7miss: a classical extremal problem can be attacked by lifting it to a richer
   8carrier, producing many hidden carrier events, and projecting those events back
   9to the visible classical surface.
  10
  11The point is not to formalize the OpenAI/Sawin proof.  The point is to name the
  12method so future classical problems are checked for the same failure mode:
  13visible-dimensional counting can be beaten when a high-rank carrier has many
  14distinct events that project to the same low-dimensional invariant.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Mathematics
  19namespace ProjectionMultiplicityMethod
  20
  21open Filter
  22open scoped Topology
  23
  24universe u v
  25
  26/-- A classical extremal problem consists of visible objects, a relation whose
  27instances are counted, and two numerical readouts: visible size and event count. -/
  28structure ClassicalExtremalProblem where
  29  Visible : Type u
  30  relation : Visible → Visible → Prop
  31  size : Finset Visible → ℝ
  32  eventCount : Finset (Visible × Visible) → ℝ
  33
  34/-- A lift puts the visible problem on a richer carrier and projects back. -/
  35structure LiftData (P : ClassicalExtremalProblem.{u}) where
  36  Carrier : Type v
  37  project : Carrier → P.Visible
  38  carrierRelation : Carrier → Carrier → Prop
  39  energy : Carrier → ℝ
  40
  41/-- A finite window in the carrier, together with its projected visible set and
  42the events certified inside the window. -/
  43structure FiniteWindow {P : ClassicalExtremalProblem.{u}}
  44    (L : LiftData.{u, v} P) where
  45  carrierSet : Finset L.Carrier
  46  visibleSet : Finset P.Visible
  47  liftedEvents : Finset (L.Carrier × L.Carrier)
  48  visibleEvents : Finset (P.Visible × P.Visible)
  49  projection_covers :
  50    ∀ x ∈ carrierSet, L.project x ∈ visibleSet
  51  event_sound :
  52    ∀ e ∈ liftedEvents,
  53      L.carrierRelation e.1 e.2 ∧
  54        P.relation (L.project e.1) (L.project e.2)
  55  event_projects :
  56    ∀ e ∈ liftedEvents,
  57      (L.project e.1, L.project e.2) ∈ visibleEvents
  58
  59/-- The projected event count beats linear growth by a fixed exponent. -/
  60def BeatsLinearBy (N E : ℕ → ℝ) (δ : ℝ) : Prop :=
  61  ∀ᶠ k in atTop, 0 < N k ∧ Real.rpow (N k) (1 + δ) ≤ E k
  62
  63/-- A projection-multiplicity certificate is the abstract shape of the
  64lift-return proof:
  65
  661. choose a richer carrier;
  672. choose finite windows in that carrier;
  683. certify that carrier events project to valid visible events;
  694. prove a fixed polynomial gain in the visible event count.
  70-/
  71structure ProjectionMultiplicityCertificate where
  72  P : ClassicalExtremalProblem.{u}
  73  L : LiftData.{u, v} P
  74  window : ℕ → FiniteWindow L
  75  visibleSize : ℕ → ℝ
  76  eventCount : ℕ → ℝ
  77  delta : ℝ
  78  delta_pos : 0 < delta
  79  size_matches :
  80    ∀ᶠ k in atTop, visibleSize k = P.size ((window k).visibleSet)
  81  event_matches :
  82    ∀ᶠ k in atTop, eventCount k = P.eventCount ((window k).visibleEvents)
  83  polynomial_gain : BeatsLinearBy visibleSize eventCount delta
  84
  85/-- The formal output of the method: the lifted carrier gives a visible
  86polynomial gain. -/
  87theorem certificate_gives_polynomial_gain
  88    (C : ProjectionMultiplicityCertificate.{u, v}) :
  89    ∃ δ : ℝ, 0 < δ ∧ BeatsLinearBy C.visibleSize C.eventCount δ :=
  90  ⟨C.delta, C.delta_pos, C.polynomial_gain⟩
  91
  92/-- Diagnostic predicate for the rule we missed.  A problem should be checked
  93for projection multiplicity when its visible relation can be expressed as the
  94projection of a carrier relation and the event count is controlled by fiber
  95multiplicity rather than by visible dimension alone. -/
  96structure ProjectionMultiplicityCandidate where
  97  has_hidden_carrier : Prop
  98  visible_relation_is_projected : Prop
  99  fibers_can_grow : Prop
 100  carrier_geometry_stays_controlled : Prop
 101
 102/-- The candidate has the four tests required before starting a full
 103projection-multiplicity attack. -/
 104def ProjectionMultiplicityCandidate.Ready
 105    (C : ProjectionMultiplicityCandidate) : Prop :=
 106  C.has_hidden_carrier ∧
 107    C.visible_relation_is_projected ∧
 108    C.fibers_can_grow ∧
 109    C.carrier_geometry_stays_controlled
 110
 111end ProjectionMultiplicityMethod
 112end Mathematics
 113end IndisputableMonolith
 114