Dart rotations and componentwise Euler planarity

Definition

FourColor_GraphRotation

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.

Formalization note: this is a source-derived graph interface. It defines cyclic incidence and Euler planarity independently of any drawing or coloring theorem; geometric existence is a separate child obligation. It supports the source-backed parent FourColor.graph_realization.

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.

Definition code

import Definitions.Def_FourColor_GraphBridge
import Mathlib.Combinatorics.SimpleGraph.Dart

/-!
# Rotation systems on graph darts

Source-derived graph interface for `FourColor.graph_realization`: Gonthier (2005),
Section 2, PDF p. 4 (graph drawings), and Section 5.1, PDF pp. 18–20 (reciprocal
darts, circular lists, triangular identity and unnumbered Euler formula). This is not the topological-map theorem
`discretize_to_hypermap` in Section 5.6, PDF pp. 48–51.

The geometric existence of a rotation satisfying Euler's equality is an explicit
separate obligation. These definitions make no assertion about plane drawings.
-/

namespace FourColor

universe u

variable {V : Type u} (G : SimpleGraph V)

/-- Reversal of an oriented graph edge. -/
def dartReverse : Equiv.Perm G.Dart where
  toFun := SimpleGraph.Dart.symm
  invFun := SimpleGraph.Dart.symm
  left_inv := SimpleGraph.Dart.symm_symm
  right_inv := SimpleGraph.Dart.symm_symm

/-- One cyclic order on all darts issuing from each nonisolated vertex. -/
structure DartRotation where
  rotate : Equiv.Perm G.Dart
  sameCycle_iff : ∀ x y, rotate.SameCycle x y ↔ x.fst = y.fst

namespace DartRotation

variable {G}

/-- Boundary permutation, with the convention forced by `node (face (edge x)) = x`. -/
def boundary (R : DartRotation G) : Equiv.Perm G.Dart :=
  dartReverse G * R.rotate⁻¹

/-- Reversal and vertex rotation generate the edge-containing graph components. -/
def Link (R : DartRotation G) (x y : G.Dart) : Prop :=
  dartReverse G x = y ∨ R.rotate x = y

/-- Euler equality for the rotation system, counting each dart component separately.
Isolated vertices have no darts and contribute to none of these four counts. -/
def EulerPlanar (R : DartRotation G) : Prop :=
  Nat.card (Quotient (Equiv.Perm.SameCycle.setoid (dartReverse G))) +
      Nat.card (Quotient (Equiv.Perm.SameCycle.setoid R.boundary)) +
      Nat.card (Quotient (Equiv.Perm.SameCycle.setoid R.rotate)) =
    Nat.card G.Dart + 2 * Nat.card (Quotient (Relation.EqvGen.setoid R.Link))

end DartRotation

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