Lax Lean Archive

Lax12.WeakColoringBound

Weak coloring numbers are bounded by strong coloring numbers

concepts/Lax12/WeakColoringBound.lean · lax-12

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

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

    Lean source view on GitHub

    1import Lax12.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 Lax12.WeakColoringBound
    32
    33open Lax12.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 Lax12.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

    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…