Formalizing Structural Graph Theory in Lean 4

Nowhere-denseness convention. The conclusion uses Definition NowhereDense (Mählmann’s Definition 13.1, \(r\)-subdivided cliques as subgraphs), not the existing Definition NowhereDense (shallow topological minors). This matches the source verbatim and avoids detouring through the (folklore but non-trivial) equivalence of the two formulations. The bridge is available separately as Lemma NowhereDenseBridge.

Monadic-dependence convention. The hypothesis uses Definition MonadicDependence, which is the full clause (3) of Mählmann’s Theorem 2.3: excluding flipped star, clique, and half-graph \(r\)-crossings of order \(k\) and the comparability grid of order \(k\) as induced subgraphs. The proof uses only the star-crossing piece, bridging through the fact that the unflipped star \(r'\)-crossing is itself a flipped star \(r'\)-crossing (via the empty flip \(F = \emptyset\) in Definition Flip). The clique- and half-graph-crossing and comparability-grid pieces of clause (3) are present in the hypothesis but unused by this proof.

Small divergences from Mählmann’s written proof.

• Mählmann writes “\(r'\)-subdivided cliques are the same as star \(r'\)-crossings”; this is a typo for “\(r'\)-subdivided bicliques”. Star \(r'\)-crossings are built on bipartite roots, and the preceding case statement in Mählmann’s proof says “\(r'\)-subdivided biclique as induced subgraph”. We write “biclique” throughout.
• Mählmann’s proof elides the Step 1 reduction from \(r\)-subdivided cliques to \(r\)-subdivided bicliques (“It is easy to see that \(\mathcal{C}\) must also contain arbitrarily large \(r\)-subdivided bicliques as subgraphs”). We spell out the half-and-half partition argument.
• Mählmann’s proof elides the pigeonhole in Step 2 (where a single \(r' \in [r]\) is fixed across the infinitely many \(n\)). We spell it out, because it will matter for the Lean proof.
• Mählmann’s proof elides the \(r = 0\) edge case by implicitly treating “\(r\)-subdivided clique” as requiring \(r \geq 1\). We handle \(r = 0\) explicitly, because Definition NowhereDense ranges over all \(r \in \mathbb{N}\).
• Mählmann’s proof cites “Theorem 2.3” for the exclusion of star \(r'\)-crossings. Since we have taken clause (3) of Theorem 2.3 as the definition of monadic dependence, we cite Definition MonadicDependence directly and make the “unflipped is a special case of flipped” bridge explicit.

Proof-dep rationale. Definition Biclique, Definition Subdivision, Definition Flip, and Definition StarCrossing appear only in the proof (the statement refers only to weak sparseness, monadic dependence, and nowhere denseness, each of which re-exports these notions through its own ). They are therefore declared as proof_deps and not as statement_deps.

Phase 2 Lean encoding. The Contract.lean statement \[\texttt{IsWeaklySparse}\ C \to \texttt{IsMonadicallyDependent}\ C \to \texttt{IsNowhereDense}\ C\] chains the three class-level predicates directly. Each unfolds to an internally \(V\)-quantified universal (over [DecidableEq V] [Fintype V] graphs satisfying \(C\)), so the proof must handle the quantifier repackaging as it moves between hypotheses.

Lean-level bridge “unflipped = flipped-with-\(F = \bot\)”. Step 3b of the proof uses that an unflipped star \(r'\)-crossing is a flipped star \(r'\)-crossing via the empty symmetric relation \(F = \bot\). Spelled out in Lean: \[\texttt{flip (starCrossing k r') layer}\ \bot\ \texttt{h}\ \cong\ \texttt{starCrossing k r'}\] (the adjacency equation of the left graph reduces to the adjacency of starCrossing k r’ when \(F = \bot\)). A small helper lemma flip_bot will need to land in Full.lean; see formalization-notes.md.

Scope of this contract. The theorem is an implication between graph-class predicates; it does not expose any auxiliary construction. The entry has no public API surface beyond the theorem itself.