Proof of `Cographs can require logarithmic Welzl trees`
groundedproofs/Lax485480Proofs/CographWelzlTreeLowerBound.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
There are cographs on between and vertices for which every Welzl tree has crossing number at least .
Proof strategy
Use the cograph from the logarithmic Welzl-order lower bound. Given any spanning tree of crossing number , repeatedly delete a leaf and reinsert it beside its unique neighbor to obtain an order of crossing number at most . The witness requires at least order crossings, so , which is equivalent over the naturals to .
Attribution
Crespelle and Gambette proved the logarithmic contiguity lower bound for cographs with complete binary cotrees. The explicit order witnesses used here are imported from lax-214022. The leaf-removal linearization is the standard depth-first factor-two conversion from tree cuts to a linear layout, and upgrades their order phenomenon to arbitrary spanning trees.