Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 GG be a three-connected plane graph. A subgraph CC is the boundary of a face if and only if CC is an induced cycle (Subgraphs, induced subgraphs and spanning subgraphs) and GV(C)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 GG and a cycle CC.

[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+1k+1 vertices is kk-connected if and only if every two vertices have kk 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 CC is a cycle by [L1]. It has no chord xyxy: the chord lies on the nonfacial side, and the chord together with each of the two xx-yy arcs of CC 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 xx-yy arc to an internal vertex of the other, avoiding x,yx,y, would have to cross the chord. Thus {x,y}\{x,y\} would be a vertex cut, contrary to three-connectivity and [L2]. Hence CC is induced.

L1L2L3
1.2

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

L3
2.1

Suppose GV(C)G-V(C) were disconnected, and let D1D_1 be one of its components. Every component has at least three neighbours on CC, since one or two such neighbours would be a vertex cut contradicting [L2]. Because CC bounds a face, every component lies in the closed complementary side of CC, which [L3] presents as a region bounded by CC. Let a1,,aka_1,\ldots,a_k with k3k\ge3 be the attachments of D1D_1 in cyclic order on CC, and let SS be a spanning tree of D1D_1 together with one edge to each aia_i. Then SS is connected, lies in that side, and meets CC exactly in {a1,,ak}\{a_1,\ldots,a_k\}, so by [L3] the set SCS\cup C divides the side into exactly kk regions, the iith bounded by the arc of CC from aia_i to ai+1a_{i+1} carrying no further attachment of D1D_1 together with two paths of SS. Every other component is connected and meets neither SS nor CC, so each lies inside a single one of those open regions; choose one, say the iith, that contains a component, and put x:=aix:=a_i and y:=ai+1y:=a_{i+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 UU consist of the open arc of CC strictly between xx and yy together with every component lying in the iith region. Distinct components of GV(C)G-V(C) are non-adjacent, and each component in that region has all of its neighbours on the closed arc from xx to yy, while D1D_1 has no attachment strictly inside that arc. A vertex of the open arc has no neighbour elsewhere on CC, because step 1.1 has already shown CC induced, so CC has no chord; and any component adjacent to such a vertex has an attachment strictly inside the arc, hence lies in the iith region and is already in UU. Hence the only neighbours of UU outside UU are xx and yy, so {x,y}\{x,y\} is a vertex cut separating UU from D1D_1, contradicting [L2]. Thus GV(C)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 · 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