Paper
Planar Graphs Are 6-Colorable
2 pages · 8 marked passages · pdflatex · download PDF · lax-909950
-
Euler's formula
Let be a finite connected graph with a crossing-free straight-line drawing in the plane. The faces of the drawing are the connected components of the plane after removing all drawn points and edge segments. If the drawing has vertices, edges and faces, then
The formula is stated as in the extended natural numbers, so that it also asserts that the number of faces is finite.
1 import Mathlib.Data.Set.Card 2 import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected 3 import Mathlib.Topology.Connected.Basic 4 import Mathlib.Topology.Instances.Real.Lemmas 5 import Lax68.StraightLineDrawings 6 … module docstring, 14 lines 21 22 set_option autoImplicit false 23 24 namespace Lax909950.EulerFormula 25 26 open Lax68.StraightLineDrawings 27 28 /-- The points of the plane covered by a straight-line drawing: the points of 29 the vertices together with the segments of the edges. -/ 30 def image {V : Type*} {G : SimpleGraph V} (D : StraightLineDrawing G) : Set Point := 31 Set.range D.point ∪ ⋃ (a : V) (b : V) (_ : G.Adj a b), segment ℝ (D.point a) (D.point b) 32 33 /-- The faces of a straight-line drawing: the connected components of the 34 complement of its image. -/ 35 def faces {V : Type*} {G : SimpleGraph V} (D : StraightLineDrawing G) : Set (Set Point) := 36 {F | ∃ x ∉ image D, F = connectedComponentIn (image D)ᶜ x} 37 38 /-- Euler's formula: a crossing-free straight-line drawing of a finite connected 39 graph with vertices and edges has exactly faces, where 40 . -/ 41 axiom euler_formula {V : Type*} [Finite V] {G : SimpleGraph V} 42 (hG : G.Connected) (D : StraightLineDrawing G) : 43 (Nat.card V : ℕ∞) + (faces D).encard = G.edgeSet.encard + 2 44 45 end Lax909950.EulerFormula 46 -
no assumptions
By induction on the number of edges. A tree has one face. Otherwise some edge lies on a cycle; its two sides lie in different faces, and deleting it merges them.
-
Planar graphs have at most 3v − 6 edges
Every finite planar graph with vertices has at most edges.
1 import Mathlib.Data.Set.Card 2 import Lax68.Planar 3 … module docstring, 7 lines 11 12 set_option autoImplicit false 13 14 namespace Lax909950.EdgeDensity 15 16 /-- A finite planar graph with vertices has at most edges. 17 (Since , the natural-number subtraction does not truncate.) -/ 18 axiom edge_density {V : Type*} [Finite V] {G : SimpleGraph V} 19 (hG : Lax68.Planar.IsPlanar G) (hV : 3 ≤ Nat.card V) : 20 G.edgeSet.ncard ≤ 3 * Nat.card V - 6 21 22 end Lax909950.EdgeDensity 23 -
For a connected graph with a cycle, every face is a side face of the edges of a cycle, hence of at least edges; each edge has at most side faces, so , and Euler's formula gives . Trees have edges. Disconnected graphs split into a component and the rest, and the bound is superadditive.
-
Planar graphs have a vertex of degree at most 5
Every finite planar graph with at least one vertex has a vertex of degree at most .
1 import Mathlib.Data.Set.Card 2 import Lax68.Planar 3 … module docstring, 8 lines 12 13 set_option autoImplicit false 14 15 namespace Lax909950.LowDegree 16 17 /-- Every nonempty finite planar graph has a vertex with at most five 18 neighbors. -/ 19 axiom exists_degree_le_five {V : Type*} [Finite V] [Nonempty V] {G : SimpleGraph V} 20 (hG : Lax68.Planar.IsPlanar G) : 21 ∃ x : V, (G.neighborSet x).ncard ≤ 5 22 23 end Lax909950.LowDegree 24 -
If every vertex had degree at least , the degree sum would be at least , contradicting the edge density bound . Graphs with at most vertices are handled directly.
-
Six color theorem
Every finite planar graph admits a proper coloring of its vertices with six colors, i.e. an assignment of one of six colors to each vertex such that adjacent vertices receive different colors.
1 import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex 2 import Lax68.Planar 3 … module docstring, 9 lines 13 14 set_option autoImplicit false 15 16 namespace Lax909950.SixColoring 17 18 /-- Every finite planar graph is -colorable. -/ 19 axiom six_colorable {V : Type*} [Finite V] {G : SimpleGraph V} 20 (hG : Lax68.Planar.IsPlanar G) : 21 G.Colorable 6 22 23 end Lax909950.SixColoring 24 -
By induction on the number of vertices: remove a vertex of degree at most , color the remaining graph, and give the removed vertex a color not used by any of its neighbors.