Motivation

How many pairs of points in an $n$-point planar set can be at distance one? Counting all pairs gives the trivial bound $\binom n2$, but Euclidean geometry imposes a much stronger restriction: there are at most $Cn^{4/3}$ unit-distance pairs, for an absolute constant $C$.

This mission concerns that upper bound alone.

Statement

For a finite set $P\subseteq\mathbb R^2$, let $u(P)$ be the number of unordered pairs of distinct points at Euclidean distance one:

$$u(P)=\#\bigl\{\{p,q\}:p,q\in P,\ p\ne q,\ \|p-q\|=1\bigr\}.$$

Prove that there exists a constant $C>0$ such that

$$u(P)\le C|P|^{4/3}$$

for every finite $P\subseteq\mathbb R^2$. The constant must be independent of $P$, and there are no general-position assumptions.

Proof idea

The supplied proof uses the crossing lemma. From the unit circles centred at the points of $P$, it constructs an auxiliary graph with $n=|P|$ vertices and $e$ edges satisfying

$$u(P)-n\le e, \qquad \operatorname{cr}(G)\le 2n^2.$$

If $e<4n$, then $u(P)<5n$. Otherwise, the crossing lemma gives

$$\frac{e^3}{100n^2}\le \operatorname{cr}(G)\le 2n^2,$$

so $e\le \sqrt[3]{200}\,n^{4/3}$. Together, these cases give the required bound.

The main work is in constructing the graph, controlling its crossings, and proving the crossing lemma. The final numerical deduction is short. The project includes a written proof alongside the Lean development.

Lean formulation and scope

The plane is represented by EuclideanSpace ℝ (Fin 2) and point sets by Finset. The definition of unitDist P counts ordered pairs of distinct points at distance one, then divides by two.

The target proposition is:

∃ C : ℝ, 0 < C ∧
  ∀ P : Finset (EuclideanSpace ℝ (Fin 2)),
    (unitDist P : ℝ) ≤
      C * (P.card : ℝ) ^ ((4 : ℝ) / 3)

This includes empty and singleton sets and uses real exponentiation.

The crossing-consequences project already contains a sorry-free proof of this theorem. The purpose of the mission is to make it available for publication and community verification on Prove2me. The crossing lemma and other supporting results are not separate mission targets. Neither an optimal constant nor a matching lower bound is required.

References

• J. Spencer, E. Szemerédi, and W. T. Trotter, Jr., “Unit distances in the Euclidean plane,” in B. Bollobás (ed.), Graph Theory and Combinatorics, Academic Press, 1984, pp. 293–303. Full text.
• wpegden/crossing-consequences, commit 8769d142033fce042f502bf2857afb6b1375b5c3. Project overview and build instructions.