Formalizing Structural Graph Theory in Lean 4

The source states Lemma 3.5 as an iff: for a distance-\(2j\) independent set \(A\) in \(G\), contracting the distance-\(j\) neighborhoods gives a depth-\(j\) minor \(H\) such that a subset of \(A\) is distance-\((2j+1)\) independent in \(G\) if and only if it is distance-\(1\) independent (i.e., an independent set) in \(H\).

The Lean contract uses a consequence form: the minor \(H\) exists, \(|A|\) vertices fit in \(H\), and any independent set of size \(m\) in \(H\) lifts back to a distance-\((2j+1)\) independent subset of \(A\) of the same size. The reverse direction (distance-\((2j+1)\) in \(G\) implies distance-\(1\) in \(H\)) is not stated because the densification proof only uses the forward direction.

Quantifier structure. The existential binds a new vertex type \(W\), instances, a graph \(H\), and the claims about \(H\). The type \(W\) may differ from \(V\) because the contraction quotient changes the vertex set. The condition \(|A| \leq |W|\) ensures \(H\) has at least as many vertices as \(A\), which is needed for applying Ramsey’s theorem in \(H\) during the densification proof.