Alphabeta Math
CorollaryStatement: 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 nonnull simple planar graph has a vertex of degree at most five

Statement

Every nonnull finite simple planar graph has a vertex of degree at most five, where degree is Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree.

Facts & Assumptions

Given: A nonnull simple planar graph GG with nn vertices and mm edges.

[L1]

Every simple planar graph with n≥3n\ge3 vertices has at most 3n−63n-6 edges (Every simple planar graph with n≥3n\ge3 vertices has at most 3n−63n-6 edges, with equality for every plane triangulation).

[L2]

∑v∈Vdeg⁡G(v)=2∣E∣\sum_{v\in V}\deg_G(v)=2|E| (Handshake lemma: the sum of the vertex degrees is twice the number of edges).

Proof

technique · contradiction
1.1

For n=1n=1 or n=2n=2, some vertex has degree at most one, hence at most five. Assume n≥3n\ge3.

given
2.1

Suppose every vertex had degree at least six. Then [L2] gives 2m≥6n2m\ge6n, so m≥3nm\ge3n, while [L1] gives m≤3n−6m\le3n-6. This contradiction proves that some degree is at most five.

step 1.1assume-contraL1L2discharge-contradiction∎

Depends on

Used by

Dependency tree · next 3 levels

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