Maximal drawable supergraph extension

Proved

WilliamsonShmoys.planar_drawing_maximal_extension__p2m_5ca561e0_6863_43fe_aa41_85fb9a3351ed_a1

by Eyal1990 · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximation-algorithmsplanar-graphstreewidth

Every graph with a drawing has a drawable supergraph on the same vertex type that is inclusion-maximal among drawable graphs. The finite maximization argument applies because there are finitely many simple graphs on the fixed finite vertex type and the family is nonempty (it contains the original graph). The child preserves the exact drawing predicate and states maximality against all drawable supergraphs.

Preamble

import Definitions.Def_WilliamsonShmoys_PlanarDrawingOn
import Mathlib

open WilliamsonShmoys
set_option autoImplicit false

Formal statement

theorem WilliamsonShmoys.planar_drawing_maximal_extension__p2m_5ca561e0_6863_43fe_aa41_85fb9a3351ed_a1
    {V : Type} [Fintype V] [LinearOrder V]
    (J : SimpleGraph V) (hJ : WilliamsonShmoys.HasPlanarDrawingOn J) :
    letI : forall K : SimpleGraph V, DecidableRel K.Adj :=
      fun K => Classical.decRel K.Adj
    exists K : SimpleGraph V,
      WilliamsonShmoys.HasPlanarDrawingOn K /\ J <= K /\
      forall L : SimpleGraph V,
        K <= L -> WilliamsonShmoys.HasPlanarDrawingOn L -> L = K := 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