Formalizing Structural Graph Theory in Lean 4

Faithfulness to the source. Mählmann’s Def. 13.5 (p. 167) is a single sentence: a class \(\mathcal{C}\) is weakly sparse iff there is a bound \(k\) such that no graph in \(\mathcal{C}\) contains the biclique of order \(k\) as a subgraph. We reproduce this verbatim; no structural changes.

“Subgraph” convention. “Contains as a subgraph” is SimpleGraph.IsContained from Mathlib (scoped notation ⊑), which is non-induced subgraph containment: existence of an injective graph homomorphism biclique k →g G. This matches Mählmann’s usage (p. 22 for “biclique”, p. 167 for the definition) — no induced-subgraph constraint.

Graph class boilerplate. The definition is quantified over a GraphClass (from Definition Preliminaries); see that entry for the discussion of why a graph class is a family of graphs with fixed structure, rather than a syntactic class. Each instantiation uses the [DecidableEq V] [Fintype V] typeclass constraints implicit in the GraphClass definition; these are needed for SimpleGraph.IsContained to unfold via finite case analysis when concretely needed.

Role in the DAG. Consumed by the target Lemma WeaklySparseMonDepIsNowhereDense (Lemma 13.7). Used twice in that proof: the \(r = 0\) case (cliques contain bicliques of half their order) and Step 3a (the biclique-as-subgraph alternative of the Ramsey dichotomy).

No separate “strongly sparse”. Mählmann does not introduce a strongly-sparse notion, and neither do we. Weak sparseness is a minimal-form forbidden-substructure condition used as a hypothesis throughout Chapter 13.