Lax2.FunctionalEquivalence
Twin-width and mixed minor number are functionally equivalent
concepts/Lax2/FunctionalEquivalence.lean · Lax2
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
| 1 | import Lax1.TwinWidth |
| 2 | import Lax2.MixedMinorNumber |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Twin-width and mixed minor number are functionally equivalent |
| 7 | type: theorem |
| 8 | --- |
| 9 | Two finite-graph parameters are *functionally equivalent* when each is |
| 10 | bounded by a numerical function of the other. Twin-width and mixed minor |
| 11 | number are functionally equivalent: there are functions *f*, *g* : ℕ → ℕ |
| 12 | such that every finite simple graph *G* satisfies both: |
| 13 | |
| 14 | - tww(*G*) ≤ *f*(mmn(*G*)); and |
| 15 | - mmn(*G*) ≤ *g*(tww(*G*)). |
| 16 | |
| 17 | # Formalization notes |
| 18 | |
| 19 | `GraphParam` is the uniform signature shared by all graph parameters in this |
| 20 | archive: a natural-valued function of finite simple graphs over `Fintype` |
| 21 | and `DecidableEq` instances. It is an abbreviation, so the statement applies |
| 22 | to `Lax1.TwinWidth.twinWidth` and `Lax2.MixedMinorNumber.mixedMinorNumber` |
| 23 | directly, without wrapper lambdas. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax2.FunctionalEquivalence |
| 27 | |
| 28 | /-- A natural-valued parameter of finite simple graphs, in the uniform |
| 29 | signature shared by all graph parameters in this archive. -/ |
| 30 | abbrev GraphParam := |
| 31 | ∀ {V : Type} [Fintype V] [DecidableEq V], SimpleGraph V → ℕ |
| 32 | |
| 33 | /-- Each of two graph parameters is bounded by a numerical function of the |
| 34 | other. -/ |
| 35 | def FunctionallyEquivalent (p q : GraphParam) : Prop := |
| 36 | (∃ f : ℕ → ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V] |
| 37 | (G : SimpleGraph V), p G ≤ f (q G)) ∧ |
| 38 | (∃ g : ℕ → ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V] |
| 39 | (G : SimpleGraph V), q G ≤ g (p G)) |
| 40 | |
| 41 | /-- Twin-width and mixed minor number are functionally equivalent graph |
| 42 | parameters. -/ |
| 43 | axiom twin_width_functionally_equivalent_mixed_minor_number : |
| 44 | FunctionallyEquivalent |
| 45 | Lax1.TwinWidth.twinWidth |
| 46 | Lax2.MixedMinorNumber.mixedMinorNumber |
| 47 | |
| 48 | end Lax2.FunctionalEquivalence |
| 49 |
Formalization notes
GraphParam is the uniform signature shared by all graph parameters in this
archive: a natural-valued function of finite simple graphs over Fintype
and DecidableEq instances. It is an abbreviation, so the statement applies
to Lax1.TwinWidth.twinWidth and Lax2.MixedMinorNumber.mixedMinorNumber
directly, without wrapper lambdas.
Imported by
none
Mathlib imports
none