Lax Lean Archive

Lax48.ExponentialSeparation

Twin-width can be exponential in treewidth

concepts/Lax48/ExponentialSeparation.lean · lax-48

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.

    Concept map

    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

    Theorem

    For every natural number k, there is a finite simple graph G with treewidth at most 2k + 4 and twin-width greater than 2ᵏ. Treewidth and twin-width are the parameters defined in the two prerequisite concepts.

    Lean source view on GitHub

    1import Lax48.Treewidth
    2import Lax48.TwinWidth
    3
    4/-!
    5---
    6title: Twin-width can be exponential in treewidth
    7type: theorem
    8---
    9For every natural number *k*, there is a finite simple graph *G* with
    10treewidth at most 2*k* + 4 and twin-width greater than 2ᵏ. Treewidth and
    11twin-width are the parameters defined in the two prerequisite concepts.
    12
    13# Formalization notes
    14
    15The graph is quantified over the canonical finite vertex types `Fin n`,
    16which loses no generality: every finite simple graph is isomorphic to a
    17graph on some `Fin n`.
    18-/
    19
    20namespace Lax48.ExponentialSeparation
    21
    22/-- For every `k`, some finite graph has treewidth at most `2 * k + 4` and
    23twin-width greater than `2 ^ k`. -/
    24axiom exists_treewidth_le_and_two_pow_lt_twinWidth (k : ℕ) :
    25 ∃ n : ℕ, ∃ G : SimpleGraph (Fin n),
    26 Lax48.Treewidth.treewidth G ≤ 2 * k + 4 ∧
    27 2 ^ k < Lax48.TwinWidth.twinWidth G
    28
    29end Lax48.ExponentialSeparation
    30
    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

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…