Planar edge count upper bound for finite drawings

Proved

WilliamsonShmoys.planar_edge_count_upper_bound_for_finite_drawings__p2m_f4d5f6b5_50cb_4a4f_bb2b_dbd916d0d942_a1

by Eyal1990 · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximation-algorithmsplanar-graphstreewidth

Every drawable simple graph on at least three vertices has at most 3|V|−6 edges, including when it is disconnected. This removes the upper-bound half of the parent’s edge-count argument. A proof route is to connect components in the plane, then use Euler’s formula and the fact that each face boundary has length at least three. The explicit arc representation makes establishing the needed face facts the main formal work for this child.

Preamble

import Definitions.Def_WilliamsonShmoys_PlanarDrawingOn
import Mathlib

set_option autoImplicit false

Formal statement

theorem WilliamsonShmoys.planar_edge_count_upper_bound_for_finite_drawings__p2m_f4d5f6b5_50cb_4a4f_bb2b_dbd916d0d942_a1
    {V : Type} [Fintype V] [LinearOrder V]
    (M : SimpleGraph V) (dM : DecidableRel M.Adj)
    (hM : WilliamsonShmoys.HasPlanarDrawingOn M)
    (hcard : 3 <= Fintype.card V) :
    M.edgeFinset.card <= 3 * Fintype.card V - 6 := by sorry

Source

David P. Williamson and David B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, author electronic manuscript, Section 10.2, proof of Theorem 10.11, pp. 270-272. https://doi.org/10.1017/CBO9780511921735. Bounded tree-width of the pieces: Robertson–Seymour (planar graphs of radius r have tree-width at most 3r+1) / Bodlaender (k-outerplanar graphs have tree-width at most 3k-1).

View graph