Draft — mutable and not usable as a dependency; its citation marks the draft state.

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.

Read the Lean proof on GitHub

Description

There are cographs on between 3k3^k and 4k4^k vertices for which every Welzl tree has crossing number at least ceil(k/2)ceil(k/2).

Proof strategy

Use the cograph from the logarithmic Welzl-order lower bound. Given any spanning tree of crossing number cc, repeatedly delete a leaf and reinsert it beside its unique neighbor to obtain an order of crossing number at most 2c2c. The witness requires at least kk order crossings, so k2ck ≤ 2c, which is equivalent over the naturals to ceil(k/2)cceil(k/2) ≤ c.

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.