Alphabeta MathHow 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.
Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one
Statement
In a plane graph (Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs), if the relative interior of an edge meets the frontier of a face, then the whole edge lies in that frontier. An edge on a cycle is incident with two distinct faces, one on each local side. A bridge is incident with one face on both local sides and is therefore traversed twice in that face's boundary walk. Edge deletion is as in Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors, and the bridge cases use the arc-complement fact The complement of a polygonal arc in is polygonally connected.
Facts & Assumptions
Given: A plane graph and an edge .
A polygon has exactly two regions, each with frontier the polygon (Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each).
An edge is a bridge if and only if it lies on no cycle (An edge of a finite graph is a bridge if and only if it lies on no cycle).
Proof
A sufficiently small rectangle about any interior point of meets the drawing only in a straight subsegment of . Its two open half-rectangles lie in faces. Sliding overlapping rectangles along the compact edge interior shows that each local side remains in one face until an endpoint is reached; hence frontier membership propagates along the entire edge.
If lies on a cycle , [L1] gives two regions of the polygonal image of . The two local sides of lie in different such regions and cannot be joined in the complement of the full drawing, so they belong to two distinct faces of .
If lies on no cycle, [L2] makes it a bridge. Delete its interior. The two local sides can be joined by a small detour around either endpoint through the component complement, because no second endpoint path closes a polygon. They therefore lie in one face, and a boundary traversal encounters once in each direction.
Depends on
- Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs
- Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each
- The complement of a polygonal arc in $\mathbb R^2$ is polygonally connected
- An edge of a finite graph is a bridge if and only if it lies on no cycle
- Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors
Used by
- For a plane graph with c components, |V|-|E|+|F|=1+c, including the null graph Corollary
- The plane dual multigraph, with a vertex for each face and one crossing edge for each primal edge Definition
- Every edge-maximal graph of order at least four with no subdivision of K₅ or K_3,3 is three-connected Lemma
- Every plane triangulation with at least three vertices is connected Lemma
- Facial boundary walks of a connected plane graph sum to 2|E|, and if every such walk has length at least g then g|F|≤2|E| Lemma
- If two distinct faces of a connected plane graph have the same boundary subgraph, then the graph is a cycle Lemma
- A two-connected plane graph of order at least three is maximal exactly when every face is triangular Proposition
- Every face of a two-connected plane graph is bounded by a cycle Proposition
- Every plane forest has exactly one face Proposition
- Euler's formula |V|-|E|+|F|=2 for every connected plane graph Theorem
- 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 Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 38 results over 10 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., Lemmas 4.2.2-4.2.3 (standard reference, not scraped)