LemmaStatement: AI-adaptedProof: 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.

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

Statement

Let $v_1,\ldots,v_5$ be the five distinct neighbours of a vertex $v$ in cyclic order in a plane graph (Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs), and suppose they have distinct colours $1,\ldots,5$ . In the coloured graph with $v$ deleted, an alternating $1$ - $3$ Kempe path from $v_1$ to $v_3$ and an alternating $2$ - $4$ Kempe path from $v_2$ to $v_4$ cannot both exist (Kempe chains as connected components induced by two colour classes). Paths use Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges.

Facts & Assumptions

Given: The plane configuration and proper colouring in the Statement.

[L1]

A polygon has exactly two regions, each with frontier the polygon (Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each).

[F1]

A path is a walk in which the vertices are distinct (Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges).

Proof

technique · contradiction

1.1

Suppose both paths exist. Choose a simple $1$ - $3$ path $P$ from $v_1$ to $v_3$ . Together with the plane edges $vv_1$ and $vv_3$ , it forms a polygonal cycle $C$ .

assume-contraF1

2.1

The cyclic order at $v$ places $v_2$ and $v_4$ on opposite local sides of $C$ . By [L1] they lie in different regions of $\mathbb R^2\setminus C$ , so every plane path between them meets $C$ . In particular the supposed $2$ - $4$ Kempe path meets $P$ or one of the two edges incident with $v$ .

step 1.1L1F1

3.1

The $2$ - $4$ path avoids $v$ and has only colours $2,4$ , whereas $P$ has only colours $1,3$ ; proper plane edges cannot cross in their interiors and the two paths cannot share a vertex. This contradicts step 2.1, so both Kempe connections cannot occur.

step 2.1discharge-contradiction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 34 results over 8 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., Proposition 5.1.2 (standard reference, not scraped)