Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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 G with n vertices and m edges.

[L1]

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

[L2]

∑v∈Vdeg⁡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=1 or n=2, some vertex has degree at most one, hence at most five. Assume n≥3.

given
2.1

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

step 1.1assume-contraL1L2discharge-contradiction∎

Depends on

Used by

Dependency tree · two levels

12 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