Lax3.NeighborhoodCoverBound

Neighborhood covers of weak coloring degree

concepts/Lax3/NeighborhoodCoverBound.lean · lax-3

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

- thm✓Lax3.OrderedNeighborhoodCover
→
thm✓Lax3.NeighborhoodCoverBound
⊢Lax3Proofs.CoverConstruction.exists_neighborhoodCover_degree_wcol

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 Lax12'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 Lax12 is uniform over subgraphs of members.

Lean source view on GitHub

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

Show Proof

Formalization notes

The statement is per-graph and class-free, with the degree bound $wcol G (2r)$ — Lax12's $wcol$ , not restated. It chooses an optimal ordering and applies the arbitrary-order construction $Lax3.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 ∈ wreach G π (2r) w}$ with the bound $(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

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…

Lax Lean Archive