Proof of `Cographs can require logarithmic Welzl orders`
groundedproofs/Lax214022Proofs/CographWelzlLowerBound.lean · lax-214022
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
For each , a cograph with between and vertices forces at least crossings in some open-neighborhood row of every order.
Proof strategy
Use a universal root above three recursive copies. In any linear order, one copy avoids the branches of both immediate neighbors of the root. Restricting the order to that copy preserves the inductive row, while the universal root is a entry separated from it by entries and therefore contributes one new crossing. A binary cotree supplies a width-zero contraction sequence, and a graph isomorphism relabels the result onto .
Attribution
The ternary construction and order obstruction are the standard lower-bound argument for cograph contiguity due to Crespelle and Gambette. The present proof is adapted to crossing counts of open-neighborhood rows.