Formalizing Structural Graph Theory in Lean 4

A graph \(H\) is a topological minor of \(G\), written \(H \preccurlyeq^{\mathrm{top}} G\), if there is a topological minor model \(\psi\) of \(H\) in \(G\): a map \(\psi\) which assigns to every vertex \(v \in V(H)\) a vertex \(\psi(v) \in V(G)\) and to every edge \(e \in E(H)\) a path \(\psi(e)\) in \(G\) such that:

1. if \(u, v \in V(H)\) with \(u \neq v\) then \(\psi(v) \neq \psi(u)\),
2. if \(e = uv \in E(H)\) then \(\psi(e)\) is a path with endpoints \(u\) and \(v\), and
3. if \(e, e' \in E(H)\) with \(e \neq e'\), then \(\psi(e)\) and \(\psi(e')\) are internally vertex disjoint.

The vertex \(\psi(v)\) is the pin of \(v\).

A graph \(H\) is a topological depth-\(d\) minor of \(G\), written \(H \preccurlyeq^{\mathrm{top}}_d G\), if there is a topological minor model \(\psi\) of \(H\) in \(G\) such that the paths \(\psi(e)\) have length at most \(2d + 1\) for all \(e \in E(H)\).

Every topological depth-\(d\) minor is a depth-\(d\) minor (Definition ShallowMinor).

For a graph \(G\) and \(d \in \mathbb{N}\): \[\widetilde{\nabla}_d(G) := \sup \left\{ \frac{|E(H)|}{|V(H)|} : H \preccurlyeq^{\mathrm{top}}_d G \right\}, \qquad \widetilde{\omega}_d(G) := \sup \left\{ t : K_t \preccurlyeq^{\mathrm{top}}_d G \right\}.\] For a graph class \(\mathcal{C}\) and \(d \in \mathbb{N}\): \[\widetilde{\nabla}_d(\mathcal{C}) := \sup_{G \in \mathcal{C}} \widetilde{\nabla}_d(G), \qquad \widetilde{\omega}_d(\mathcal{C}) := \sup_{G \in \mathcal{C}} \widetilde{\omega}_d(G).\]