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.
In a three-connected plane graph, face boundaries are exactly the induced cycles whose deletion leaves the graph connected
Statement
Let be a three-connected plane graph. A subgraph is the boundary of a face if and only if is an induced cycle (Subgraphs, induced subgraphs and spanning subgraphs) and is connected or empty (Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors).
Facts & Assumptions
Given: A three-connected plane graph and a cycle .
Every face of a two-connected plane graph is bounded by a cycle (Every face of a two-connected plane graph is bounded by a cycle).
In a three-connected graph, every two distinct vertices are joined by at least three internally vertex-disjoint paths (A finite graph on at least vertices is -connected if and only if every two vertices have internally disjoint paths).
A polygon has exactly two complementary regions and is the frontier of each (Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each).
Proof
A facial boundary is a cycle by [L1]. It has no chord : the chord lies on the nonfacial side, and the chord together with each of the two - arcs of is a polygon by [L3]. These two polygons bound disjoint subregions of the nonfacial side. Since the facial side contains no graph edge, a path from an internal vertex of one - arc to an internal vertex of the other, avoiding , would have to cross the chord. Thus would be a vertex cut, contrary to three-connectivity and [L2]. Hence is induced.
Conversely, let be induced and suppose is connected or empty. If is not facial, both complementary regions from [L3] contain graph material. Inducedness rules out a chord as that material, so each side contains a vertex outside . When is connected, a path in it joins vertices on the two sides and must cross , contradicting the plane embedding. If is empty, the drawing consists only of , and both sides are faces. Thus is facial.
Suppose were disconnected, and let be one of its components. Every component has at least three neighbours on , since one or two such neighbours would be a vertex cut contradicting [L2]. Because bounds a face, every component lies in the closed complementary side of , which [L3] presents as a region bounded by . Let with be the attachments of in cyclic order on , and let be a spanning tree of together with one edge to each . Then is connected, lies in that side, and meets exactly in , so by [L3] the set divides the side into exactly regions, the th bounded by the arc of from to carrying no further attachment of together with two paths of . Every other component is connected and meets neither nor , so each lies inside a single one of those open regions; choose one, say the th, that contains a component, and put and . This is where the alternation of attachments is not enough: two components may share all three of their attachments, in which case no four attachments alternate, and the region argument rather than the crossing argument is what confines them. Let consist of the open arc of strictly between and together with every component lying in the th region. Distinct components of are non-adjacent, and each component in that region has all of its neighbours on the closed arc from to , while has no attachment strictly inside that arc. A vertex of the open arc has no neighbour elsewhere on , because step 1.1 has already shown induced, so has no chord; and any component adjacent to such a vertex has an attachment strictly inside the arc, hence lies in the th region and is already in . Hence the only neighbours of outside are and , so is a vertex cut separating from , contradicting [L2]. Thus is connected when nonempty.
Steps 1.1 and 2.1 prove the forward implication, and step 1.2 proves the reverse, including the empty-deletion boundary.
Depends on
- Every face of a two-connected plane graph is bounded by a cycle
- A finite graph on at least $k+1$ vertices is $k$-connected if and only if every two vertices have $k$ internally disjoint paths
- Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each
- Subgraphs, induced subgraphs and spanning subgraphs
- Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 40 results over 9 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.7 (standard reference, not scraped)