Lax Lean Archive

Lax49.TwinWidthFromMixedMinorNumber

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

concepts/Lax49/TwinWidthFromMixedMinorNumber.lean · lax-49

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.

    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 Lax48, mixed minor number the parameter of the prerequisite concept.

    Lean source view on GitHub

    1import Lax48.TwinWidth
    2import Lax49.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 Lax48, 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 Lax49.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 Lax48.TwinWidth.twinWidth G ≤ f (Lax49.MixedMinorNumber.mixedMinorNumber G)
    31
    32end Lax49.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

    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…