Proof of `Cographs have logarithmic Welzl trees`
groundedproofs/Lax485480Proofs/CographWelzlTreeUpperBound.lean · lax-485480
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
Every nonempty cograph has a spanning Welzl tree with at most crossings per open-neighborhood row.
Proof strategy
Apply the preceding logarithmic Welzl-order theorem and join consecutive vertices of its witnessing order. This graph is a spanning path, hence a tree, and the order-path bridge identifies its tree crossing number with the crossing number of the order.
Attribution
The logarithmic cograph-order phenomenon is the contiguity upper bound of Crespelle and Gambette. The path construction is the immediate tree form of Welzl's crossing-number definition; its formal order bound is imported from lax-214022.