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.
Every three-connected graph with no or minor is planar
Statement
Every three-connected finite graph with neither a nor a minor is planar. Minors and simple contraction are from Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors, connectivity from Vertex cuts, edge cuts, vertex connectivity and edge connectivity , with conventions for complete and one-vertex graphs, and the separation argument uses A finite graph on at least vertices is -connected if and only if every two vertices have internally disjoint paths and Menger's theorem: the finite directed and undirected arc, edge and nonadjacent-vertex forms. Plane-face control is supplied by Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each, Every face of a plane subgraph contains each face of the original graph that it meets and Every face of a two-connected plane graph is bounded by a cycle.
Facts & Assumptions
Given: A three-connected finite graph with neither forbidden minor.
Every three-connected simple graph with more than four vertices has an edge whose simple contraction remains three-connected (Every three-connected simple graph with more than four vertices has an edge whose simple contraction remains three-connected).
A graph has a or minor exactly when it contains a subdivision of one of them (A graph has a or minor exactly when it has a subdivision of or as a subgraph).
Proof
A three-connected graph of order four is , which has the usual plane drawing. Assume the result for smaller three-connected graphs that exclude the two minors.
If , choose from [L1]. The contraction remains three-connected and excludes the forbidden minors because the minor relation is transitive. It has a plane drawing by the induction hypothesis.
Let be the contracted vertex and delete it from the plane drawing of . Its incident faces merge into one face of , and every former neighbour of lies on that face boundary. Since is two-connected, the boundary is a cycle . Put and , both viewed on . Enumerate cyclically and let the intervening -arcs partition .
All vertices of lie on one intervening -arc. Otherwise two vertices of alternate on with two vertices of ; the paths through and , together with the two arcs of , form a subdivision of . The only remaining alternating degeneracy is three common neighbours of , which together with form a subdivision of . Both contradict [L2].
Delete from the drawing of the edges at corresponding only to , and regard as . The arc of containing bounds, together with the two adjacent -edges, a face of this drawing by polygonal separation and face containment. Place in that face, join it polygonally to all vertices of , and draw inside a small neighbourhood of . The arcs have disjoint interiors and recover a plane drawing of .
The base and contraction step prove the lemma for all finite orders.
Depends on
- A graph has a $K_5$ or $K_{3,3}$ minor exactly when it has a subdivision of $K_5$ or $K_{3,3}$ as a subgraph
- Every three-connected simple graph with more than four vertices has an edge whose simple contraction remains three-connected
- A finite graph on at least $k+1$ vertices is $k$-connected if and only if every two vertices have $k$ internally disjoint paths
- Vertex cuts, edge cuts, vertex connectivity $\kappa(G)$ and edge connectivity $\lambda(G)$, with conventions for complete and one-vertex graphs
- Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors
- Menger's theorem: the finite directed and undirected arc, edge and nonadjacent-vertex forms
- Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each
- Every face of a plane subgraph contains each face of the original graph that it meets
- Every face of a two-connected plane graph is bounded by a cycle
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 63 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- R. Diestel, Graph Theory, 6th ed., Lemma 4.4.3 (standard reference, not scraped)