ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck 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 degree-five vertex is inserted into a plane graph after one explicit Kempe-chain colour swap

Example

One Kempe swap extends a five-colouring across the centre of a plane wheel with five rim vertices.

Facts & Assumptions

Given: Let $v_{1}, v_{2}, v_{3}, v_{4}, v_{5}$ occur in this cyclic order on a plane $5$ -cycle. Colour $v_{i}$ with colour $i$ , and plan to insert a vertex $v$ inside the cycle adjacent to every $v_{i}$ .

[L1]

Swapping two colours on one Kempe component preserves a proper colouring (Swapping the two colours on one Kempe component preserves a proper colouring).

[L2]

The alternating Kempe connections between cyclic neighbours $v_{1}, v_{3}$ and $v_{2}, v_{4}$ cannot both occur (For five cyclically ordered neighbours of a plane vertex, alternating Kempe paths between the first and third and between the second and fourth cannot both occur).

Verification

technique · constructive

1.1

Before $v$ is inserted, its five prospective neighbours use all five colours. In the subgraph induced by colours $1$ and $3$ , both $v_{1}$ and $v_{3}$ are isolated: their two cycle neighbours have colours $2, 5$ and $2, 4$ , respectively. In particular there is no alternating $1$ - $3$ path between them, consistently with [L2].

L2construct

2.1

Swap colours $1$ and $3$ on the Kempe component ${v_{1}}$ . The colouring remains proper by [L1]; now both $v_{1}$ and $v_{3}$ have colour $3$ , but they are nonadjacent, and no rim vertex has colour $1$ . Give the inserted centre $v$ colour $1$ . Every spoke then has differently coloured endpoints, producing an explicit five-colouring of the plane wheel and illustrating the swap used in Five colour theorem: every planar graph has chromatic number at most five.

L1step 1.1discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

R. Diestel, Graph Theory, 6th ed., Proposition 5.1.2 (standard reference, not scraped)