Plane Graphs, Euler's Formula and the Five Colour Theorem

About this page

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 28 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 28 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

1 · Prerequisites

Abstract Algebra

Combinatorics

Linear Algebra

Real Analysis

Set Theory

Topology

2 · Logical flowchart

3 · Items

Definition

Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs

Lemma

In a three-connected plane graph, face boundaries are exactly the induced cycles whose deletion leaves the graph connected

Definition

Facial boundary walks of a connected plane graph sum to 2|E|, and if every such walk has length at least g then g|F|≤2|E|

Lemma

In an edge-maximal graph with no K₅ or K_3,3 subdivision, a minimum proper separation of order at most two has an adjacent two-vertex separator and edge-maximal sides

Lemma

Every edge-maximal graph of order at least four with no subdivision of K₅ or K_3,3 is three-connected

Theorem

Kuratowski–Wagner theorem: a finite graph is planar exactly when it has neither a K₅ nor a K_3,3 minor, equivalently neither subdivision

Definition

The plane dual multigraph, with a vertex for each face and one crossing edge for each primal edge

Theorem

Every connected plane graph has a plane dual multigraph, and when that dual is simple the reciprocal embedding identifies the double dual with the original graph

Theorem

Every planar graph has a proper vertex colouring with at most six colours

Lemma

For five cyclically ordered neighbours of a plane vertex, alternating Kempe paths between the first and third and between the second and fourth cannot both occur

Theorem

Five colour theorem: every planar graph has chromatic number at most five

Sources

Plane Graphs, Euler's Formula and the Five Colour Theorem

3 · Items

Polygonal arcs and polygons as non-self-intersecting finite unions of line segments in ℝ²

Regions of the complement of a planar set and their frontiers

Every point off a polygon admits a ray meeting it transversely in finitely many nonvertex points

The parity of transverse ray crossings with a polygon is locally constant on its complement

Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each

The complement of a polygonal arc in ℝ² is polygonally connected

Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs

A plane graph has finitely many faces and exactly one unbounded face

Every face of a plane subgraph contains each face of the original graph that it meets

Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one

Every plane forest has exactly one face

If two distinct faces of a connected plane graph have the same boundary subgraph, then the graph is a cycle

Every face of a two-connected plane graph is bounded by a cycle

In a three-connected plane graph, face boundaries are exactly the induced cycles whose deletion leaves the graph connected

Maximal plane graphs, plane triangulations, and maximally planar abstract graphs

A two-connected plane graph of order at least three is maximal exactly when every face is triangular

Euler's formula |V|-|E|+|F|=2 for every connected plane graph

For a plane graph with c components, |V|-|E|+|F|=1+c, including the null graph

Facial boundary walks of a connected plane graph sum to 2|E|, and if every such walk has length at least g then g|F|≤2|E|

Every plane triangulation with at least three vertices is connected

Every simple planar graph with n≥3 vertices has at most 3n-6 edges, with equality for every plane triangulation

Every triangle-free simple planar graph with n≥3 vertices has at most 2n-4 edges

Every nonnull simple planar graph has a vertex of degree at most five

K₅ and K_3,3 are nonplanar

A planar graph contains no subdivision of K₅ or K_3,3

For a two-connected planar graph of order at least three, maximal planarity is equivalent to having 3n-6 edges

A graph has a K₅ or K_3,3 minor exactly when it has a subdivision of K₅ or K_3,3 as a subgraph

Every three-connected graph with no K₅ or K_3,3 minor is planar

In an edge-maximal graph with no K₅ or K_3,3 subdivision, a minimum proper separation of order at most two has an adjacent two-vertex separator and edge-maximal sides

Every edge-maximal graph of order at least four with no subdivision of K₅ or K_3,3 is three-connected

Kuratowski–Wagner theorem: a finite graph is planar exactly when it has neither a K₅ nor a K_3,3 minor, equivalently neither subdivision

The plane dual multigraph, with a vertex for each face and one crossing edge for each primal edge

Every connected plane graph has a plane dual multigraph, and when that dual is simple the reciprocal embedding identifies the double dual with the original graph

Every planar graph has a proper vertex colouring with at most six colours

For five cyclically ordered neighbours of a plane vertex, alternating Kempe paths between the first and third and between the second and fourth cannot both occur

Five colour theorem: every planar graph has chromatic number at most five