IndisputableMonolith.Mathematics.BipartiteDistanceSpectrum

   1import Mathlib
   2
   3/-!
   4# Bipartite Distance Spectrum
   5
   6This module records the physicalized form of Erdős problem #661.
   7
   8In RS terms the problem is a two-channel range-spectrum question:
   9two finite planar channels `P` and `Q` are coupled by Euclidean propagation
  10delay, and the classical distance count is the alphabet size of the
  11cross-coupling spectrum.
  12
  13The positive Erdős #661 direction asks whether that alphabet can be
  14`o(n / sqrt(log n))`.  The RS physical reading suggests the opposite target:
  15in a single positive-definite planar carrier, true two-sector orthogonality is
  16unavailable, so the square-grid `n / sqrt(log n)` scale should be rigid.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Mathematics
  21namespace BipartiteDistanceSpectrum
  22
  23open Filter
  24open scoped Topology
  25
  26noncomputable section
  27
  28abbrev Point2 := EuclideanSpace ℝ (Fin 2)
  29abbrev Point4 := EuclideanSpace ℝ (Fin 4)
  30
  31/-- The squared cross-distance alphabet between two finite planar channels. -/
  32noncomputable def crossDistSqSpectrum (P Q : Finset Point2) : Finset ℝ := by
  33  classical
  34  exact (P.product Q).image (fun pq => dist pq.1 pq.2 ^ 2)
  35
  36/-- The unsquared distance alphabet.  Squaring is often cleaner algebraically,
  37but both alphabets carry the same asymptotic information away from sign issues
  38because distance is nonnegative. -/
  39noncomputable def crossDistSpectrum (P Q : Finset Point2) : Finset ℝ := by
  40  classical
  41  exact (P.product Q).image (fun pq => dist pq.1 pq.2)
  42
  43/-- A two-channel range experiment: sources and detectors in the visible plane. -/
  44structure TwoChannelRangeExperiment where
  45  sources : Finset Point2
  46  detectors : Finset Point2
  47
  48/-- The physical readout is the cross-coupling alphabet. -/
  49noncomputable def TwoChannelRangeExperiment.crossCouplingSpectrum
  50    (E : TwoChannelRangeExperiment) : Finset ℝ :=
  51  crossDistSpectrum E.sources E.detectors
  52
  53/-- Trivial upper bound: the cross spectrum has at most one value per
  54source-detector pair. -/
  55theorem crossDistSqSpectrum_card_le_pairs (P Q : Finset Point2) :
  56    (crossDistSqSpectrum P Q).card ≤ P.card * Q.card := by
  57  classical
  58  unfold crossDistSqSpectrum
  59  calc
  60    ((P.product Q).image (fun pq => dist pq.1 pq.2 ^ 2)).card ≤
  61        (P.product Q).card := Finset.card_image_le
  62    _ = P.card * Q.card := by simp
  63
  64/-- Positive formulation of Erdős #661: there are two `n`-point planar channels
  65whose cross-distance alphabet is little-o of the square-grid scale. -/
  66def Erdos661Positive : Prop :=
  67  ∃ P Q : ℕ → Finset Point2,
  68    (∀ᶠ n in atTop, (P n).card = n ∧ (Q n).card = n) ∧
  69      Tendsto
  70        (fun n : ℕ =>
  71          ((crossDistSpectrum (P n) (Q n)).card : ℝ) /
  72            ((n : ℝ) / Real.sqrt (Real.log n)))
  73        atTop
  74        (𝓝 0)
  75
  76/-- Negative RS target: planar cross-spectrum rigidity at the grid scale. -/
  77def PlanarCrossSpectrumRigidity : Prop :=
  78  ∃ c : ℝ, 0 < c ∧
  79    ∀ᶠ n in atTop,
  80      ∀ P Q : Finset Point2,
  81        P.card = n →
  82        Q.card = n →
  83          c * ((n : ℝ) / Real.sqrt (Real.log n)) ≤
  84            ((crossDistSpectrum P Q).card : ℝ)
  85
  86/-- Lenz-style collapse in a richer carrier: all cross-distances between two
  87finite channels in `ℝ⁴` are the same.  Erdős #661 is hard because this
  88orthogonal two-sector mechanism is not available in one planar carrier. -/
  89def FixedCrossDistanceInFourSpace (P Q : Finset Point4) : Prop :=
  90  ∃ r : ℝ, ∀ p ∈ P, ∀ q ∈ Q, dist p q = r
  91
  92/-! ## Planar norm-fiber rigidity target -/
  93
  94/-- Squared norm in the visible planar carrier. -/
  95noncomputable def normSq (p : Point2) : ℝ :=
  96  ‖p‖ ^ 2
  97
  98/-- The squared-norm alphabet of a finite planar set. -/
  99noncomputable def normSqImage (A : Finset Point2) : Finset ℝ := by
 100  classical
 101  exact A.image normSq
 102
 103/-- The cross-difference set `Q - P`. -/
 104noncomputable def crossDifferenceSet (P Q : Finset Point2) : Finset Point2 := by
 105  classical
 106  exact (P.product Q).image (fun pq => pq.2 - pq.1)
 107
 108/-- The squared-norm alphabet of all cross-differences. -/
 109noncomputable def crossNormSqAlphabet (P Q : Finset Point2) : Finset ℝ :=
 110  normSqImage (crossDifferenceSet P Q)
 111
 112/-- A rank-two lattice-like carrier in the visible plane, recorded only at the
 113level needed for the inverse theorem target.  The `basis` map is the proposed
 114Gaussian-integer coordinate chart; `integral_norm` says visible squared norm is
 115read from an integral positive binary quadratic form after scaling. -/
 116structure GaussianLikeLattice where
 117  basis : (Fin 2 → ℤ) → Point2
 118  scale : ℝ
 119  scale_pos : 0 < scale
 120  qform : (Fin 2 → ℤ) → ℤ
 121  qform_nonneg : ∀ z, 0 ≤ qform z
 122  integral_norm :
 123    ∀ z, normSq (basis z) = scale * (qform z : ℝ)
 124
 125/-- A finite set is approximately carried by a Gaussian-like lattice if all but
 126`error` of its points lie in the lattice image.  This is deliberately weak:
 127future work can replace it by density-in-a-box, Freiman-isomorphism, or Hausdorff
 128distance variants without changing the physical statement. -/
 129def ApproxContainedInGaussianLikeLattice
 130    (A : Finset Point2) (Λ : GaussianLikeLattice) (error : ℕ) : Prop :=
 131  ∃ A₀ : Finset Point2,
 132    A₀ ⊆ A ∧
 133      A.card ≤ A₀.card + error ∧
 134      ∀ a ∈ A₀, ∃ z : Fin 2 → ℤ, Λ.basis z = a
 135
 136/-- The inverse theorem target left by the RS physicalization:
 137small cross-norm alphabet at the Landau-Ramanujan scale forces the visible
 138points to be approximately carried by a Gaussian-integer-like lattice.
 139
 140This is not asserted as proved here; it is the exact classical lemma needed to
 141turn the RS physical statement into a conventional proof. -/
 142def PlanarNormFiberRigidityTarget : Prop :=
 143  ∀ᶠ n in atTop,
 144    ∀ P Q : Finset Point2,
 145      P.card = n →
 146      Q.card = n →
 147      ((crossNormSqAlphabet P Q).card : ℝ) ≤
 148          (n : ℝ) / Real.sqrt (Real.log n) →
 149        ∃ Λ : GaussianLikeLattice,
 150          ApproxContainedInGaussianLikeLattice P Λ (n / 100) ∧
 151          ApproxContainedInGaussianLikeLattice Q Λ (n / 100)
 152
 153end
 154end BipartiteDistanceSpectrum
 155end Mathematics
 156end IndisputableMonolith
 157