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 simple graph with more than four vertices has an edge whose simple contraction remains three-connected

Statement

Facts & Assumptions

Given: A three-connected simple graph GK4G\ne K_4.

[L1]

A finite graph on at least four vertices is three-connected exactly when every two distinct vertices are joined by at least three internally vertex-disjoint paths (A finite graph on at least k+1k+1 vertices is kk-connected if and only if every two vertices have kk internally disjoint paths).

[F1]

Simple contraction deletes resulting loops and merges parallel edges (Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors).

Proof

technique · contradiction
1.1

Suppose no edge is contractible. For every edge xyxy, the graph G/xyG/xy has a separator of at most two vertices. Three-connectivity of GG forces that separator to have the form {vxy,z}\{v_{xy},z\}, where vxyv_{xy} is the contracted vertex; lifting it shows that {x,y,z}\{x,y,z\} separates GG. Every member of this triple has a neighbour in every component of its deletion, since no proper subset can separate a three-connected graph.

assume-contraL1F1
2.1

Among all choices of xy,zxy,z and a component CC of G{x,y,z}G-\{x,y,z\}, choose one with C|C| least, and choose a neighbour vCv\in C of zz. The assumed noncontractibility of zvzv similarly gives a vertex ww such that {z,v,w}\{z,v,w\} separates GG, with every member adjacent into every component of its deletion.

step 1.1
3.1

Because xx and yy are adjacent, some component DD of G{z,v,w}G-\{z,v,w\} avoids both xx and yy. The separator-neighbour property puts a neighbour of vv in DD; since vCv\in C and DD avoids x,y,zx,y,z, that neighbour and every vertex of DD reached without the new separator lie in CC. Moreover vDv\notin D, so DD is a proper nonempty subset of CC. The triple {z,v,w}\{z,v,w\} with component DD is therefore a smaller choice than CC.

step 2.1L1
4.1

Step 3.1 contradicts the minimality in step 2.1. Hence some edge has a simple contraction that remains three-connected.

step 2.1step 3.1discharge-contradiction

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 46 results over 21 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