Lax Lean Archive

Twin-width is bounded by a function of mixed minor number

Lax153141.TwinWidthFromMixedMinorNumber · concepts/Lax153141/TwinWidthFromMixedMinorNumber.lean · lax-153141

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

    There is a function f : ℕ → ℕ such that every finite simple graph G satisfies tww(G) ≤ f(mmn(G)): a graph whose adjacency matrix admits no large mixed minor in any vertex ordering has bounded twin-width. Twin-width is the parameter of submission Lax228581, mixed minor number the parameter of the prerequisite concept.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax228581.TwinWidth
    2import Lax153141.MixedMinorNumber
    3
    4/-!
    5---
    6title: Twin-width is bounded by a function of mixed minor number
    7type: theorem
    8---
    9There is a function *f* : ℕ → ℕ such that every finite simple graph *G*
    10satisfies tww(*G*) ≤ *f*(mmn(*G*)): a graph whose adjacency matrix admits no
    11large mixed minor in any vertex ordering has bounded twin-width. Twin-width
    12is the parameter of submission Lax228581, mixed minor number the parameter of the
    13prerequisite concept.
    14
    15# Formalization notes
    16
    17The bound is stated over the two parameters themselves, on arbitrary finite
    18vertex types carrying `Fintype` and `DecidableEq` instances — the signature
    19both parameters have. Only the existence of a bounding function is claimed:
    20the known witness is doubly exponential, and its shape is not part of the
    21result.
    22-/
    23
    24namespace Lax153141.TwinWidthFromMixedMinorNumber
    25
    26/-- Twin-width is bounded by a numerical function of mixed minor number. -/
    27axiom exists_twinWidth_bound_of_mixedMinorNumber :
    28 ∃ f : ℕ → ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V]
    29 (G : SimpleGraph V),
    30 Lax228581.TwinWidth.twinWidth G ≤ f (Lax153141.MixedMinorNumber.mixedMinorNumber G)
    31
    32end Lax153141.TwinWidthFromMixedMinorNumber
    33
    Show Proof
    Formalization notes

    The bound is stated over the two parameters themselves, on arbitrary finite vertex types carrying FintypeFintype and DecidableEqDecidableEq instances — the signature both parameters have. Only the existence of a bounding function is claimed: the known witness is doubly exponential, and its shape is not part of the result.

    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…