Mathematics Bipartite Distance Spectrum

The distance spectrum

The bipartite distance spectrum is a classical combinatorial object. Given two finite sets of points, P and Q, it is the set of all distances between a point of P and a point of Q. The central question, Erdős problem #661, asks whether two n-point sets in the plane can have a distance spectrum whose size grows slower than n divided by the square root of the natural logarithm of n. The square-grid construction, where both sets are n points on a lattice, achieves exactly this scale, so the problem is whether any configuration can beat it.

The problem has a long history. Erdős posed it in 1946 in the wake of his work on the distinct distances problem, where the same counting question is asked for a single set. The bipartite version is strictly harder: the two sets can be placed to maximize collisions between distances, and the square grid is the natural candidate for the extremal configuration. The scale n / sqrt(log n) arises from the number of distinct values of a quadratic form on a lattice, a count that connects to the distribution of sums of two squares.

The framework's library, a machine-checked collection of formal theorems, reformulates this problem in physical language. In this account, the two sets are sources and detectors in a plane, and the distance spectrum is the readout of a range experiment. The framework models the square-grid scale as rigid: it predicts that no planar configuration can force the spectrum below that scale, because true orthogonality between two sectors is unavailable in a single plane. This is stated as a target, not a proof.

The module also records a striking contrast in four dimensions. In R^4, it is possible for all cross-distances between two finite sets to be identical, a configuration called a Lenz-style collapse. This orthogonal two-sector mechanism, available in four dimensions, is exactly what is missing in the plane, and its absence is why the planar problem is hard. The module defines the four-dimensional collapse as a formal property, and the planar rigidity target as a separate conjecture.

The library proves one simple theorem: the size of the squared distance spectrum is at most the product of the sizes of the two sets. This is a trivial upper bound, but it is the starting point for the real question, which is how far below that bound a configuration can go. The framework's contribution is to name the exact lemma needed for a conventional proof: if the cross-distance spectrum is small, then the points must lie approximately on a Gaussian-integer-like lattice. That lemma is not proved here; it is the stated target for future work.

/-- The unsquared distance alphabet.  Squaring is often cleaner algebraically,
but both alphabets carry the same asymptotic information away from sign issues
because distance is nonnegative. -/
noncomputable def crossDistSpectrum (P Q : Finset Point2) : Finset ℝ := by
  classical
  exact (P.product Q).image (fun pq => dist pq.1 pq.2)

/-- Negative RS target: planar cross-spectrum rigidity at the grid scale. -/
def PlanarCrossSpectrumRigidity : Prop :=
  ∃ c : ℝ, 0 < c ∧
    ∀ᶠ n in atTop,
      ∀ P Q : Finset Point2,
        P.card = n →
        Q.card = n →
          c * ((n : ℝ) / Real.sqrt (Real.log n)) ≤
            ((crossDistSpectrum P Q).card : ℝ)

/-- Lenz-style collapse in a richer carrier: all cross-distances between two
finite channels in `ℝ⁴` are the same.  Erdős #661 is hard because this
orthogonal two-sector mechanism is not available in one planar carrier. -/
def FixedCrossDistanceInFourSpace (P Q : Finset Point4) : Prop :=
  ∃ r : ℝ, ∀ p ∈ P, ∀ q ∈ Q, dist p q = r

/-- Trivial upper bound: the cross spectrum has at most one value per
source-detector pair. -/
theorem crossDistSqSpectrum_card_le_pairs (P Q : Finset Point2) :
    (crossDistSqSpectrum P Q).card ≤ P.card * Q.card := by
  classical
  unfold crossDistSqSpectrum
  calc
    ((P.product Q).image (fun pq => dist pq.1 pq.2 ^ 2)).card ≤
        (P.product Q).card := Finset.card_image_le
    _ = P.card * Q.card := by simp

What this page does not claim

The planar rigidity target is not proved in this module. The inverse theorem on Gaussian-like lattices is not asserted as proved. The framework's physical reading does not constitute a mathematical proof of Erdős #661.

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/BipartiteDistanceSpectrum.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: