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.
A graph has a or minor exactly when it has a subdivision of or as a subgraph
Statement
A finite graph contains or as a minor if and only if it contains a subdivision of or as a subgraph. Minors and subdivisions are those of Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors, and the two standard graphs are from Empty and complete graphs, complete bipartite graphs, and the convention that and have vertices.
Facts & Assumptions
Given: A finite graph containing at least one of the two stated obstructions in one of the two senses.
A graph is a minor of when it can be obtained by vertex deletions, edge deletions and edge contractions (Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors).
Proof
Choose a minor model with the fewest total vertices in its pairwise disjoint connected branch sets, and retain one model edge for each edge of the obstruction. Each branch set is then the minimal tree joining the endpoints of its incident model edges; otherwise a leaf or surplus edge could be removed. Attachment endpoints are allowed to coincide.
Conversely, contract every internally subdivided path of a or subdivision to one edge. By [F1] this produces the corresponding graph as a minor.
For a model, each branch tree carries at most three attachment incidences. A minimal tree joining at most three attachment vertices has a vertex from which internally disjoint arms reach all three incidences (zero-length arms are allowed when incidences coincide). Taking these six centres as branch vertices and adjoining the model edges therefore gives a subdivision of .
In a model, inspect the minimal subtree carrying the four attachment incidences in each branch tree, putting one unit of weight at each incidence even when several coincide. Starting at any vertex, move into a component of its deletion containing more than two incidences whenever such a component exists. This strictly advances through the finite minimal subtree, so it stops at a vertex for which every component of the deletion contains at most two incidences. If one contains two, the first edge from into it separates the incidences two from two. Otherwise each such component contains at most one, and the paths from to the incidences are internally disjoint, with zero-length arms for incidences at . Thus every four-marked branch tree has either a four-arm centre or a - edge. If every branch tree has a four-arm centre, those five centres and the model edges form a subdivision of . Otherwise contract the two sides of a - edge to vertices , and contract the other four branch trees to vertices , labelled so meets and meets . Then the bipartition and displays a minor: , the four attachment edges at , and the four model edges across the two pairs supply its nine edges. Step 2.1 converts this minor model to a subdivision.
Steps 2.1 and 3.1 prove the minor-to-subdivision implication for the union of the two obstructions, and step 1.2 proves the converse.
Depends on
Used by
- Every edge-maximal graph of order at least four with no subdivision of K₅ or K_3,3 is three-connected Lemma
- Every three-connected graph with no K₅ or K_3,3 minor is planar 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
- Kuratowski–Wagner theorem: a finite graph is planar exactly when it has neither a K₅ nor a K_3,3 minor, equivalently neither subdivision Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 9 results over 5 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.2 (standard reference, not scraped)