Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Planar graphs have at most 3v − 6 edges`

groundedproofs/Lax909950Proofs/EdgeDensity.lean · lax-909950

What this proof establishes

thm✓Lax909950.EdgeDensity

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 1 of this submission's paper

Description

For a connected graph with a cycle, every face is a side face of the edges of a cycle, hence of at least 33 edges; each edge has at most 22 side faces, so 3f≤2e3f \leq 2e, and Euler's formula v−e+f=2v - e + f = 2 gives e≤3v−6e \leq 3v - 6. Trees have v−1≤3v−6v - 1 \leq 3v - 6 edges. Disconnected graphs split into a component and the rest, and the bound is superadditive.