Lax Lean Archive

Twin-width and mixed minor number are functionally equivalent

Lax153141.FunctionalEquivalence · concepts/Lax153141/FunctionalEquivalence.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

    Two finite-graph parameters are functionally equivalent when each is bounded by a numerical function of the other. Twin-width and mixed minor number are functionally equivalent: there are functions f, g : ℕ → ℕ such that every finite simple graph G satisfies both:

    • tww(G) ≤ f(mmn(G)); and
    • mmn(G) ≤ g(tww(G)).
    Concept map
    4 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.GraphParameters
    3import Lax153141.MixedMinorNumber
    4
    5/-!
    6---
    7title: Twin-width and mixed minor number are functionally equivalent
    8type: theorem
    9---
    10Two finite-graph parameters are *functionally equivalent* when each is
    11bounded by a numerical function of the other. Twin-width and mixed minor
    12number are functionally equivalent: there are functions *f*, *g* : ℕ → ℕ
    13such that every finite simple graph *G* satisfies both:
    14
    15- tww(*G*) ≤ *f*(mmn(*G*)); and
    16- mmn(*G*) ≤ *g*(tww(*G*)).
    17
    18# Formalization notes
    19
    20`FunctionallyEquivalent` and the uniform parameter signature it is stated
    21over come from the graph parameters concept; the equivalence applies the
    22relation to `Lax228581.TwinWidth.twinWidth` and
    23`Lax153141.MixedMinorNumber.mixedMinorNumber` directly, without wrapper lambdas.
    24
    25The two directions are also stated on their own, as the sibling concepts
    26`TwinWidthFromMixedMinorNumber` and `MixedMinorNumberFromTwinWidth`: each has
    27its own literature proof and is usable on its own. This concept is the
    28headline claim that both hold at once.
    29-/
    30
    31namespace Lax153141.FunctionalEquivalence
    32
    33open Lax153141.GraphParameters
    34
    35/-- Twin-width and mixed minor number are functionally equivalent graph
    36parameters. -/
    37axiom twin_width_functionally_equivalent_mixed_minor_number :
    38 FunctionallyEquivalent
    39 Lax228581.TwinWidth.twinWidth
    40 Lax153141.MixedMinorNumber.mixedMinorNumber
    41
    42end Lax153141.FunctionalEquivalence
    43
    Show Proof
    Formalization notes

    FunctionallyEquivalentFunctionallyEquivalent and the uniform parameter signature it is stated over come from the graph parameters concept; the equivalence applies the relation to Lax228581.TwinWidth.twinWidthLax228581.TwinWidth.twinWidth and Lax153141.MixedMinorNumber.mixedMinorNumberLax153141.MixedMinorNumber.mixedMinorNumber directly, without wrapper lambdas.

    The two directions are also stated on their own, as the sibling concepts TwinWidthFromMixedMinorNumberTwinWidthFromMixedMinorNumber and MixedMinorNumberFromTwinWidthMixedMinorNumberFromTwinWidth: each has its own literature proof and is usable on its own. This concept is the headline claim that both hold at once.

    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…