Spencer-Szemerédi-Trotter unit-distance upper bound

unit_distance_upper_bound — a formalization challenge from the lean-eval benchmark.

Notes

For a finite set P ⊆ ℝ² write ν(P) for the number of unordered pairs at Euclidean distance 1, and ν(n) = max over n-point sets. Erdős posed the unit-distance problem in 1946 alongside the dual distinct-distances problem (resolved up to log factors by Guth-Katz, 2015). The first nontrivial upper bound ν(n) = O(n^{3/2}) follows from the Kővári-Sós-Turán theorem applied to the K_{2,3}-free unit-distance graph. Spencer-Szemerédi-Trotter (1984) sharpened this to ν(n) = O(n^{4/3}) using the Szemerédi-Trotter incidence bound for points and lines; Székely later gave a short crossing-number proof of the same exponent. The exponent 4/3 has stood since 1984 with only constant-factor improvements (Ágoston-Pálvölgyi, 2022). The matching lower bound is widely conjectured to lie much closer to the upper bound — see the companion problem erdos_unit_distance_conjecture_false.

Formal statement

/-- **Spencer–Szemerédi–Trotter (1984).** The number of unit-distance
pairs in any finite planar set is `O(n^{4/3})`: there is an absolute
constant `C > 0` such that every finite `P ⊆ ℝ²` satisfies

  `unitDist P ≤ C · |P|^{4/3}`. -/
theorem unit_distance_upper_bound :
    ∃ C : ℝ, 0 < C ∧
      ∀ P : Finset (EuclideanSpace ℝ (Fin 2)),
        (unitDist P : ℝ) ≤ C * (P.card : ℝ) ^ ((4 : ℝ) / 3) := by
  sorry

Informal solution sketch

Build the bipartite incidence structure of P with the family of unit circles centred at points of P: each unit-distance pair (x, y) corresponds to the incidence (y, C_x), where C_x is the unit circle centred at x. Two unit circles intersect in at most two points, so the incidence graph is K_{2,3}-free. Apply the Szemerédi-Trotter theorem (any n points and n curves with bounded pairwise intersection number have O(n^{4/3}) incidences) — or equivalently, Székely's crossing-number argument: draw the unit-distance graph with circular arcs, count crossings two ways, and conclude via the crossing-number inequality. Either route gives ν(n) ≤ C · n^{4/3}.

Source

J. Spencer, E. Szemerédi, W. T. Trotter Jr., Unit distances in the Euclidean plane, in Graph Theory and Combinatorics (Cambridge 1983), Academic Press, 1984. Short crossing-number proof: L. A. Székely, Crossing numbers and hard Erdős problems in discrete geometry, Combin. Probab. Comput. 6 (1997). Best constant: P. Ágoston, D. Pálvölgyi, An improved constant factor for the unit distance problem, Studia Sci. Math. Hungar. 59 (2022).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: unit_distance_upper_bound
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.