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

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.

Read the Lean proof on GitHub

Description

For each kk, a cograph with between 3k3^k and 4k4^k vertices forces at least kk 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 truetrue entry separated from it by falsefalse entries and therefore contributes one new crossing. A binary cotree supplies a width-zero contraction sequence, and a graph isomorphism relabels the result onto FinnFin n.

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.