Lax Lean Archive

Lax49.MixedMinorNumberFromTwinWidth

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

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.

    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 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.

    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

    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…