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

Direct proofs for planar graph classes

lax-303502·formalized by Clemens Kuske·created ·GitHub @dd76469·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    This submission gives direct geometric proofs that every finite tree is outerplanar, that every finite star is outerplanar and planar, and that every two-terminal series-parallel graph is planar. It also proves that a finite graph is outerplanar if and only if it has neither a K4K_4 nor a K2,3K_{2,3} minor. The tree and star drawings place vertices on the unit circle using a rational parametrization.

    For trees, induction removes a leaf and then inserts it beside its neighbour in a gap between the existing circle parameters. An affine functional for the new chord separates it from all edges with disjoint endpoints. A tangent functional rules out vertices inside edges. The star proof is also given separately: all its edges share the centre.

    For series-parallel graphs, an induction keeps the terminals at the ends of a horizontal segment and the other vertices in the triangle above it, with a positive height bound. Explicit affine maps join drawings in series. Vertical compression separates parallel components. The proof checks all vertex and edge intersections, including a terminal edge shared by both components, and requires no excluded-minor or straightening theorem.

    For the outerplanar characterization, induction splits disconnected graphs and graphs with a cut vertex into smaller pieces. Acyclic connected pieces use the tree construction. In the remaining case, a longest cycle contains every vertex: an outside component would either extend the cycle or produce a K2,3K_{2,3} minor. A pair of alternating chords would produce a K4K_4 minor, so the cycle order gives the required circle drawing. Conversely, connected minor branch sets preserve circular noncrossing order, and neither forbidden graph admits such an order. This follows the direct cycle argument in Leander's On the bunkbed conjecture, Theorem 14, with explicit proofs of the decompositions, minor witnesses, and geometric steps.

    The proofs discharge the original statements in Planar Graph Classes (Lax68), without changing its definitions or assuming any open characterization theorem. Each proof is added to the archive after kernel validation.

    Together with the existing Lax68 proofs, finite-tree outerplanarity also settles finite-tree planarity and path outerplanarity and planarity. Thus all Lax68 statements labeled as theorems are proved in the combined proof network. Series-parallel planarity and the outerplanar excluded-minor characterization close two statements labeled opnopn. Two remain open: Kuratowski's theorem and Wagner's theorem.

    Concepts

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimClaim from this submission / another submissionProof — open large view for details
    Proof list

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: only B's proofs build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-303502,
      author = {Clemens Kuske},
      title = {Direct proofs for planar graph classes},
      year = {2026},
      howpublished = {Lax Archive, lax-303502},
      url = {https://laxarchive.org/lax-303502/},
      note = {draft},
    }

    References

    1. Reinhard Diestel. Graph Theory. Springer, 2025. diestel-graph-theory.com
    2. János Pach and Jenő Törőcsik. Layout of Rooted Trees. Princeton University CS-TR-369-92, 1992. cs.princeton.edu/techreports/1992/369.pdf
    3. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic, a Language Theoretic Approach. 2011. April 2011 preprint, Section 1.2.2, page 33. labri.fr/perso/courcell/Book/TheBook.pdf
    4. Madeleine Leander. On the bunkbed conjecture. Stockholm University 2009:7, 2009. Theorem 14, page 37. kurser.math.su.se/pluginfile.php/16103/mod_folder/content/0/2009/2009_07_report.pdf

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…