Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax3.OrderedNeighborhoodCover

Neighborhood covers from vertex orderings

concepts/Lax3/OrderedNeighborhoodCover.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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    Any vertex ordering whose weak 2r-reachability sets have size at most k gives an r-neighborhood cover of radius 2r and degree at most k. The cluster of a vertex u consists of the vertices from which u is weakly 2r-reachable.

    This is the arbitrary-order construction of Lemma 6.9 of Grohe–Kreutzer–Siebertz. The model-checking algorithm uses it for the ordering it computes. The companion theorem Lax3.NeighborhoodCoverBound.existsneighborhoodCoverdegreewcolLax3.NeighborhoodCoverBound.exists_neighborhoodCover_degree_wcol uses it for an optimal ordering, obtaining the weak coloring number itself as the degree bound.

    Lean source view on GitHub

    1import Lax3.NeighborhoodCovers
    2import Lax12.ColoringNumbers
    3
    4/-!
    5---
    6title: Neighborhood covers from vertex orderings
    7type: theorem
    8---
    9Any vertex ordering whose weak 2*r*-reachability sets have size at most
    10*k* gives an *r*-neighborhood cover of radius 2*r* and degree at most
    11*k*. The cluster of a vertex *u* consists of the vertices from which
    12*u* is weakly 2*r*-reachable.
    13
    14This is the arbitrary-order construction of Lemma 6.9 of
    15Grohe–Kreutzer–Siebertz. The model-checking algorithm uses it for the
    16ordering it computes. The companion theorem
    17`Lax3.NeighborhoodCoverBound.exists_neighborhoodCover_degree_wcol`
    18uses it for an optimal ordering, obtaining the weak coloring number
    19itself as the degree bound.
    20
    21# Formalization notes
    22
    23The statement is per-graph and class-free, with the ordering `π` and
    24bound `k` supplied explicitly. The cluster of `u` is
    25`{w | u ∈ wreach G π (2r) w}`, using Lax12's weak reachability sets.
    26The hypothesis directly bounds the number of clusters containing a
    27given vertex. The radius condition follows from reversing a weak
    28reachability walk. For covering, choose a `π`-minimal vertex of an
    29`r`-ball; every other vertex of the ball reaches it along a walk of
    30length at most `2r` whose support remains in the ball.
    31
    32The claim is discharged by
    33`Lax3Proofs.CoverConstruction.isNeighborhoodCover_wreach`. Both the
    34existential cover theorem and the algorithm consume this interface,
    35sharing the same proved construction.
    36-/
    37
    38namespace Lax3.OrderedNeighborhoodCover
    39
    40open Lax3.NeighborhoodCovers
    41open Lax12.ColoringNumbers
    42
    43/-- The fibers of weak `2r`-reachability under any ordering `π` form
    44an `r`-neighborhood cover of radius `2r` and degree at most `k`,
    45provided every weak `2r`-reachability set has size at most `k`.
    46This is the arbitrary-order construction of Lemma 6.9 of
    47Grohe–Kreutzer–Siebertz, used both by the algorithm with its computed
    48ordering and by the existential cover theorem with an optimal one. -/
    49axiom isNeighborhoodCover_wreach {n : ℕ} (G : SimpleGraph (Fin n)) (r k : ℕ)
    50 (π : Equiv.Perm (Fin n)) (hk : ∀ v, (wreach G π (2 * r) v).ncard ≤ k) :
    51 IsNeighborhoodCover G r (fun u => {w | u ∈ wreach G π (2 * r) w}) k
    52
    53end Lax3.OrderedNeighborhoodCover
    54
    Show Proof

    Formalization notes

    The statement is per-graph and class-free, with the ordering ππ and bound kk supplied explicitly. The cluster of uu is w∣u∈wreachGπ(2r)w{w | u ∈ wreach G π (2r) w}, using Lax12's weak reachability sets. The hypothesis directly bounds the number of clusters containing a given vertex. The radius condition follows from reversing a weak reachability walk. For covering, choose a ππ-minimal vertex of an rr-ball; every other vertex of the ball reaches it along a walk of length at most 2r2r whose support remains in the ball.

    The claim is discharged by Lax3Proofs.CoverConstruction.isNeighborhoodCoverwreachLax3Proofs.CoverConstruction.isNeighborhoodCover_wreach. Both the existential cover theorem and the algorithm consume this interface, sharing the same proved construction.

    Builds on

    Used by

    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…