Formalizing Structural Graph Theory in Lean 4

The thesis uses \(r\)-subdivisions without explicit preliminaries. We fix the standard convention: subdividing an edge \(r\) times means inserting \(r\) fresh internal vertices, so the resulting path has length \(r+1\). In particular, \(H^{(0)} = H\) and \(H^{(1)}\) subdivides each edge once (a two-edge path per original edge). This matches Mählmann’s usage on p. 14, where a “star \(r\)-crossing of order \(n\)” is built from \(r\)-vertex paths between the bipartite roots — i.e. paths of length \(r + 1\).

We define “contains as subgraph” via an injection preserving edges (no constraint on non-edges), and “contains as induced subgraph” via an injection that preserves both edges and non-edges on its image. This is standard and matches the distinction Mählmann draws in the proof of Lemma 13.8 (p. 167), where he moves between “as a subgraph” and “as an induced subgraph”.

Open notational point. The thesis does not consistently name the principal vertices of a subdivision. We use “principal vertices” for the image of \(V(H) \subseteq V(H^{(r)})\) and “subdivision vertices” for the \(x^e_i\); this matches the star-\(r\)-crossing convention of “roots” vs. “path vertices” on p. 14 and the use of “principal vertices” in the proofs on pp. 167–168.

Lean scope cut: no abstract subdivide H r. In Lean, we do not formalize the general \(r\)-subdivision of an arbitrary graph \(H : \mathrm{SimpleGraph}\ V\). Only the two concrete instances subdividedClique n r and subdividedBiclique n r are provided. Reason: Mathlib’s SimpleGraph uses unordered edges (Sym2 V), so defining \(H^{(r)}\) generically requires orienting each edge before placing its \(r\) fresh path vertices — doable but requires Classical.choice or a LinearOrder V assumption, and contributes nothing to the target scope (Mählmann uses \(H^{(r)}\) only for \(H = K_n\) and \(H = K_{n,n}\)). The two concrete definitions side-step the orientation question by hard-coding the Fin n-based ordering in the vertex type.

Vertex-type shape. We use sum types rather than a discriminated dependent record:

• SubdividedCliqueVert n r := Fin n ⊕ ({p : Fin n × Fin n // p.1 < p.2} × Fin r)
• SubdividedBicliqueVert n r := (Fin n ⊕ Fin n) ⊕ ((Fin n × Fin n) × Fin r)

Sum types compose cleanly with Lean’s pattern-matcher and give decidable equality for free. The clique version uses the subtype {p : Fin n × Fin n // p.1 < p.2} to index unordered edges of \(K_n\); the biclique version indexes by Fin n × Fin n directly (ordered pair of left/right sides), which matches \(K_{n, n}\) having no diagonal.

Edge relation via SimpleGraph.fromRel. SimpleGraph.fromRel takes a relation \(R : V \to V \to Prop\) and builds the symmetric, irreflexive closure: adjacency is \(x \neq y \land (R\ x\ y \lor R\ y\ x)\). We only populate the “forward” direction of each edge pattern; the “backward” direction is handled by fromRel’s symmetrization. The catch-all | _, _ => False branch in the match handles all pairs whose reverse is already covered by an earlier clause (e.g. (.inr, .inl) reverses to (.inl, .inr)).