Lax Lean Archive

Proof of `Twin-width can be exponential in treewidth`

groundedproofs/Lax48Proofs/Main.lean · lax-48

What this proof establishes

no assumptions

thm✓Lax48.ExponentialSeparation

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

In the paper

  • page 5 of this submission's paper

Description

Self-contained proof of the Bonnet–Déprés exponential gap: for every kk, the Bonnet–Déprés graph BDkBD_k has treewidth at most 2∗k+42*k + 4 while its twin-width exceeds 2k2^k.

Proof strategy

The source development phrases contraction sequences as trigraph state machines; the proof bridges them to the submitted partition-based sequences through the invariant that black and red edges agree with completeness and non-homogeneity in the graph, and relabels the result onto the canonical vertex type FinnFin n.

Attribution

Ported from Édouard Bonnet's formalization of Bonnet–Déprés, Twin-width can be exponential in treewidth (JCTB 2023).