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.

A two-connected plane graph of order at least three is maximal exactly when every face is triangular

Statement

A two-connected plane graph with at least three vertices is maximal plane if and only if it is a plane triangulation (Maximal plane graphs, plane triangulations, and maximally planar abstract graphs). Two-connectivity is what makes every facial boundary a cycle (Every face of a two-connected plane graph is bounded by a cycle); Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs assumes no boundary walk is a cycle until a connectivity result proves it, and the polygonal Jordan argument below is about polygons, not about walks that may repeat a vertex. Facial walks and cycles use Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one and Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges.

Facts & Assumptions

Given: A plane graph G with at least three vertices.

[L1]

A polygon has exactly two regions, one bounded and one unbounded, and each has frontier the polygon (Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each).

[L2]

In a two-connected plane graph, every facial boundary walk is a cycle (Every face of a two-connected plane graph is bounded by a cycle).

[L3]

For a polygon P and a point x∉P, the parity of the transverse crossings of a general-position ray from x is independent of the ray, is constant on an open neighbourhood of x in the complement, and is therefore constant on each region of R2∖P (The parity of transverse ray crossings with a polygon is locally constant on its complement); such a ray exists because only finitely many directions meet a vertex or run along a segment (Every point off a polygon admits a ray meeting it transversely in finitely many nonvertex points).

[L4]

A region of the complement of a set is a connected component of that complement (Regions of the complement of a planar set and their frontiers), and every connected component of an open subset of Rn is open and polygonally connected (Every connected component of an open subset of Rn is open and polygonally connected).

[L5]

If the relative interior of an edge meets the frontier of a face, the whole edge lies in that frontier (Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one).

Proof

technique · direct
1.1

Let f be a face of G. By [L2] its boundary walk is a cycle C, drawn as a polygon. By [L5] every frontier point of f in the relative interior of an edge puts that whole edge in the frontier, so Fr⁡(f) is exactly the point set of C. Now f is connected and disjoint from C, so it lies in one region R0 of C [L1, L4]; f is open, and f‾∩R0=(f∪C)∩R0=f, so f is also closed in R0. A nonempty clopen subset of the connected R0 is all of it, so the face is one of the two regions of its own boundary cycle.

L1L2L4L5
1.2

If instead every face is triangular, the interior of any proposed new plane edge is connected and disjoint from the drawing, so it lies in one face, with both endpoints on that face's boundary [L4]. Those endpoints are already adjacent because that boundary is a triangle, so no missing edge can be added.

givenL4
1.3

The two regions of a polygon P carry different crossing parities. Fix a point p in the relative interior of one of the finitely many segments making up P, so p is not a vertex, and by [L6] take a disc D about p small enough to meet P only in that segment. Then D∖P is two open half-discs, each connected and disjoint from P and so contained in a single region [L4]; by [L1] there are exactly two regions and each has frontier P∋p, so each meets D, and therefore the two half-discs lie in different regions. Only finitely many directions fail to be in general position for P [L3], and only the two directions along the segment fail to meet it transversely, so some direction d avoids both finite sets. Put q=p−εd and q′=p+εd with ε small enough that both lie in D; since d is not along the segment, q and q′ lie in the two different half-discs, and [q,q′] meets P only at p. The ray from q in direction d is [q,q′] followed by the ray from q′ in direction d, so its crossing count is that of the latter plus the single transverse crossing at p. Both rays are in general position, so by [L3] those counts are the parities of q and of q′, which therefore differ; and parity is constant on each region [L3].

L1L3L4L6
2.1

Let u be a vertex of C. By [L6] a small enough disc D about u contains no other vertex and meets the drawing only in initial straight segments of the finitely many edges at u. Deleting those segments leaves finitely many open sectors of D, each connected and disjoint from the drawing and hence inside a single face [L4]. Since u∈Fr⁡(f), points of f lie in every disc about u, so one sector S satisfies S⊆f, and the straight radius from u into S meets the drawing only at u.

step 1.1L4L6
3.1

Let u≠v be vertices of C, with radii as in step 2.1 and inner endpoints u′,v′∈f. By step 1.1 f is a region, hence an open connected plane set and polygonally connected [L4], so a polygonal path joins u′ to v′ inside f; discarding the portion between the first and last visit to each repeated point makes it simple. Concatenating the two radii with it gives a polygonal arc from u to v meeting the drawing only at u and v. If u and v are nonadjacent in G, drawing the edge uv along that arc keeps the drawing plane, so G is not maximal plane.

step 1.1step 2.1L4
4.1

Suppose now G is maximal plane and some facial boundary cycle C has length at least four. Let u1,u2,u3,u4 occur in this cyclic order on C and let P1,P2 be the two u1–u3 subpaths of C, with u2 on P1 and u4 on P2. Both pairs are nonconsecutive on C, so by step 3.1 u1u3 and u2u4 are edges of G, neither an edge of C; write e,e′ for their arcs. They share no endpoint, so by [L6] the relative interior of each avoids C and the other, and both avoid f because they are part of the drawing. Hence J1=e∪P1 and J2=e∪P2 are polygons.

step 3.1L6assume-contra
5.1

From any point off C∪e there is a ray meeting that finite union of segments transversely in finitely many nonvertex points, by the finiteness count of [L3], and one such ray is in general position for C, e, J1 and J2 at once. Its crossings with J1 plus its crossings with J2 equal its crossings with C plus twice its crossings with e, so those three parities satisfy J1+J2=C modulo two at every point off C∪e. Now f avoids C, J1 and J2 and is connected, so all three parities are constant on it, say p1, p2 and p1+p2. The relative interior of e′ is connected and also avoids J1 and J2, so its J1- and J2-parities are constant. Its endpoint u4 is off J1 and lies in Fr⁡(f) by step 1.1, so a neighbourhood of u4 off J1 carrying a constant parity [L3] meets both f and that relative interior, forcing the J1-parity along e′ to be p1; symmetrically u2∉J2 forces the J2-parity to be p2. The C-parity along e′ is then p1+p2, that of f. The two regions of C carry different parities by step 1.3, so equal C-parity places the relative interior of e′ in the same region of C as f — which by step 1.1 is f itself. That is impossible for part of the drawing, so the assumption fails and every facial boundary cycle has length three.

step 1.1step 1.3step 4.1L3discharge-contradiction
6.1

The order assumption excludes the one- and two-vertex degeneracies, and steps 5.1 and 1.2 prove both directions.

step 5.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

36 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