Edge count of a maximal drawable graph

Proved

WilliamsonShmoys.triangulation_2a27a388_e06b_4db0_bfe8_7a93ec4c9c7f_maximal_edge_count

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

approximation-algorithmsplanar-graphstreewidth

An inclusion-maximal graph with a crossing-free drawing on at least three vertices has exactly three times the number of vertices minus six edges. This removes the topological and Euler-counting work from the parent. A proof route is to use the drawing arcs as a plane embedding, show maximality rules out disconnected components and nontriangular faces by adding an edge inside a face, and then combine Euler’s formula with the fact that each triangular face contributes three edge incidences and each edge borders two face sides. The lower bound on the number of vertices is essential: on fewer vertices, maximal drawable graphs need not have this edge count. Formalizing this plane-embedding argument from the supplied arc predicate remains the core obligation.

Preamble

import Definitions.Def_WilliamsonShmoys_PlanarDrawingOn

set_option autoImplicit false

Formal statement

theorem WilliamsonShmoys.triangulation_2a27a388_e06b_4db0_bfe8_7a93ec4c9c7f_maximal_edge_count
    {V : Type} [Fintype V] [LinearOrder V]
    (K : SimpleGraph V)
    (hV : 3 <= Fintype.card V)
    (hK : WilliamsonShmoys.HasPlanarDrawingOn K)
    (hmax : forall L : SimpleGraph V, K <= L ->
      WilliamsonShmoys.HasPlanarDrawingOn L -> L = K) :
    K.edgeSet.ncard + 6 = 3 * Fintype.card V := 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