Lax Lean Archive

Neighborhood covers of weak coloring degree

Lax3.NeighborhoodCoverBound · concepts/Lax3/NeighborhoodCoverBound.lean · lax-3

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

    Every graph has, for every radius r, an r-neighborhood cover of radius 2r whose degree is at most the weak 2r-coloring number of the graph.

    This is Theorem 6.2 of Grohe–Kreutzer–Siebertz (via their Lemma 6.9): from a vertex ordering witnessing the weak coloring number, take as the cluster of v the set of vertices from which v is weakly 2r-reachable. On a nowhere dense class this composes with Lax199508's subpolynomial weak coloring numbers to covers of degree c · n^ε for every ε > 0 — the form the model-checking recursion consumes, on every arena, since the weak coloring bound of Lax199508 is uniform over subgraphs of members.

    Concept map
    6 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 Lax3.OrderedNeighborhoodCover
    2import Lax199508.ColoringNumbers
    3
    4/-!
    5---
    6title: Neighborhood covers of weak coloring degree
    7type: theorem
    8---
    9Every graph has, for every radius *r*, an *r*-neighborhood cover of
    10radius 2*r* whose degree is at most the weak 2*r*-coloring number of
    11the graph.
    12
    13This is Theorem 6.2 of Grohe–Kreutzer–Siebertz (via their Lemma 6.9):
    14from a vertex ordering witnessing the weak coloring number, take as
    15the cluster of *v* the set of vertices from which *v* is weakly
    162*r*-reachable. On a nowhere dense class this composes with Lax199508's
    17subpolynomial weak coloring numbers to covers of degree *c* · *n*^ε
    18for every ε > 0 — the form the model-checking recursion consumes, on
    19every arena, since the weak coloring bound of Lax199508 is uniform over
    20subgraphs of members.
    21
    22# Formalization notes
    23
    24The statement is per-graph and class-free, with the degree bound
    25`wcol G (2r)` — Lax199508's `wcol`, not restated. It chooses an optimal
    26ordering and applies the arbitrary-order construction
    27`Lax3.OrderedNeighborhoodCover.isNeighborhoodCover_wreach` to it.
    28That core names the clusters explicitly and accepts the supplied
    29ordering's weak reachability bound; it is also the form the
    30model-checking algorithm consumes for its computed ordering. The
    31existential theorem composes with any wcol bound a consumer owns,
    32including the subpolynomial bound for nowhere dense classes.
    33
    34The discharge shows that an optimal ordering `π` exists, then applies
    35the core claim to the clusters `{w | u ∈ wreach G π (2r) w}` with
    36the bound `(wreach G π (2r) v).ncard ≤ wcol G (2r)`. Covering and
    37radius are the elementary walk arguments proved for the core. The
    38*computation* of such a cover on the word RAM — including computing a
    39good-enough ordering — is proved in the algorithmic layer and is not
    40part of this claim.
    41-/
    42
    43namespace Lax3.NeighborhoodCoverBound
    44
    45open Lax3.NeighborhoodCovers
    46open Lax199508.ColoringNumbers
    47
    48/-- Every graph has an `r`-neighborhood cover of radius `2r` and
    49degree at most its weak `2r`-coloring number. -/
    50axiom exists_neighborhoodCover_degree_wcol {n : ℕ}
    51 (G : SimpleGraph (Fin n)) (r : ℕ) :
    52 ∃ X : Fin n → Set (Fin n),
    53 IsNeighborhoodCover G r X (wcol G (2 * r))
    54
    55end Lax3.NeighborhoodCoverBound
    56
    Show Proof
    Formalization notes

    The statement is per-graph and class-free, with the degree bound wcolG(2r)wcol G (2r) — Lax199508's wcolwcol, not restated. It chooses an optimal ordering and applies the arbitrary-order construction Lax3.OrderedNeighborhoodCover.isNeighborhoodCoverwreachLax3.OrderedNeighborhoodCover.isNeighborhoodCover_wreach to it. That core names the clusters explicitly and accepts the supplied ordering's weak reachability bound; it is also the form the model-checking algorithm consumes for its computed ordering. The existential theorem composes with any wcol bound a consumer owns, including the subpolynomial bound for nowhere dense classes.

    The discharge shows that an optimal ordering ππ exists, then applies the core claim to the clusters w∣u∈wreachGπ(2r)w{w | u ∈ wreach G π (2r) w} with the bound (wreachGπ(2r)v).ncard≤wcolG(2r)(wreach G π (2r) v).ncard ≤ wcol G (2r). Covering and radius are the elementary walk arguments proved for the core. The computation of such a cover on the word RAM — including computing a good-enough ordering — is proved in the algorithmic layer and is not part of this claim.

    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…