Prove2Me

Minimal drawing without adjacent crossings

Open
NoAdjacentMinimalDrawing

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

crossing-numbergeometrygraph-theory

Every finite simple graph has an ordinary polygonal drawing that realizes the graph crossing number and has no crossing between adjacent edges:

∃D,∣crossingSet⁡(D)∣=CrossingNumber⁡(G)andadjacentEdgeCrossingCount⁡(D)=0.\exists D,\quad |\operatorname{crossingSet}(D)|=\operatorname{CrossingNumber}(G) \quad\text{and}\quad \operatorname{adjacentEdgeCrossingCount}(D)=0.

The statement is obtained by choosing a crossing-minimal drawing and locally rerouting the tails of any pair of adjacent crossing edges. It is the general-position drawing used by the crossing-lemma proof.

Preamble
import Definitions.Def_CrossingNumber

open Classical
noncomputable section
Formal statement
lemma NoAdjacentMinimalDrawing {V : Type*} [Fintype V] (G : SimpleGraph V)
    [Fintype G.edgeSet] :
    ∃ D : OrdinaryPolygonalDrawing G,
      D.crossingSet.card = CrossingNumber G ∧ D.adjacentEdgeCrossingCount = 0 := by sorry
Source
https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/NoAdjacentMinimalDrawing.lean#L1-L38

View graph