Lax Lean Archive

Weak coloring numbers are bounded by strong coloring numbers

Lax199508.WeakColoringBound · concepts/Lax199508/WeakColoringBound.lean · lax-199508

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    The weak r-coloring number of a graph is at most 1 + r · (scol_r − 1)^r, where scol_r is its strong r-coloring number. With the trivial bound scol_r ≤ wcol_r this says that the two generalized coloring numbers are functionally equivalent parameters.

    This is Lemma 2.6 of Chapter 2 of the source lecture notes (2019/20 edition), which state it for a fixed vertex ordering; composed with their Lemma 2.5 it gives their Corollary 2.7, wcol_r ≤ 1 + r(adm_r − 1)^(r²).

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax199508.ColoringNumbers
    2
    3/-!
    4---
    5title: Weak coloring numbers are bounded by strong coloring numbers
    6type: theorem
    7---
    8The weak *r*-coloring number of a graph is at most
    91 + *r* · (scol_r − 1)^*r*, where scol_r is its strong *r*-coloring
    10number. With the trivial bound scol_r ≤ wcol_r this says that the two
    11generalized coloring numbers are functionally equivalent parameters.
    12
    13This is Lemma 2.6 of Chapter 2 of the source lecture notes (2019/20
    14edition), which state it for a fixed vertex ordering; composed with
    15their Lemma 2.5 it gives their Corollary 2.7,
    16wcol_r ≤ 1 + *r*(adm_r − 1)^(*r*²).
    17
    18# Formalization notes
    19
    20Both parameters are the minima over vertex orderings defined in the
    21imported concept, and the statement is the minimized form: the
    22literature proves it for each ordering separately, and the minimized
    23form follows because the right-hand side is monotone in scol_r, so an
    24ordering optimal for the strong coloring number witnesses the bound. The
    25proof idea is that a weakly reachable vertex is found by a bounded
    26search tree of strongly reachable vertices, of depth *r* and branching
    27scol_r − 1. Natural subtraction is harmless: strong coloring numbers
    28count the vertex itself, so they are at least 1 on every nonempty graph.
    29-/
    30
    31namespace Lax199508.WeakColoringBound
    32
    33open Lax199508.ColoringNumbers
    34
    35/-- The weak `r`-coloring number is at most `1 + r · (scol_r - 1) ^ r`. -/
    36axiom wcol_le_of_scol {n : ℕ} (G : SimpleGraph (Fin n)) (r : ℕ) :
    37 wcol G r ≤ 1 + r * (scol G r - 1) ^ r
    38
    39end Lax199508.WeakColoringBound
    40
    Show Proof
    Formalization notes

    Both parameters are the minima over vertex orderings defined in the imported concept, 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 scol_r, so an ordering optimal for the strong coloring number witnesses the bound. The proof idea is that a weakly reachable vertex is found by a bounded search tree of strongly reachable vertices, of depth r and branching scol_r − 1. Natural subtraction is harmless: strong coloring numbers count the vertex itself, so they are at least 1 on every nonempty graph.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…