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

Proof of `Neighborhood covers of weak coloring degree`

groundedproofs/Lax3Proofs/CoverConstruction.lean · lax-3

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Neighborhood covers of weak coloring degree (Theorem 6.2 of Grohe–Kreutzer–Siebertz, via their Lemma 6.9): every graph has, for every radius rr, an rr-neighborhood cover of radius 2r2r whose degree is at most its weak 2r2r-coloring number.

Proof strategy

Choose an ordering attaining wcolG(2r)wcol G (2r): the defining infimum is over a nonempty set of natural-number bounds, so it is attained. Apply Lax3.OrderedNeighborhoodCover.isNeighborhoodCoverwreachLax3.OrderedNeighborhoodCover.isNeighborhoodCover_wreach to that ordering and its bound. The arbitrary-order construction is discharged by isNeighborhoodCoverwreachisNeighborhoodCover_wreach above.