Proof of `Wagner's theorem`
conditional — 1 open assumptionproofs/Lax303502Proofs/Wagner.lean · lax-303502
What this proof establishes
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
Wagner's characterization follows from Kuratowski's straight-line characterization and the equivalence of the two forbidden pairs. The utility-graph obstruction is proved independently by polygonal separation. The only statement assumption is .
Proof strategy
First prove the combinatorial equivalence independently of planarity. A subdivision gives a minor by contracting every path towards one endpoint. For the converse, choose one connecting edge for every adjacent pair of minor branch sets. Three attachment vertices in a connected branch set have paths meeting only at one center, so a minor gives a subdivision.
For a minor, attach the fourth terminal to the three-arm construction at its first point of contact. If every branch set gives four paths meeting only at a center, the local paths combine into a subdivision of . Otherwise one branch set splits into two disjoint connected sets with two attachments each and an edge between them. Those two sets and the other four branch sets give a minor, to which the previous construction applies. Finally use the assumed Kuratowski characterization to obtain the original straight-line version of Wagner's theorem.
Attribution
Diestel, Graph Theory, sixth edition, Chapter 4, Lemma 4.4.2, printed page 107, with the degree-three conversion from Chapter 1, Proposition 1.7.3. The implementation replaces the minimal-tree argument by explicit paths and their first points of contact. Every minor branch set and subdivision route is constructed and checked. No drawing theorem is used in the combinatorial bridge.
The independent utility-graph obstruction uses Álvaro Begué's polygonal Jordan and crosscut separation proofs, included with attribution in the submission's bibliography and source notices.