Catalog/Sparsity/ColoringNumberOrdering/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.ColoringNumberOrdering
8
9	variable {V : Type*} [Fintype V] [LinearOrder V]
10
11	/-- Proposition 2.4 (first part): adm_r ≤ scol_r for any graph and ordering. -/
12	axiom adm_le_scol (G : SimpleGraph V) (r : ℕ) :
13	adm G r ≤ scol G r
14
15	/-- Proposition 2.4 (second part): scol_r ≤ wcol_r for any graph and ordering. -/
16	axiom scol_le_wcol (G : SimpleGraph V) (r : ℕ) :
17	scol G r ≤ wcol G r
18
19	/-- Lemma 2.6: wcol_r ≤ 1 + r · (scol_r - 1)^r. -/
20	axiom wcol_le_of_scol (G : SimpleGraph V) (r : ℕ) :
21	wcol G r ≤ 1 + r * (scol G r - 1) ^ r
22
23	end Catalog.Sparsity.ColoringNumberOrdering
24