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.

Every three-connected graph with no K5K_5 or K3,3K_{3,3} minor is planar

Statement

Facts & Assumptions

Given: A three-connected finite graph GG with neither forbidden minor.

[L1]

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).

[L2]

A graph has a K5K_5 or K3,3K_{3,3} minor exactly when it contains a subdivision of one of them (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).

Proof

technique · induction
1.1

A three-connected graph of order four is K4K_4, which has the usual plane drawing. Assume the result for smaller three-connected graphs that exclude the two minors.

baseL2
1.2

If G>4|G|>4, choose xyxy from [L1]. The contraction H=G/xyH=G/xy remains three-connected and excludes the forbidden minors because the minor relation is transitive. It has a plane drawing by the induction hypothesis.

ihL1
2.1

Let vv be the contracted vertex and delete it from the plane drawing of HH. Its incident faces merge into one face of HvH-v, and every former neighbour of vv lies on that face boundary. Since HvH-v is two-connected, the boundary is a cycle CC. Put X=NG(x){y}X=N_G(x)\setminus\{y\} and Y=NG(y){x}Y=N_G(y)\setminus\{x\}, both viewed on CC. Enumerate XX cyclically and let the intervening XX-arcs partition CC.

step 1.2
3.1

All vertices of YY lie on one intervening XX-arc. Otherwise two vertices of YY alternate on CC with two vertices of XX; the paths through xx and yy, together with the two arcs of CC, form a subdivision of K3,3K_{3,3}. The only remaining alternating degeneracy is three common neighbours of x,yx,y, which together with x,yx,y form a subdivision of K5K_5. Both contradict [L2].

step 2.1L2
4.1

Delete from the drawing of HH the edges at vv corresponding only to YXY\setminus X, and regard vv as xx. The arc of CC containing YY bounds, together with the two adjacent xx-edges, a face of this drawing by polygonal separation and face containment. Place yy in that face, join it polygonally to all vertices of YY, and draw xyxy inside a small neighbourhood of xx. The arcs have disjoint interiors and recover a plane drawing of GG.

step 3.1construct
5.1

The base and contraction step prove the lemma for all finite orders.

step 1.1step 4.1discharge-induction

Depends on

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