Lax

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

Lax1.ExponentialSeparation

Twin-width can be exponential in treewidth

concepts/Lax1/ExponentialSeparation.lean · Lax1

proven

Theorem

For every k∈Nk\in\mathbb{N}, there is a finite simple graph GG such that $$ \operatorname{tw}(G) \le 2k+4 \quad\text{and}\quad 2^k < \operatorname{tww}(G). $$ Here tw⁡\operatorname{tw} and tww⁡\operatorname{tww} are the treewidth and twin-width parameters defined in the two prerequisite concepts.

Lean source

1import Lax1.Treewidth
2import Lax1.TwinWidth
3
4/-!
5---
6title: Twin-width can be exponential in treewidth
7type: theorem
8---
9For every $k\in\mathbb{N}$, there is a finite simple graph $G$ such that
10$$
11 \operatorname{tw}(G) \le 2k+4
12 \quad\text{and}\quad
13 2^k < \operatorname{tww}(G).
14$$
15Here $\operatorname{tw}$ and $\operatorname{tww}$ are the treewidth and
16twin-width parameters defined in the two prerequisite concepts.
17
18# Formalization notes
19
20The graph is quantified over the canonical finite vertex types
21$\operatorname{Fin} n$, which loses no generality: every finite simple
22graph is isomorphic to a graph on some $\operatorname{Fin} n$.
23-/
24
25namespace Lax1.ExponentialSeparation
26
27/-- For every `k`, some finite graph has treewidth at most `2 * k + 4` and
28twin-width greater than `2 ^ k`. -/
29axiom twin_width_can_be_exponential_in_treewidth (k : ℕ) :
30 ∃ n : ℕ, ∃ G : SimpleGraph (Fin n),
31 Lax1.Treewidth.treewidth G ≤ 2 * k + 4 ∧
32 2 ^ k < Lax1.TwinWidth.twinWidth G
33
34end Lax1.ExponentialSeparation
35

Formalization notes

The graph is quantified over the canonical finite vertex types Fin⁡n\operatorname{Fin} n, which loses no generality: every finite simple graph is isomorphic to a graph on some Fin⁡n\operatorname{Fin} n.

Imported

Imported by

none

Mathlib imports

none