Lax12.StrongColoringBound

Strong coloring numbers are bounded by admissibility

concepts/Lax12/StrongColoringBound.lean · lax-12

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax12.StrongColoringBound

⊢Lax12Proofs.StrongColoringBound.scol_le_of_adm

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²).

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

Show Proof

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 $adm_r − 1$ 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.

Builds on

Used by

none

From Mathlib

none

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive