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

Proof of `Neighborhood covers from vertex orderings`

groundedproofs/Lax3Proofs/CoverConstruction.lean · lax-3

What this proof establishes

no assumptions

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

The cover of an ordering (Lemma 6.9 of Grohe–Kreutzer–Siebertz, the parametric core of their Theorem 6.2). For any ordering ππ whose weak 2r2r-reachability sets have at most kk elements, the fibers of weak 2r2r-reachability form an rr-neighborhood cover of radius 2r2r and degree at most kk.

Proof strategy

For the supplied ordering ππ, let the cluster of uu be wuwreachGπ(2r)w{w | u ∈ wreach G π (2r) w}, the set of vertices from which uu is weakly 2r2r-reachable.

The degree bound is the definition read backwards: the set of clusters containing vv is indexed by uuwreachGπ(2r)v{u | u ∈ wreach G π (2r) v}, which is wreachGπ(2r)vwreach G π (2r) v itself, of size at most kk by hypothesis. The radius bound drops the minimality clause: a vertex in the cluster of uu reaches uu by a walk of length at most 2r2r, which reversed puts it in the 2r2r-ball of uu.

Covering is the only real argument. Given vv, let uu be a ππ-minimal vertex of the rr-ball of vv, which is nonempty and finite. For ww in that ball, concatenate the reversed ball walk wvw → v with the ball walk vuv → u: a walk of length at most 2r2r from ww to uu. Every vertex on it lies on one of the two halves, and cutting a walk of length at most rr at any of its vertices shows that vertex to be within distance rr of both endpoints — so the whole support stays inside the rr-ball of vv, where uu is ππ-minimal. Hence uu is weakly 2r2r-reachable from ww, i.e. ww lies in the cluster of uu.