Lax Lean Archive

Version history

Submission versions

  1. lax-153141current versionviewing

    Functional Equivalence of Twin-Width and Mixed Minor Number

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceShown on this page
  2. lax-49

    Functional Equivalence of Twin-Width and Mixed Minor Number

    Created Lean v4.30.0mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f
    GitHub sourceOpen version

Functional Equivalence of Twin-Width and Mixed Minor Number

lax-153141·formalized by Édouard Bonnet @EdouardBonnet · Claude Fable 5 (Anthropic) · Codex (OpenAI)·registered·created ·GitHub @bf77d7f·Lean v4.33.0 epoch · mathlib db584cd6d46c·

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    For finite graphs, twin-width and mixed minor number are functionally equivalent: each is bounded by a numerical function of the other. We define mixed minor number, prove both directional bounds for the twin-width parameter of lax-228581, and derive their functional equivalence.

    Concepts

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimClaim from this submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-153141,
  author = {Édouard Bonnet and Claude Fable 5 (Anthropic) and Codex (OpenAI)},
  title = {Functional Equivalence of Twin-Width and Mixed Minor Number},
  year = {2026},
  howpublished = {Lax Archive, lax-153141},
  url = {https://laxarchive.org/lax-153141/},
}

    References

    1. Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé and Rémi Watrigant. Twin-width I: Tractable FO Model Checking. Journal of the ACM 69(1):3:1–3:46, 2022. doi:10.1145/3486655
    2. Adam Marcus and Gábor Tardos. Excluded permutation matrices and the Stanley-Wilf conjecture. Journal of Combinatorial Theory, Series A 107(1):153–160, 2004. doi:10.1016/j.jcta.2004.04.002

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…