Lax Lean Archive

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

Lax153141.MixedMinorNumberFromTwinWidth · concepts/Lax153141/MixedMinorNumberFromTwinWidth.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 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 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: 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 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 for this direction is linear.
    21-/
    22
    23namespace Lax153141.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 Lax153141.MixedMinorNumber.mixedMinorNumber G ≤ g (Lax228581.TwinWidth.twinWidth G)
    30
    31end Lax153141.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…