Proof of `Series-parallel graphs are planar`
groundedproofs/Lax303502Proofs/SeriesParallel.lean · lax-303502
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Every two-terminal series-parallel graph with full support has a straight-line planar drawing.
Proof strategy
Strengthen the induction on the two-terminal construction. Place the terminals at and , all vertices in , and all other vertices above a positive height. Keep a certificate that intersecting edges or singleton vertices have a common endpoint.
For series composition use the affine maps and . The drawings occupy opposite half-strips, with the shared terminal at . For parallel composition, multiply the second drawing's heights by half the first drawing's positive height bound. Its segments then lie below every non-baseline segment of the first drawing, except at a shared terminal. A baseline edge present in both components is handled explicitly. The new positive bounds are respectively one quarter of the minimum old bound, and the minimum of the first and scaled second bound.
Finally the full-support hypothesis upgrades the supported certificate to the exact required by the original statement. This proof uses neither an excluded-minor theorem nor a straightening theorem.
Attribution
First checked Diestel, Graph Theory, sixth edition, Chapters 4 and 12; the consulted material did not give the direct two-terminal construction. Courcelle and Engelfriet, Graph Structure and Monadic Second-Order Logic, a Language Theoretic Approach, April 2011 preprint, Section 1.2.2, printed page 33, give the induction with both terminals on the external face. The explicit affine maps, height invariant and separation inequalities above are the straight-line realization formalized in this submission.