Alphabeta MathHow 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.
Euler's formula for every connected plane graph
Statement
If a connected plane graph has vertex, edge and face sets (Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs), then
Deletion is as in Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors, the tree boundary case uses Every plane forest has exactly one face and Deleting any edge of a tree separates it into exactly two tree components, and the finite induction is The principle of mathematical induction.
Facts & Assumptions
Given: A connected plane graph .
A finite graph is connected if and only if it has a spanning tree (A finite graph is connected if and only if it has a spanning tree).
A cycle edge borders two faces and a bridge borders one face (Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one).
Proof
Choose a spanning tree by [L1]. It has all vertices and edges, and its plane drawing has one face by the forest proposition. Hence .
Add the edges of in their fixed embedding. Each added edge joins vertices already connected in , so it closes a cycle. By [L2] it splits one old face into two: the edge count and face count each increase by one, while the vertex count is unchanged. Thus the Euler expression remains invariant.
Equivalently, deleting a cycle edge from a connected plane graph merges its two incident faces and decreases both and by one. Deleting a bridge would disconnect the graph and is not used in this connected induction.
Starting from and adding all remaining edges yields , so the invariant value from step 1.1 is for .
Depends on
- Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs
- Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one
- Every plane forest has exactly one face
- A finite graph is connected if and only if it has a spanning tree
- Deleting any edge of a tree separates it into exactly two tree components
- Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors
- The principle of mathematical induction
Used by
- Every simple planar graph with n≥3 vertices has at most 3n-6 edges, with equality for every plane triangulation Corollary
- Every triangle-free simple planar graph with n≥3 vertices has at most 2n-4 edges Corollary
- For a plane graph with c components, |V|-|E|+|F|=1+c, including the null graph Corollary
- Euler's formula checked on a plane tree, a cycle, and the four-face embedding of K₄ Example
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 54 results over 16 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., Theorem 4.2.9 (standard reference, not scraped)
- R. Grassl and O. Levin, Exploring Combinatorial Mathematics, Theorem 3.3.1 (standard reference, not scraped)