Lax Lean Archive

Lax49.FunctionalEquivalence

Twin-width and mixed minor number are functionally equivalent

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

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

    Lean source view on GitHub

    1import Lax48.TwinWidth
    2import Lax49.GraphParameters
    3import Lax49.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 `Lax48.TwinWidth.twinWidth` and
    23`Lax49.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 Lax49.FunctionalEquivalence
    32
    33open Lax49.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 Lax48.TwinWidth.twinWidth
    40 Lax49.MixedMinorNumber.mixedMinorNumber
    41
    42end Lax49.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 Lax48.TwinWidth.twinWidthLax48.TwinWidth.twinWidth and Lax49.MixedMinorNumber.mixedMinorNumberLax49.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

    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…