Plane drawings admit Euler-planar rotations on oriented edges

Open

FourColor.plane_drawing_dart_rotation

by Minghui · Sep 28, 2026 · Mathlib c5ea003 (Lean v4.30.0)

four-color-theoremgraph-theory

Let $G$ be a simple graph on a finite type $V$ . Write $D$ for its oriented edges: a dart is an ordered adjacent pair $(v,w)$ . Let $\alpha(v,w)=(w,v)$ . A dart rotation $\rho$ is a permutation of $D$ whose cycles are exactly the nonempty sets of darts with a fixed initial vertex. Thus isolated vertices have no darts. Write $c(\sigma)$ for the number of cycles of a permutation, including fixed points, and $C$ for the number of classes of the equivalence generated by the steps $d\mapsto\alpha d$ and $d\mapsto\rho d$ . Here $n = |D|$ is the number of darts. There is no probability model. The predicate EulerPlanar is the exact equality

c(\alpha)+c(\alpha\rho^{-1})+c(\rho)=n+2C.

Component counts omit isolated vertices; boundary cycles are counted separately for each edge-containing component, not as the regions of the global plane complement.

Suppose $G$ has a crossing-free drawing by continuous injective arcs in the real plane, with distinct vertices, reversal-compatible parameterizations, and no intersections except shared endpoints. Then

\exists\rho,\quad (d\sim_\rho d'\iff d.\mathrm{fst}=d'.\mathrm{fst})\quad\text{and}\quad c(\alpha)+c(\alpha\rho^{-1})+c(\rho)=n+2C.

This includes empty, edgeless, disconnected graphs and graphs with bridges. It assumes neither polygonal arcs nor differentiability nor connectedness.

Formalization note: this is the source-derived geometric child of FourColor.graph_realization, isolating the passage from continuous graph drawings to compatible cyclic orders and Euler equality. It is not a literal restatement of the region-map theorem discretize_to_hypermap. Its conclusion is stronger than an arbitrary choice of cyclic orders at vertices.

Source: Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem (2005), https://www.microsoft.com/en-us/research/wp-content/uploads/2012/10/4colproof.pdf; Section 2, PDF p. 4, paragraph beginning Although the statement; Section 5.1, PDF p. 18, numbered construction items 2–3 (reciprocal darts and geometrically ordered circular lists), PDF p. 19, item 5 (triangular identity), and PDF p. 20, paragraph following the unnumbered Euler formula (orbit counts, components and graph/map duality). The displayed identities are unnumbered. The source-backed parent is FourColor.graph_realization.

Preamble

import Definitions.Def_FourColor_GraphRotation

Formal statement

namespace FourColor
universe u
theorem plane_drawing_dart_rotation :
  ∀ (V : Type u) [Finite V] (G : SimpleGraph V), IsPlanar G →
    ∃ R : DartRotation G, R.EulerPlanar := by sorry
end FourColor

Source

Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem (2005), https://www.microsoft.com/en-us/research/wp-content/uploads/2012/10/4colproof.pdf; Section 2, PDF p. 4, paragraph beginning Although the statement; Section 5.1, PDF p. 18, numbered construction items 2–3 (reciprocal darts and geometrically ordered circular lists), PDF p. 19, item 5 (triangular identity), and PDF p. 20, paragraph following the unnumbered Euler formula (orbit counts, components and graph/map duality). The displayed identities are unnumbered. The source-backed parent is FourColor.graph_realization.

View graph