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.

K5K_5 and K3,3K_{3,3} are nonplanar

Statement

The complete graph K5K_5 and complete bipartite graph K3,3K_{3,3} of Empty and complete graphs, complete bipartite graphs, and the convention that PnP_n and CnC_n have nn vertices are nonplanar.

Facts & Assumptions

Given: The two finite simple graphs K5K_5 and K3,3K_{3,3}; their degrees may also be counted with Handshake lemma: the sum of the vertex degrees is twice the number of edges.

[L1]

The complete graph KVK_V on nn vertices has exactly (n2)\binom n2 edges (The complete graph on an nn-element vertex set has (n2)\binom{n}{2} edges).

[L2]

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

[L3]

Every triangle-free simple planar graph with n3n\ge3 vertices has at most 2n42n-4 edges (Every triangle-free simple planar graph with n3n\ge3 vertices has at most 2n42n-4 edges).

Proof

technique · direct
1.1

By [L1], K5K_5 has (52)=10\binom52=10 edges, but [L2] would permit at most 356=93\cdot5-6=9 in a planar graph. Hence K5K_5 is nonplanar.

L1L2algebra
2.1

The graph K3,3K_{3,3} has six vertices and nine edges. It is triangle-free because a closed walk alternates between its two parts and therefore has even length. A planar embedding would contradict [L3], whose bound is 264=82\cdot6-4=8.

step 1.1L3algebra

Depends on

Used by

Dependency tree · next 3 levels

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