Catalog.Sparsity.ColoringNumberOrdering
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).\]
Furthermore: \[\operatorname{wcol}_r(G, \sigma) \leq 1 + r(\operatorname{scol}_r(G, \sigma) - 1)^r.\]
Review notes
This entry bundles two results: Proposition 2.4 (the trivial ordering \(\operatorname{adm}_r \leq \operatorname{scol}_r \leq \operatorname{wcol}_r\)) and Lemma 2.6 (the reverse bound \(\operatorname{wcol}_r \leq 1 + r(\operatorname{scol}_r - 1)^r\)). Together with Lemma StrongColoringBoundByAdm (Lemma 2.5), they give the full polynomial equivalence of Corollary 2.7.
The signature argument in Lemma 2.6 encodes each weakly reachable vertex as a sequence of indices into the strongly reachable sets along the milestone chain. Injectivity of the encoding gives the counting bound.
Lean encoding.
The contract states three per-ordering axioms using the definitions from
Definition ColoringNumbers (which depend on LinearOrder V).
No graph-level versions are stated; the per-ordering form is strictly stronger.
Subtraction in \(1 + r(k-1)^r\) uses natural number arithmetic; since
\(\operatorname{scol}_r \geq 1\) always, no underflow occurs.
Catalog/Sparsity/ColoringNumberOrdering/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.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 |