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.
A plane graph has finitely many faces and exactly one unbounded face
Statement
Every plane graph (Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs) has finitely many faces, exactly one of which is unbounded. A subset of the plane is bounded here when both coordinate projections are bounded in the real sense of Lower bound, bounded below, bounded set. The proof adds finitely many vertices and edges by The principle of mathematical induction.
Facts & Assumptions
Given: A finite polygonal plane drawing.
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).
A polygonal arc does not separate the plane (The complement of a polygonal arc in is polygonally connected).
Proof
The finite union of bounded line segments lies in a sufficiently large rectangle. The exterior of that rectangle is connected and disjoint from the drawing, so it lies in one face; every unbounded face must meet the exterior and hence equals that face. Thus there is exactly one unbounded face.
Add the edge arcs one at a time. An arc that does not close a cycle can be exposed inside one existing face and, by [L2], does not split it. An arc that closes a polygon lies in one existing face and, by [L1], splits that face into exactly two. Isolated vertices likewise do not disconnect a plane region. Each addition therefore changes the face count by at most one.
Starting from the empty drawing with one face, finitely many additions yield finitely many faces, and step 1.1 identifies exactly one as unbounded.
Depends on
- Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs
- Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each
- The complement of a polygonal arc in $\mathbb R^2$ is polygonally connected
- The principle of mathematical induction
- Lower bound, bounded below, bounded set
Used by
- For a plane graph with c components, |V|-|E|+|F|=1+c, including the null graph Corollary
- Facial boundary walks of a connected plane graph sum to 2|E|, and if every such walk has length at least g then g|F|≤2|E| Lemma
- Every connected plane graph has a plane dual multigraph, and when that dual is simple the reciprocal embedding identifies the double dual with the original graph Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 43 results over 12 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., Chapter 4, Section 4.2 (standard reference, not scraped)