Lax Lean Archive

Version history

Submission versions

  1. lax-153141current version

    Functional Equivalence of Twin-Width and Mixed Minor Number

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceOpen version
  2. lax-49viewing

    Functional Equivalence of Twin-Width and Mixed Minor Number

    Created Lean v4.30.0mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f
    GitHub sourceShown on this page

Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

Mixed minor number is bounded by a function of twin-width

Lax49.MixedMinorNumberFromTwinWidth · concepts/Lax49/MixedMinorNumberFromTwinWidth.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.

    Natural Language Statement

    Theorem

    There is a function g : ℕ → ℕ such that every finite simple graph G satisfies mmn(G) ≤ g(tww(G)): a graph of bounded twin-width admits a vertex ordering whose adjacency matrix has no large mixed minor. Twin-width is the parameter of submission Lax48, 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 Lax48.TwinWidth
    2import Lax49.MixedMinorNumber
    3
    4/-!
    5---
    6title: Mixed minor number is bounded by a function of twin-width
    7type: theorem
    8---
    9There is a function *g* : ℕ → ℕ such that every finite simple graph *G*
    10satisfies mmn(*G*) ≤ *g*(tww(*G*)): a graph of bounded twin-width admits a
    11vertex ordering whose adjacency matrix has no large mixed minor. 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 for this direction is linear.
    21-/
    22
    23namespace Lax49.MixedMinorNumberFromTwinWidth
    24
    25/-- Mixed minor number is bounded by a numerical function of twin-width. -/
    26axiom exists_mixedMinorNumber_bound_of_twinWidth :
    27 ∃ g : ℕ → ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V]
    28 (G : SimpleGraph V),
    29 Lax49.MixedMinorNumber.mixedMinorNumber G ≤ g (Lax48.TwinWidth.twinWidth G)
    30
    31end Lax49.MixedMinorNumberFromTwinWidth
    32
    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 for this direction is linear.

    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…