Lax Lean Archive

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

groundedproofs/Lax228581Proofs/Main.lean · lax-228581

What this proof establishes

no assumptions

thm✓Lax228581.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

For every natural number kk, there is a finite simple graph GG whose treewidth tw(G)\mathrm{tw}(G) and twin-width tww(G)\mathrm{tww}(G) satisfy

tw(G)≤2k+4and2k<tww(G).\mathrm{tw}(G) \le 2k + 4 \qquad\text{and}\qquad 2^k < \mathrm{tww}(G).

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 Twin-width can be exponential in treewidth (JCTB 2023).