Proof of `Twin-width and mixed minor number are functionally equivalent`
groundedproofs/Lax49Proofs/Main.lean · lax-49
What this proof establishes
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
Twin-width and mixed minor number are functionally equivalent, from the two sibling statements bounding each parameter by a function of the other.
Proof strategy
unfolds to the conjunction of the two directional existentials, so pairing the two assumed statements is the whole proof. The mathematical content lives in the proofs of those two statements ( and ).
Attribution
Bonnet–Kim–Thomassé–Watrigant, Twin-width I: Tractable FO Model Checking (J. ACM 2022), state the equivalence as the conjunction of these two bounds.