Formalizing Structural Graph Theory in Lean 4

Role in the DAG. The target Lemma WeaklySparseMonDepIsNowhereDense (Lemma 13.7) concludes nowhere-denseness in the sense of Definition NowhereDense. Users who want the catalog’s standard Definition NowhereDense conclusion (in terms of depth-\(d\) shallow minors) compose with this bridge lemma. The bridge is not needed for the target Lemma 13.7 itself.

Folklore source. The equivalence is folklore (not stated as such in Mählmann’s thesis). The nearest textbook reference is Nešetřil–Ossona de Mendez, Sparsity, Chapters 5 and 12. Both source.tex and statement.tex state only what is actually true about the parameter relation, which is weaker than what the folklore is sometimes claimed to give (see below).

Parameter relation is functional, not polynomial. An earlier draft of this entry claimed the parameter functions are polynomially related. That claim is incorrect. The forward direction (shallow-minor bound \(\Rightarrow\) subdivision bound) is indeed linear: an \(r\)-subdivided clique is a depth-\(\lceil r/2 \rceil\) topological minor of the clique it subdivides, so \(N_r \leq \omega_{\lceil r/2 \rceil}(\mathcal{C}) + 1\). The backward direction (subdivision bound \(\Rightarrow\) shallow-minor bound) goes through a Ramsey argument — BFS trees rooted at branch-set centres, bridge edges, then iterative Ramsey over the branching pattern of the induced centre-to-centre paths — and the extracted bound on \(t\) is of Ramsey type in the depth parameter. No polynomial bound is known in general, and the standard proof does not deliver one. The statement has been corrected accordingly.

Lean encoding (Phase 2). The Lean Contract.lean states only the qualitative equivalence \[\texttt{Dev.MonadicDependence.NowhereDense.IsNowhereDense}\ C \leftrightarrow \texttt{Catalog.Sparsity.NowhereDense.IsNowhereDense}\ C,\] without any quantitative parameter-relation clause. This is the standard form used in the literature and avoids committing to a particular Ramsey-type bound in the contract surface. If downstream work ever needs an explicit bounding function, a quantitative refinement can be stated as a separate entry without reopening this one.

Proof scope. proof.tex gives a proof sketch at the strategy level: the forward direction is written out fully (it is a short observation); the backward direction is broken into five labelled steps (BFS trees, length-normalising Ramsey, iterative branching-pattern Ramsey, reduction to a canonical internally-disjoint subdivision, contradiction with the subdivision bound). The exact Ramsey bookkeeping and the precise function \(t(d, (N_r)_{r \leq 2d+1})\) are not pinned down in the sketch; they will be made explicit in the Lean formalization (Phases 2–3).