Catalog.Sparsity.ColoringNumberEquivalence
Lemma
Let \(\operatorname{adm}_r\), \(\operatorname{scol}_r\), and \(\operatorname{wcol}_r\) be as in Definition ColoringNumbers.
For every \(r \in \mathbb{N}\), graph \(G\), and vertex ordering \(\sigma\): \[\operatorname{adm}_r(G, \sigma) \leq \operatorname{scol}_r(G, \sigma) \leq \operatorname{wcol}_r(G, \sigma) \leq 1 + r(\operatorname{adm}_r(G, \sigma) - 1)^{r^2}.\]
In particular, for every \(r \in \mathbb{N}\) and graph \(G\): \[\operatorname{adm}_r(G) \leq \operatorname{scol}_r(G) \leq \operatorname{wcol}_r(G) \leq 1 + r(\operatorname{adm}_r(G) - 1)^{r^2}.\]
Review notes
The graph-level inequalities require a small argument: per-ordering pointwise bounds \(f(\sigma) \leq g(\sigma)\) give \(\min_\sigma f \leq \min_\sigma g\), and \(g(\sigma) \leq h(f(\sigma))\) with \(h\) monotone gives \(\min_\sigma g \leq h(\min_\sigma f)\) by evaluating at the \(f\)-minimizer.
Lean encoding.
Only the new upper bound \(\operatorname{wcol}_r \leq 1 + r(\operatorname{adm}_r - 1)^{r^2}\) is stated per ordering. The lower bounds are already in Lemma ColoringNumberOrdering. The graph-level version from the source follows by choosing appropriate orderings but is not stated separately.
Catalog/Sparsity/ColoringNumberEquivalence/Contract.lean (full)
| 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 |