Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.
Strong coloring numbers are bounded by admissibility
Lax12.StrongColoringBound · concepts/Lax12/StrongColoringBound.lean · lax-12
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The strong r-coloring number of a graph is at most 1 + (adm_r − 1)^r, where adm_r is its r-admissibility. Together with the trivial bound adm_r ≤ scol_r this says that admissibility and the strong coloring number are functionally equivalent parameters.
This is Lemma 2.5 of Chapter 2 of the source lecture notes (2019/20 edition), which state it for a fixed vertex ordering; the two bounds combine in their Corollary 2.7 to wcol_r ≤ 1 + r(adm_r − 1)^(r²).
Concept map
Lean source view on GitHub
| 1 | import Lax12.Admissibility |
| 2 | import Lax12.ColoringNumbers |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Strong coloring numbers are bounded by admissibility |
| 7 | type: theorem |
| 8 | --- |
| 9 | The strong *r*-coloring number of a graph is at most |
| 10 | 1 + (adm_r − 1)^*r*, where adm_r is its *r*-admissibility. Together with |
| 11 | the trivial bound adm_r ≤ scol_r this says that admissibility and the |
| 12 | strong coloring number are functionally equivalent parameters. |
| 13 | |
| 14 | This is Lemma 2.5 of Chapter 2 of the source lecture notes (2019/20 |
| 15 | edition), which state it for a fixed vertex ordering; the two bounds |
| 16 | combine in their Corollary 2.7 to wcol_r ≤ 1 + *r*(adm_r − 1)^(*r*²). |
| 17 | |
| 18 | # Formalization notes |
| 19 | |
| 20 | Both parameters are the minima over vertex orderings defined in the |
| 21 | imported concepts, and the statement is the minimized form: the |
| 22 | literature proves it for each ordering separately, and the minimized |
| 23 | form follows because the right-hand side is monotone in adm_r, so an |
| 24 | ordering optimal for admissibility witnesses the bound. Natural |
| 25 | subtraction `adm_r − 1` is harmless: admissibility counts the vertex |
| 26 | itself, so it is at least 1 on every nonempty graph, and on the empty |
| 27 | graph both sides degenerate to a true inequality. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax12.StrongColoringBound |
| 31 | |
| 32 | open Lax12.Admissibility Lax12.ColoringNumbers |
| 33 | |
| 34 | /-- The strong `r`-coloring number is at most `1 + (adm_r - 1) ^ r`. -/ |
| 35 | axiom scol_le_of_adm {n : ℕ} (G : SimpleGraph (Fin n)) (r : ℕ) : |
| 36 | scol G r ≤ 1 + (adm G r - 1) ^ r |
| 37 | |
| 38 | end Lax12.StrongColoringBound |
| 39 |
Formalization notes
Both parameters are the minima over vertex orderings defined in the imported concepts, and the statement is the minimized form: the literature proves it for each ordering separately, and the minimized form follows because the right-hand side is monotone in adm_r, so an ordering optimal for admissibility witnesses the bound. Natural subtraction is harmless: admissibility counts the vertex itself, so it is at least 1 on every nonempty graph, and on the empty graph both sides degenerate to a true inequality.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments