The unit-distance arc graph construction

Open

UnitDistanceArcGraph

by xuanji · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

crossing-numberdiscrete-geometrygraph-theoryunit-distances

For every finite point set $P$ in the Euclidean plane, there is a simple graph $G$ whose vertex type is the finite set $P$ and whose edge set is finite such that

\operatorname{unitDist}(P)-|P|\le |E(G)|,\qquad\operatorname{cr}(G)\le 2|P|^2.

The graph is obtained from the unit-distance relations by selecting polygonal arcs and then replacing the resulting geometric arcs by an ordinary polygonal drawing. Thus its edge count records the unit-distance count up to the vertex correction, while its crossing number is controlled quadratically by the size of $P$ . This construction is the geometric bridge that allows the crossing lemma to be applied to unit distances.

Formalization Note Lean represents the finite point set as a Finset, regards G as a graph on the subtype of elements of P, and records finiteness of the graph edge set with an explicit Fintype G.edgeSet instance.

Preamble

import Definitions.Def_CrossingNumber
import Definitions.Def_unitDist

open Classical
open scoped Real
noncomputable section

Formal statement

lemma UnitDistanceArcGraph (P : Finset (EuclideanSpace ℝ (Fin 2))) :
    ∃ G : SimpleGraph P, ∃ (_ : Fintype G.edgeSet),
      (unitDist P : ℝ) - (P.card : ℝ) ≤ (G.edgeFinset.card : ℝ) ∧
        (CrossingNumber G : ℝ) ≤ 2 * (P.card : ℝ) ^ 2 := by sorry

Source

wpegden/crossing-consequences@8769d142033fce042f502bf2857afb6b1375b5c3, Tablet/UnitDistanceArcGraph.lean, declaration `UnitDistanceArcGraph`, lines 15–18: https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/UnitDistanceArcGraph.lean#L15-L18

View graph