Formalizing Structural Graph Theory in Lean 4

The proof constructs a vertex ordering by a greedy procedure (always removing the vertex with smallest \(b_r\)) and argues by contradiction: if admissibility is too large, the path families can be combined with an independent set in the auxiliary graph \(H\) to build a depth-\((r-1)\) topological minor that is too dense, contradicting \(\widetilde{\nabla}_{r-1}(G) = d\).

The cube in \(d^3\) comes from: \(d\) contributes to the size of \(K\) (internal vertices), to the edge count of \(H\) (bounding \(|I|\) via a \((2d+1)\)-coloring), and to the final density comparison.

Lean encoding: reformulation.

The source states \(\operatorname{adm}_r(G) \leq 1 + 6r \lceil \widetilde{\nabla}_{r-1}(G) \rceil^3\). The contract avoids defining the topological grad \(\widetilde{\nabla}\) as a supremum over types and instead takes an explicit integer bound \(d\) with a hypothesis: \[\forall H,\; H \preccurlyeq^{\mathrm{top}}_{r-1} G \implies |E(H)| \leq d \cdot |V(H)| \quad \Longrightarrow \quad \exists\, \sigma,\; \operatorname{adm}_r(G,\sigma) \leq 1 + 6rd^3.\] Setting \(d = \lceil \widetilde{\nabla}_{r-1}(G) \rceil\) recovers the source statement exactly. The hypothesis-based form is more directly usable downstream.

The result is existential over orderings (\(\exists\;\texttt{ord}\)) rather than using a graph-level \(\operatorname{adm}_r(G)\).