Polygonal replacement for geometric arcs

Open

PolygonalReplacementForGeometricArcs

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

crossing-numbergeometrygraph-theory

Let $G$ be a finite simple graph and let $D$ be a geometric arc drawing of $G$ . Then there is an ordinary polygonal drawing $D'$ of the same graph such that

|\operatorname{crossingSet}(D')|\le \operatorname{localPairCount}(D) \qquad ext{and}\qquad \operatorname{CrossingNumber}(G)\le \operatorname{localPairCount}(D).

Thus every geometric arc drawing can be replaced by a polygonal drawing whose crossing set, and hence the graph's minimum crossing number, is controlled by the local pair count of the original drawing.

Preamble

import Definitions.Def_GeometricArcDrawing
import Definitions.Def_CrossingNumber

open Classical
noncomputable section

Formal statement

lemma PolygonalReplacementForGeometricArcs {V : Type*} [Fintype V]
    (G : SimpleGraph V) [Fintype G.edgeSet] (D : GeometricArcDrawing G) :
    ∃ D' : OrdinaryPolygonalDrawing G,
      D'.crossingSet.card ≤ D.localPairCount ∧
        CrossingNumber G ≤ D.localPairCount := by sorry

Source

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

View graph