Alphabeta Math
TheoremStatement: 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.

Every connected plane graph has a plane dual multigraph, and when that dual is simple the reciprocal embedding identifies the double dual with the original graph

Statement

Every connected plane graph GG admits a polygonal plane embedding of its dual multigraph The plane dual multigraph, with a vertex for each face and one crossing edge for each primal edge in which each dual edge crosses its corresponding primal edge exactly once and crosses no other primal or dual edge. In this reciprocal embedding, if G∗G^* is itself simple — equivalently, if GG has no bridge and no two faces share more than one edge — then G∗G^* is a plane graph in the sense of Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs and (G∗)∗(G^*)^* is isomorphic to GG in the sense of Graph isomorphisms, automorphisms and graph complements. The simplicity hypothesis is necessary and not a convenience: a plane graph is a finite simple graph here, while The plane dual multigraph, with a vertex for each face and one crossing edge for each primal edge may produce loops and parallel edges, so the double dual is otherwise not formed at all. For G=K2G=K_2 the single edge is a bridge and G∗G^* is one vertex with a loop, which is not a plane graph and has no dual under these definitions. Face finiteness is A plane graph has finitely many faces and exactly one unbounded face, local incidence is Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one, and polygonal separation is Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each.

Facts & Assumptions

Given: A connected plane graph GG.

[F1]

An edge assigned one endpoint is a loop, and distinct edges assigned the same endpoint set are parallel edges (Multigraphs, loops and directed graphs as variants distinct from the default finite simple graph).

[L1]

Each primal edge has two local face sides, possibly belonging to the same face when it is a bridge (Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one).

Proof

technique · constructive
1.1

Choose one point pfp_f in each of the finitely many faces. Around every primal vertex take a small disk, and around each edge interior take a thin polygonal corridor; choose these finitely many neighbourhoods mutually disjoint except at their prescribed incidences. In each face, connect its point polygonally inside that face to the appropriate side of every incident edge corridor.

L1construct
2.1

For each primal edge ee, join the two incident face paths across its corridor by one transverse segment through ee. These arcs meet no other primal edge, and the corridors and within-face paths can be chosen successively disjoint. If both sides of ee are the same face, the arc closes to a loop; repeated face pairs yield parallel edges as allowed by [F1]. Thus the resulting drawing is a plane embedding of G∗G^*.

step 1.1F1L1
3.1

In the reciprocal drawing, a small punctured neighbourhood of each primal vertex is one face of G∗G^*, and every dual face arises this way: walking around a dual face crosses precisely the primal edges incident with that vertex. The dual of e∗e^* crosses it in the original corridor and corresponds canonically to ee.

step 1.1step 2.1
4.1

Map each primal vertex to its surrounding dual face and each primal edge ee to (e∗)∗(e^*)^*. Step 3.1 makes these maps bijective and incidence preserving, so they define an isomorphism G≅(G∗)∗G\cong(G^*)^*.

step 3.1discharge-construct∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 45 results over 12 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