Euler-planar dart rotations give exact hypermap face representations

Proved

FourColor.dart_rotation_face_realization

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.

For every Euler-planar dart rotation of $G$ , there is a hypermap $H$ on $\operatorname{Fin}(n)$ such that

H\text{ is planar and plain},\qquad \exists r:\operatorname{Fin}(n)\to V,\quad (x\sim_f y\iff r(x)=r(y)),

G(v,w)\iff\exists x,\ r(x)=v\ \land\ r(e(x))=w.

Planar means the exact componentwise Euler equality; plain means the edge permutation is a fixed-point-free involution. This includes zero darts.

Formalization note: a purely finite formal bridge to the source-backed parent FourColor.graph_realization from its child plane_drawing_dart_rotation. It translates graph-dart rotation data into the existing hypermap interface. It requires no drawing and does not assert geometric existence of a rotation.

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 dart_rotation_face_realization :
  ∀ (V : Type u) [Finite V] (G : SimpleGraph V) (R : DartRotation G), R.EulerPlanar →
    ∃ (n : ℕ) (H : Hypermap n), H.Planar ∧ H.Plain ∧ Nonempty (FaceRepresentation G H) := 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