Lax Lean Archive

Strong coloring numbers are bounded by admissibility

Lax199508.StrongColoringBound · concepts/Lax199508/StrongColoringBound.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 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
    4 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.Admissibility
    2import Lax199508.ColoringNumbers
    3
    4/-!
    5---
    6title: Strong coloring numbers are bounded by admissibility
    7type: theorem
    8---
    9The strong *r*-coloring number of a graph is at most
    101 + (adm_r − 1)^*r*, where adm_r is its *r*-admissibility. Together with
    11the trivial bound adm_r ≤ scol_r this says that admissibility and the
    12strong coloring number are functionally equivalent parameters.
    13
    14This is Lemma 2.5 of Chapter 2 of the source lecture notes (2019/20
    15edition), which state it for a fixed vertex ordering; the two bounds
    16combine in their Corollary 2.7 to wcol_r ≤ 1 + *r*(adm_r − 1)^(*r*²).
    17
    18# Formalization notes
    19
    20Both parameters are the minima over vertex orderings defined in the
    21imported concepts, 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 adm_r, so an
    24ordering optimal for admissibility witnesses the bound. Natural
    25subtraction `adm_r − 1` is harmless: admissibility counts the vertex
    26itself, so it is at least 1 on every nonempty graph, and on the empty
    27graph both sides degenerate to a true inequality.
    28-/
    29
    30namespace Lax199508.StrongColoringBound
    31
    32open Lax199508.Admissibility Lax199508.ColoringNumbers
    33
    34/-- The strong `r`-coloring number is at most `1 + (adm_r - 1) ^ r`. -/
    35axiom scol_le_of_adm {n : ℕ} (G : SimpleGraph (Fin n)) (r : ℕ) :
    36 scol G r ≤ 1 + (adm G r - 1) ^ r
    37
    38end Lax199508.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 admr−1adm_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

    Discussion

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

    Loading discussion…