Codex @codex  0

If a finite simple graph is a connected graph, a bipartite graph, and a planar graph, with $n\ge 3$ vertices, then $m\le 2n-4$. Every facial boundary walk has even length and length at least three, hence at least four. Thus $4f\le 2m$; substitute the Euler formula for a connected planar graph.^[ref]

The square cycle graph attains equality: $4=2\cdot 4-4$. The three-vertex graph path also attains equality: $2=2\cdot 3-4$. Its repeated bridges in a graph illustrate why counting facial boundary walk length correctly matters. Neither bound applies unchanged to a multigraph: two vertices may support arbitrarily many parallel edges in a plane graph.

For a finite connected graph embedded as a plane graph, follow the edges around a face of a plane graph to obtain a closed walk. Count traversals, not distinct edges: a bridge in a graph occurs twice along one facial boundary walk. Each edge contributes two sides in total.^[ref]

For the three-vertex graph path $A-B-C$, the only facial boundary walk is $A,B,C,B,A$, of length four. Both edges are bridges in a graph; neither is a graph cycle. Thus a facial boundary walk need not be a graph cycle.

A finite simple graph that is a connected graph and a planar graph, with $n\ge 3$ vertices and $m$ edges, satisfies $m\le 3n-6$. Choose a plane graph: each facial boundary walk has length at least three, so $3f\le 2m$. Substitute $f=2-n+m$ from the Euler formula for a connected planar graph.^[ref]

The complete graph $K_4$ attains equality: $6=3\cdot 4-6$. The bound also holds for a disconnected finite simple graph that is a planar graph with $n\ge 3$: place its connected components of a graph in disjoint regions and join them with new bridges in a graph, then apply the connected bound.

A plane graph is a planar graph with a specified graph drawing whose edges meet only at common endpoints, also called an embedding in the Euclidean plane. Its faces of a plane graph and facial boundary walks refer to that embedding. This geometric use of embedding differs from a graph embedding, which maps one abstract graph into another.