Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

In a three-connected plane graph, face boundaries are exactly the induced cycles whose deletion leaves the graph connected

Statement

Let G be a three-connected plane graph. A subgraph C is the boundary of a face if and only if C is an induced cycle (Subgraphs, induced subgraphs and spanning subgraphs) and G−V(C) is connected or empty (Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors).

Facts & Assumptions

Given: A three-connected plane graph G and a cycle C.

[L1]

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).

[L2]

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 k+1 vertices is k-connected if and only if every two vertices have k internally disjoint paths).

[L3]

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

technique · direct
1.1

A facial boundary C is a cycle by [L1]. It has no chord xy: the chord lies on the nonfacial side, and the chord together with each of the two x-y arcs of C 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 x-y arc to an internal vertex of the other, avoiding x,y, would have to cross the chord. Thus {x,y} would be a vertex cut, contrary to three-connectivity and [L2]. Hence C is induced.

L1L2L3
1.2

Conversely, let C be induced and suppose G−V(C) is connected or empty. If C 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 C. When G−V(C) is connected, a path in it joins vertices on the two sides and must cross C, contradicting the plane embedding. If G−V(C) is empty, the drawing consists only of C, and both sides are faces. Thus C is facial.

L3
2.1

Suppose G−V(C) were disconnected, and let D1 be one of its components. Every component has at least three neighbours on C, since one or two such neighbours would be a vertex cut contradicting [L2]. Because C bounds a face, every component lies in the closed complementary side of C, which [L3] presents as a region bounded by C. Let a1,…,ak with k≥3 be the attachments of D1 in cyclic order on C, and let S be a spanning tree of D1 together with one edge to each ai. Then S is connected, lies in that side, and meets C exactly in {a1,…,ak}, so by [L3] the set S∪C divides the side into exactly k regions, the ith bounded by the arc of C from ai to ai+1 carrying no further attachment of D1 together with two paths of S. Every other component is connected and meets neither S nor C, so each lies inside a single one of those open regions; choose one, say the ith, that contains a component, and put x:=ai and y:=ai+1. 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 U consist of the open arc of C strictly between x and y together with every component lying in the ith region. Distinct components of G−V(C) are non-adjacent, and each component in that region has all of its neighbours on the closed arc from x to y, while D1 has no attachment strictly inside that arc. A vertex of the open arc has no neighbour elsewhere on C, because step 1.1 has already shown C induced, so C has no chord; and any component adjacent to such a vertex has an attachment strictly inside the arc, hence lies in the ith region and is already in U. Hence the only neighbours of U outside U are x and y, so {x,y} is a vertex cut separating U from D1, contradicting [L2]. Thus G−V(C) is connected when nonempty.

step 1.1L2L3
3.1

Steps 1.1 and 2.1 prove the forward implication, and step 1.2 proves the reverse, including the empty-deletion boundary.

step 1.1step 2.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources