Formalizing Structural Graph Theory in Lean 4

The catalog already has Definition NowhereDense, which defines nowhere denseness via shallow topological minors: \(\omega_d(\mathcal{C}) < +\infty\) for every \(d \in \mathbb{N}\). Mählmann’s Definition 13.1 uses \(r\)-subdivided cliques as subgraphs instead. The two are classically known to be equivalent (with polynomially related parameters), but the equivalence is not entirely trivial.

We introduce a local Definition NowhereDense that tracks Mählmann’s statement verbatim. This keeps the statement of the target Lemma WeaklySparseMonDepIsNowhereDense (Lemma 13.7) and its proof faithful to the source. A sorried bridge lemma, Lemma NowhereDenseBridge, states the equivalence to Definition NowhereDense; its proof is out of scope for this work.

Lean encoding. The predicate IsNowhereDense : GraphClass → Prop is \[\forall\, r,\ \exists\, N,\ \forall\, V\ [\texttt{DecidableEq}]\ [\texttt{Fintype}]\ (G : \texttt{SimpleGraph } V),\ C\ G \to \neg (\texttt{subdividedClique } N\ r).\texttt{IsContained}\ G.\] The internal universe quantification over \(V\) (with decidable-equality and finiteness typeclasses) matches the GraphClass interpretation in Definition Preliminaries: a graph class is a property of graphs parameterized by the vertex type, not a syntactic marker. The [Fintype V] assumption makes subdivided-clique containment decidable, which is needed for later finite enumeration.

Reuse of subdividedClique. Dev.MonadicDependence.Subdivision.subdividedClique N r is the concrete graph we forbid. An alternative framing (“\(r\)-subdivision of any graph of order \(\geq N\)”) would require the general subdivide H r operator, which we scope-cut in Definition Subdivision; the concrete-clique version is equivalent for this definition because any subdivision of \(K_N\) is contained in any \(r\)-subdivision of a supergraph of \(K_N\).