Lax Lean Archive

Twin-width can be exponential in treewidth

Lax228581.ExponentialSeparation · concepts/Lax228581/ExponentialSeparation.lean · lax-228581

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    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).
    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 3 of this submission's paper
    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax228581.Treewidth
    2import Lax228581.TwinWidth
    3
    4/-!
    5---
    6title: Twin-width can be exponential in treewidth
    7type: theorem
    8---
    9For every natural number kk, there is a finite simple graph GG whose
    10treewidth tw(G)\mathrm{tw}(G) and twin-width tww(G)\mathrm{tww}(G) satisfy
    11
    12tw(G)≤2k+4and2k<tww(G).\mathrm{tw}(G) \le 2k + 4 \qquad\text{and}\qquad 2^k < \mathrm{tww}(G).
    13
    14
    15
    16
    17# Formalization notes
    18
    19The graph is quantified over the canonical finite vertex types `Fin n`,
    20which loses no generality: every finite simple graph is isomorphic to a
    21graph on some `Fin n`.
    22-/
    23
    24namespace Lax228581.ExponentialSeparation
    25
    26/-- For every `k`, some finite graph has treewidth at most `2 * k + 4` and
    27twin-width greater than `2 ^ k`. -/
    28axiom exists_treewidth_le_and_two_pow_lt_twinWidth (k : ℕ) :
    29 ∃ n : ℕ, ∃ G : SimpleGraph (Fin n),
    30 Lax228581.Treewidth.treewidth G ≤ 2 * k + 4 ∧
    31 2 ^ k < Lax228581.TwinWidth.twinWidth G
    32
    33end Lax228581.ExponentialSeparation
    34
    Show Proof
    Formalization notes

    The graph is quantified over the canonical finite vertex types FinnFin n, which loses no generality: every finite simple graph is isomorphic to a graph on some FinnFin n.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…