Catalog/Sparsity/ColoringNumberEquivalence/Contract.lean
| 1 | import Catalog.Sparsity.ColoringNumbers.Contract |
| 2 | import Catalog.Sparsity.Admissibility.Contract |
| 3 | |
| 4 | open Catalog.Sparsity.ColoringNumbers |
| 5 | open Catalog.Sparsity.Admissibility |
| 6 | |
| 7 | namespace Catalog.Sparsity.ColoringNumberEquivalence |
| 8 | |
| 9 | variable {V : Type*} [Fintype V] [LinearOrder V] |
| 10 | |
| 11 | /-- Corollary 2.7: wcol_r ≤ 1 + r · (adm_r - 1)^(r²) per ordering. |
| 12 | Combined with Catalog.Sparsity.ColoringNumberOrdering (adm ≤ scol ≤ wcol), |
| 13 | this shows all three parameters are polynomially equivalent. -/ |
| 14 | axiom wcol_le_of_adm (G : SimpleGraph V) (r : ℕ) : |
| 15 | wcol G r ≤ 1 + r * (adm G r - 1) ^ (r ^ 2) |
| 16 | |
| 17 | end Catalog.Sparsity.ColoringNumberEquivalence |
| 18 |