Formalizing Structural Graph Theory in Lean 4

Theorem 2.3 as definition. Mählmann’s Theorem 2.3 (p. 9) proves a four-way equivalence for a graph class \(\mathcal{C}\):

1. \(\mathcal{C}\) is monadically dependent (i.e. does not transduce the class of all graphs; model-theoretic),
2. \(\mathcal{C}\) is flip-breakable (Definition 2.10; combinatorial),
3. \(\mathcal{C}\) excludes the four patterns in this entry’s statement (forbidden induced subgraphs; combinatorial),
4. the hereditary closure of \(\mathcal{C}\) does not efficiently interpret the class of all graphs (algorithmic).

Per the user’s direction, we take clause (3) verbatim as the definition of monadic dependence in this formalization. This avoids the model-theoretic notions (transductions, interpretations) needed for clauses (1) and (4), and the flip-breakability construction needed for clause (2). Equivalences with clauses (1), (2), (4) remain out of scope for this work.

Faithful coverage. All four components of clause (3) are included: the flipped star, clique, and half-graph \(r\)-crossings and the (unflipped) comparability grid. Mählmann explains (p. 15) why the comparability grid needs no flipped variant: any huge flipped comparability grid contains a still large unflipped comparability grid as an induced subgraph, so flipping does not add strength.

Unflipped crossings are included. Taking \(F = \emptyset\) in Definition Flip yields the identity flip, so an unflipped star / clique / half-graph \(r\)-crossing is a flipped \(X\) \(r\)-crossing via the trivial flip. In particular, a monadically dependent class excludes arbitrarily large unflipped star \(r\)-crossings as induced subgraphs, which is the specific consequence the proof of Lemma WeaklySparseMonDepIsNowhereDense (Lemma 13.7) relies on.

Edge case \(r = 0\). Mählmann’s clause (3) is stated for \(r \geq 1\) because the star / clique / half-graph \(r\)-crossing is only defined for \(r \geq 1\) (see Definition StarCrossing). We keep this convention. For the proof of Lemma 13.7, the missing \(r = 0\) case is handled separately (cliques of arbitrarily large order contain bicliques of half their order, which contradicts weak sparseness without needing monadic dependence).

Lean encoding: uniform quantification over the flip. Rather than introducing three separate IsFlippedXCrossing predicates and quantifying over them, the Lean definition inlines the flip structure: \[\forall\ F\ (\mathrm{Fsymm} : \texttt{Symmetric } F),\ \neg\ (\texttt{flip (XCrossing k r) layer } F\ \mathrm{Fsymm}) .\texttt{IsIndContained}\ G.\] This is equivalent to Mählmann’s quantification over flipped \(X\)-crossings (every flipped \(X\)-crossing of order \(k\) is of this shape, and isomorphic graphs are equivalent modulo IsIndContained) but avoids an extra layer of indirection through IsFlippedXCrossing predicates. The definition therefore does not import StarCrossing.IsFlippedStarCrossing and its siblings.

\(r \geq 1\) as a hypothesis. The \(1 \leq r\) hypothesis is threaded through the outer \(\forall r\) and is needed because the three XCrossing k r definitions are only meaningful for \(r \geq 1\). The clause is a single \(\forall r, 1 \leq r \to \exists k, \ldots\), matching the source’s “for every \(r \geq 1\)”.

[DecidableEq V] [Fintype V] assumptions. These come from the GraphClass interface; they let IsIndContained reduce to a decidable property when the ambient graph is finite. No separate hypothesis is carried by the definition of monadic dependence itself.