Proof of `Mixed minor number is bounded by a function of twin-width`
groundedproofs/Lax49Proofs/MixedMinorNumberFromTwinWidth.lean · lax-49
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The submitted mixed minor number is bounded by a numerical function of twin-width (the parameter of submission Lax48); the witness is the linear function .
Proof strategy
The left-to-right leaf order of a twin-decomposition of width makes the ordered adjacency matrix twin-ordered, and the first item of the grid-minor theorem for twin-width bounds the mixed number of a twin-ordered matrix linearly; the absorbs the diagonal convention and the two one-sided child zones created by mirroring a graph contraction as a row and a column fusion. Rewriting with the two parameter equalities of moves the bound onto the submitted parameters.
Attribution
Bonnet, Kim, Thomassé and Watrigant, Twin-width I: Tractable FO Model Checking (J. ACM 2022).