LemmaStatement: 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.

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|\le2|E|$

Statement

Let $G$ be a connected plane graph, and write $\ell(f)$ for the length of the facial boundary walk of $f$ . Then

$\sum_{f\in F(G)}\ell(f)=2|E(G)|.$

Consequently, if every facial boundary walk has length at least a positive natural $g$ , then

$g|F(G)|\le2|E(G)|.$

Facial walks count a bridge twice by Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one. Cyclic boundary terminology and girth use Every face of a two-connected plane graph is bounded by a cycle and Graph distance within a component, eccentricity, diameter and girth, including the acyclic convention, and finite sums use The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form.

Facts & Assumptions

Given: Such a graph $G$ and lower bound $g$ .

[L1]

Double counting gives the same finite incidence total by summing either its row fibres or its column fibres (Double counting: $\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^y\rvert$ for a relation between finite sets).

[L2]

Each edge contributes two local face sides; a bridge contributes twice to its single facial boundary walk (Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one).

[L3]

Every plane graph has finitely many faces, exactly one of which is unbounded (A plane graph has finitely many faces and exactly one unbounded face).

Proof

technique · direct

1.1

By [L3], $F(G)$ is finite. Count incidences between faces and local edge sides. By [L2] every edge supplies exactly two sides, while the fibre over a face has size equal to its boundary-walk length. Thus [L1] gives $\sum_{f\in F}\ell(f)=2|E|$ .

L1L2L3

2.1

Since each $\ell(f)\ge g$ , summing these inequalities yields $g|F|\le\sum_f\ell(f)=2|E|$ .

step 1.1L2algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 79 results over 22 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., Chapter 4, Section 4.2 (standard reference, not scraped)
R. Grassl and O. Levin, Exploring Combinatorial Mathematics, Sections 3.3-3.4 (standard reference, not scraped)

Facial boundary walks of a connected plane graph sum to 2∣E∣2|E|2∣E∣, and if every such walk has length at least ggg then g∣F∣≤2∣E∣g|F|\le2|E|g∣F∣≤2∣E∣