Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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 K5K_5 or K3,3K_{3,3} minor exactly when it has a subdivision of K5K_5 or K3,3K_{3,3} as a subgraph

Statement

A finite graph contains K5K_5 or K3,3K_{3,3} as a minor if and only if it contains a subdivision of K5K_5 or K3,3K_{3,3} 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 PnP_n and CnC_n have nn vertices.

Facts & Assumptions

Given: A finite graph GG containing at least one of the two stated obstructions in one of the two senses.

[F1]

A graph HH is a minor of GG 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

technique · direct
1.1

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.

F1
1.2

Conversely, contract every internally subdivided path of a K5K_5 or K3,3K_{3,3} subdivision to one edge. By [F1] this produces the corresponding graph as a minor.

F1
2.1

For a K3,3K_{3,3} 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 K3,3K_{3,3}.

step 1.1
3.1

In a K5K_5 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 cc for which every component of the deletion contains at most two incidences. If one contains two, the first edge from cc into it separates the incidences two from two. Otherwise each such component contains at most one, and the paths from cc to the incidences are internally disjoint, with zero-length arms for incidences at cc. Thus every four-marked branch tree has either a four-arm centre or a 22-22 edge. If every branch tree has a four-arm centre, those five centres and the model edges form a subdivision of K5K_5. Otherwise contract the two sides of a 22-22 edge to vertices a,ba,b, and contract the other four branch trees to vertices u1,u2,u3,u4u_1,u_2,u_3,u_4, labelled so aa meets u1,u2u_1,u_2 and bb meets u3,u4u_3,u_4. Then the bipartition {a,u3,u4}\{a,u_3,u_4\} and {b,u1,u2}\{b,u_1,u_2\} displays a K3,3K_{3,3} minor: abab, the four attachment edges at a,ba,b, and the four model edges uiuju_i u_j across the two pairs supply its nine edges. Step 2.1 converts this minor model to a K3,3K_{3,3} subdivision.

step 1.1step 2.1
4.1

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.

step 2.1step 3.1step 1.2

Depends on

Used by

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