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.
Plane Graphs, Euler's Formula and the Five Colour Theorem — Examples
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Eulerian and Hamiltonian Graphs
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Graph Colouring
- Graphs, Walks and Connectivity
- Inclusion–Exclusion, the Pigeonhole Principle and Double Counting
- Limits of Real Functions
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matchings, Covers, Menger and Network Flows
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Plane Graphs, Euler's Formula and the Five Colour Theorem
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Topology of Euclidean Space
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Trees, Forests and Spanning Trees
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Euler's formula checked on a plane tree, a cycle, and the four-face embedding of
Example
Euler's formula gives the same value on a plane tree, a cycle, and the tetrahedral embedding of .
Facts & Assumptions
Given: A plane tree on vertices, a plane cycle on vertices, and the standard plane embedding of .
Every connected plane graph satisfies (Euler's formula for every connected plane graph).
A finite forest satisfies , so a tree on vertices has edges (For every forest, , where is the number of connected components).
Verification
By [L2], a tree on vertices has edges, and its plane embedding has one face by Every plane forest has exactly one face. Thus . This includes the one-vertex tree, for which the edge count is zero.
A plane cycle , in the notation of Empty and complete graphs, complete bipartite graphs, and the convention that and have vertices, has vertices and edges. Its polygon bounds one face and has the unbounded face on the other side, so .
Embed three vertices of as a triangle and place the fourth inside it, joined to all three corners. The graph has four vertices, six edges, three bounded triangular faces, and the unbounded triangular face. Hence , as [L1] requires.
is planar but has chromatic number four, so the five-colour bound cannot be lowered to three
Statement refuted
The conclusion of Five colour theorem: every planar graph has chromatic number at most five can be strengthened to say that every planar graph is three-colourable.
Facts & Assumptions
Given: The complete graph of Empty and complete graphs, complete bipartite graphs, and the convention that and have vertices.
A proper vertex colouring assigns distinct colours to adjacent vertices (Proper vertex colourings and chromatic number).
Every two distinct vertices of are adjacent (Empty and complete graphs, complete bipartite graphs, and the convention that and have vertices).
Counterexample
Draw three vertices as a triangle, place the fourth inside it, and join that vertex to the three corners. The six edges meet only at their common endpoints, so this is a plane embedding of .
By [F1] and [F2], the four vertices must receive pairwise distinct colours in any proper colouring. Assigning a different colour to each vertex is proper, so . Thus a planar graph need not be three-colourable, although Five colour theorem: every planar graph has chromatic number at most five supplies five colours for every planar graph.
The Petersen graph is nonplanar by an explicit subdivision of after deleting one vertex
Example
Deleting one vertex from the Petersen graph exposes a subdivision of .
Facts & Assumptions
Given: Label a Petersen vertex by a two-element subset of , with adjacency exactly when labels are disjoint, as in The Petersen graph on the two-element subsets of a five-element set, adjacent when disjoint.
A finite graph is planar exactly when it contains neither a subdivision of nor a subdivision of (Kuratowski–Wagner theorem: a finite graph is planar exactly when it has neither a nor a minor, equivalently neither subdivision).
Two Petersen vertices are adjacent exactly when their two-element labels are disjoint (The Petersen graph on the two-element subsets of a five-element set, adjacent when disjoint).
Verification
Delete the vertex . Take the branch classes and . The six direct branch connections are to , to , and to . The remaining three are the paths , , and .
Every consecutive pair in the displayed list has disjoint labels, so it is an edge by [F1]. The internal vertices are distinct and are not branch vertices; all other listed connections are single edges. Thus the nine paths are internally disjoint and form a subdivision, in the sense of Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors, of with branch classes and . This subdivision lies in a subgraph of the Petersen graph, so [L1] proves that the Petersen graph is nonplanar.
Two plane embeddings of one connected planar graph have nonisomorphic dual multigraphs
Example
The abstract graph below has two plane embeddings whose dual multigraphs are distinguished by their degree multisets. For a finite multigraph with the endpoint map of Multigraphs, loops and directed graphs as variants distinct from the default finite simple graph, count an ordinary incident edge once and a loop twice in the degree. An isomorphism of such endpoint-map structures is a pair of vertex and edge bijections preserving endpoints, and therefore preserves the degree multiset.
Facts & Assumptions
Given: Let have vertices . Its edges form three internally disjoint - paths , , and , together with the bridge .
Every connected plane graph has a plane dual (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).
An endpoint-preserving multigraph isomorphism preserves the degree multiset because it bijects the incident edge-ends at every vertex, with a loop contributing two ends.
Verification
Embed the three - paths in cyclic order. Write for the faces between the indicated path pairs. In the dual of The plane dual multigraph, with a vertex for each face and one crossing edge for each primal edge, the path lengths give respectively that many parallel dual edges between the two faces on each side of the path. Before accounting for , the degrees of are . The bridge may be drawn into any one of these face sectors at ; it then gives a dual loop at that face.
In one embedding draw into ; the dual degree multiset is then . In another draw it into ; the dual degree multiset is . These multisets differ, since a loop contributes two to its incident degree. By [F1] the two dual multigraphs are nonisomorphic, although both arise from the same connected planar graph .
A degree-five vertex is inserted into a plane graph after one explicit Kempe-chain colour swap
Example
One Kempe swap extends a five-colouring across the centre of a plane wheel with five rim vertices.
Facts & Assumptions
Given: Let occur in this cyclic order on a plane -cycle. Colour with colour , and plan to insert a vertex inside the cycle adjacent to every .
Swapping two colours on one Kempe component preserves a proper colouring (Swapping the two colours on one Kempe component preserves a proper colouring).
The alternating Kempe connections between cyclic neighbours and cannot both occur (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).
Verification
Before is inserted, its five prospective neighbours use all five colours. In the subgraph induced by colours and , both and are isolated: their two cycle neighbours have colours and , respectively. In particular there is no alternating - path between them, consistently with [L2].
Swap colours and on the Kempe component . The colouring remains proper by [L1]; now both and have colour , but they are nonadjacent, and no rim vertex has colour . Give the inserted centre colour . Every spoke then has differently coloured endpoints, producing an explicit five-colouring of the plane wheel and illustrating the swap used in Five colour theorem: every planar graph has chromatic number at most five.
satisfies but is nonplanar, so the planar edge bound is not sufficient
Statement refuted
Every finite simple graph with vertices and at most edges is planar.
Facts & Assumptions
Given: The complete bipartite graph of Empty and complete graphs, complete bipartite graphs, and the convention that and have vertices.
Every simple planar graph with vertices has at most edges (Every simple planar graph with vertices has at most edges, with equality for every plane triangulation).
The graph is nonplanar ( and are nonplanar).
Counterexample
The two parts of contain three vertices each, so . Every vertex in either part is adjacent to all three vertices of the other part, giving ; equivalently this follows from Handshake lemma: the sum of the vertex degrees is twice the number of edges. Consequently , so the necessary inequality in [L1] holds.
Nevertheless [L2] says that this graph is nonplanar. Hence satisfying the planar simple-graph edge bound does not suffice for planarity.
An injective nonpolygonal arc drawing is excluded by the page's finite polygonal plane-graph convention
Statement refuted
Every injective continuous drawing of an abstract edge is a plane graph under this page's definition.
Facts & Assumptions
Given: Let be defined by and for .
A path is a continuous map from the unit interval (Paths, path-connected spaces and path components).
A plane graph uses finitely polygonal edge arcs that meet only at common endpoints (Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs).
Counterexample
The first coordinate of is , so is injective. For it is continuous, and shows continuity at . Thus [F1] makes it a continuous arc with distinct endpoints. It is not polygonal: the second coordinate vanishes at infinitely many points accumulating at and changes sign between them, whereas a finite union of line segments either has only finitely many such crossings of the horizontal axis or contains a nontrivial segment of that axis. The latter is impossible here because is not identically zero on any interval.
Use the image of as the drawing of the sole edge of a two-vertex abstract graph. The drawing is injective but its edge is not a polygonal arc in the sense of Polygonal arcs and polygons as non-self-intersecting finite unions of line segments in , so [L1] excludes this particular drawing from the page's class of plane graphs. This does not make the abstract one-edge graph nonplanar: drawing its edge as a straight segment gives a plane embedding.
Sources
Standard references
Recommended treatments; not extraction sources.
- R. Diestel, Graph Theory, 6th ed., Theorem 4.2.9
- R. Diestel, Graph Theory, 6th ed., Chapter 5
- R. Diestel, Graph Theory, 6th ed., Section 4.4
- J. A. Bondy and U. S. R. Murty, Graph Theory with Applications, plane duals
- Jeff Erickson, Planar Graphs
- R. Diestel, Graph Theory, 6th ed., Proposition 5.1.2
- R. Diestel, Graph Theory, 6th ed., Corollary 4.2.11