Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.
Proof of `Twin-width can be exponential in treewidth`
groundedproofs/Lax48Proofs/Main.lean · lax-48
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.
In the paper
- page 5 of this submission's paper
Description
Self-contained proof of the Bonnet–Déprés exponential gap: for every , the Bonnet–Déprés graph has treewidth at most while its twin-width exceeds .
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 .
Attribution
Ported from Édouard Bonnet's formalization of Bonnet–Déprés, Twin-width can be exponential in treewidth (JCTB 2023).