Formalizing Structural Graph Theory in Lean 4

Faithfulness. The thesis proves Lemma 13.8 in a fairly compact style, defining the coloring by atomic types only implicitly (“by \((*)\)”) and reasoning by repeated halvings of \(I\) and \(J\) each time a semi-induced biclique would be exposed. Our proof.tex spells these steps out and makes explicit the induction on the shortest-path length \(r'\). No step changes Mählmann’s argument; we only expose the implicit coloring and the fact that each “large biclique” alternative short-circuits the proof.

Bound shape. Mählmann uses \(U\)-notation: the output size is some \(U_r(n)\), monotone and unbounded in \(n\). Iterated halvings preserve this property, so the final bound is still of the form \(U_r(n)\). A Lean formalization will need to pick a concrete bound; we leave this as a Phase 2/3 design choice.

Typo in the thesis. The last case of the proof of Lemma 13.7 writes “\(r'\)-subdivided cliques are the same as star \(r'\)-crossings”; it should read “\(r'\)-subdivided bicliques are the same as star \(r'\)-crossings”. Our statement of Lemma 13.8 uses “biclique” throughout to match the actual geometry. See Lemma WeaklySparseMonDepIsNowhereDense’s review.tex for the corresponding note on the Lemma 13.7 proof.

Lean encoding: containment relations. The two alternatives use Mathlib’s two different containment relations:

• “contains the biclique of order \(U_r(n)\) as a subgraph” is (biclique (U n)).IsContained G (non-induced subgraph);
• “contains an \(r'\)-subdivided biclique of order \(U_r(n)\) as an induced subgraph” is (subdividedBiclique (U n) r’).IsIndContained G.

The distinction is load-bearing: the induced-subgraph alternative is what feeds the IsFlippedStarCrossing exclusion from monadic dependence in Lemma 13.7’s Step 3b, and a subgraph witness would not suffice there.

\(U\)-notation packaging. Same shape as Lemma BipartiteRamsey: an existentially packaged \((U, \texttt{Monotone}, \text{unbounded})\).

Statement constraints on the ambient graph \(G\). The containment hypothesis (subdividedBiclique n r).IsContained G is stated over arbitrary \(V\) with [DecidableEq V] [Fintype V], matching the assumption shape used in GraphClass (and hence in IsNowhereDense / IsMonadicallyDependent / IsWeaklySparse). This lets the statement compose directly with these class-level predicates in the proof of Lemma 13.7.