Linear crossing-number inequality

Open

LinearCrossingInequality

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

crossing-numbergraph-theory

For a finite simple graph $G$ on vertex set $V$ , the minimum crossing number is bounded below by the excess of edges over the planar threshold:

|E(G)|-3|V|\le \operatorname{CrossingNumber}(G).

Here the crossing number is the minimum cardinality of the finite crossing set among ordinary polygonal drawings of $G$ . This is the linear inequality used in the probabilistic proof of the crossing lemma: every induced subgraph contributes its edge surplus beyond $3|V|$ to the crossing count.

Preamble

import Definitions.Def_CrossingNumber

open Classical
noncomputable section

Formal statement

lemma LinearCrossingInequality {V : Type*} [Fintype V] (G : SimpleGraph V)
    [Fintype G.edgeSet] :
    (G.edgeFinset.card : ℤ) - 3 * (Fintype.card V : ℤ) ≤
      (CrossingNumber G : ℤ) := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/LinearCrossingInequality.lean#L1-L71

View graph