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.
Every face of a two-connected plane graph is bounded by a cycle
Statement
In a two-connected plane graph (Vertex cuts, edge cuts, vertex connectivity and edge connectivity , with conventions for complete and one-vertex graphs), every facial boundary walk is a cycle (Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges). Edge incidence is supplied by Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one.
Facts & Assumptions
Given: A two-connected plane graph and a face with its closed boundary walk.
For , a finite graph on at least vertices is -connected if and only if every two distinct vertices are joined by at least internally vertex-disjoint paths (A finite graph on at least vertices is -connected if and only if every two vertices have internally disjoint paths).
Proof
Suppose the facial boundary walk repeats a vertex before returning to its start. The two portions between consecutive occurrences leave through different local sectors of the face.
Vertices or edges incident with those two portions lie in different components of : a path between them avoiding would, together with boundary subpaths, cross the face boundary in the plane. Thus is a cut vertex.
By [L1], two-connectivity supplies two internally vertex-disjoint paths between vertices chosen on the two portions, so deletion of cannot separate them. This contradicts step 2.1. The boundary walk has no repeated vertex and is therefore a cycle.
Depends on
- Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one
- A finite graph on at least $k+1$ vertices is $k$-connected if and only if every two vertices have $k$ internally disjoint paths
- Vertex cuts, edge cuts, vertex connectivity $\kappa(G)$ and edge connectivity $\lambda(G)$, with conventions for complete and one-vertex graphs
- Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges
Used by
- Every edge-maximal graph of order at least four with no subdivision of K₅ or K_3,3 is three-connected Lemma
- Every three-connected graph with no K₅ or K_3,3 minor is planar Lemma
- 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
- A two-connected plane graph of order at least three is maximal exactly when every face is triangular Proposition
- In a three-connected plane graph, face boundaries are exactly the induced cycles whose deletion leaves the graph connected Proposition
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 37 results over 14 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., Proposition 4.2.6 (standard reference, not scraped)