Formalizing Structural Graph Theory in Lean 4

Scope. This entry bundles three informally-introduced notions with the main Definition 3.1: distance-\(r\) independence, the vertex deletion \(G - S\), and uniform quasi-wideness itself. The source introduces the first two in its preliminaries and only uses them here and in the proofs of Lemmas 3.3 / 3.4; co-locating them keeps the contract self-contained and avoids a thin “preliminaries” bucket. Catalog.Sparsity.Preliminaries retains only GraphClass.

DistIndependent. The walk-based formulation A.Pairwise (fun u v => ∀ (p : G.Walk u v), r < p.length) ensures that unreachable vertex pairs are always considered distance-\(r\) independent for every \(r\), matching the source convention that unreachable vertices have infinite distance. Mathlib’s SimpleGraph.dist returns \(0\) for unreachable pairs, which would give the wrong answer.

deleteVerts. We define deleteVerts G S as a SimpleGraph V (same vertex type) where adjacency requires both endpoints to lie outside \(S\). This avoids subtype coercions that would arise from G.induce Sc. The trade-off is that deleted vertices remain in the type but become isolated.

UniformlyQuasiWide. The Lean definition follows the source closely. The key encoding choices:

• The threshold function \(N_r\) is existentially quantified as N : ℕ → ℕ. The source writes \(N_r(m)\); we write N m after fixing \(r\).
• The separator bound \(s_r\) is existentially quantified as s : ℕ.
• The set \(B \subseteq A \setminus S\) is encoded as ↑B ⊆ ↑A \(\setminus\) ↑S, lifting Finset to Set for the set difference.
• Distance-\(r\) independence of \(B\) in \(G - S\) uses DistIndependent (deleteVerts G ↑S) r ↑B, now defined locally in this entry.

The source quantifies over “all \(m \in \mathbb{N}\), \(G \in \mathcal{C}\), and \(A \subseteq V(G)\) with \(|A| \geq N_r(m)\),” which we mirror exactly with the Lean binder order: \(m\), then type-polymorphic \(G\) with \(C\;G\), then \(A\) with the cardinality hypothesis.