Catalog.Sparsity.StrongColoringBoundByAdm
Lemma
For every \(r \in \mathbb{N}\), graph \(G\), and vertex ordering \(\sigma\): \[\operatorname{scol}_r(G, \sigma) \leq 1 + (\operatorname{adm}_r(G, \sigma) - 1)^r.\]
Review notes
The Lean statement matches the source inequality directly, using the
per-ordering scol and adm from Catalog.Sparsity.ColoringNumbers.
Natural-number subtraction makes \(\operatorname{adm} - 1\) safe: when \(\operatorname{adm} = 0\) the right-hand side is \(1 + 0^r \geq 1\) which is trivially at least \(\operatorname{scol}\) (since \(\operatorname{scol} \geq 0\) in \(\mathbb{N}\)).
Catalog/Sparsity/StrongColoringBoundByAdm/Contract.lean (full)
| 1 | import Catalog.Sparsity.ColoringNumbers.Contract |
| 2 | import Catalog.Sparsity.Admissibility.Contract |
| 3 | |
| 4 | namespace Catalog.Sparsity.StrongColoringBoundByAdm |
| 5 | |
| 6 | variable {V : Type*} [DecidableEq V] [Fintype V] [LinearOrder V] |
| 7 | |
| 8 | /-- Lemma 2.5: the strong r-coloring number is bounded by a power of the |
| 9 | r-admissibility. -/ |
| 10 | axiom scol_le_one_add_adm_sub_one_pow (G : SimpleGraph V) (r : ℕ) : |
| 11 | Catalog.Sparsity.ColoringNumbers.scol G r ≤ |
| 12 | 1 + (Catalog.Sparsity.Admissibility.adm G r - 1) ^ r |
| 13 | |
| 14 | end Catalog.Sparsity.StrongColoringBoundByAdm |
| 15 |