Theorem 3.3 (Mader): for $t\le 7$, no $K_t$ minor $\Rightarrow$$|E|\le (t-2)n-\binom{t-1}{2}$

Note — non-blind read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the intended meaning. It is not independent or blind testimony, and no reviewer should treat it as such; an independent audit is still needed.

Let $t\in\mathbb N$ with $t\le 7$, let $V$ be a finite type with $n=|V|$, and $G$ a simple graph on $V$. Assume $t-2\le n$ (as integers, so this is automatic for $t\le 2$) and that $G$ has no $K_t$ minor. Then, computing in the integers, the number of edges of $G$ is at most $(t-2)n-\lfloor (t-1)(t-2)/2\rfloor$ (the floor is the integer division rounding toward $-\infty$). For $t=0$ the hypothesis “no $K_0$ minor” is never satisfied, so that case is vacuous. Here, for graphs $H$ on a vertex type $W$ and $G$ on a vertex type $V$, “$H$ is a minor of $G$” means: there are sets $B_w\subseteq V$ ($w\in W$) such that (i) each $B_w$ induces a connected subgraph of $G$ (in particular $B_w\neq\emptyset$), (ii) $B_{w_1}\cap B_{w_2}=\emptyset$ whenever $w_1\neq w_2$, and (iii) whenever $w_1w_2$ is an edge of $H$, some vertex of $B_{w_1}$ is adjacent in $G$ to some vertex of $B_{w_2}$. “$G$ has a $K_t$ minor” means the complete graph on the $t$-element set $\{0,\dots,t-1\}$ is a minor of $G$ in this sense (so: $t$ pairwise disjoint connected nonempty vertex sets, every two joined by an edge of $G$; for $t=0$ this holds for every graph). “$k$-colourable” means there is a map from $V$ to a $k$-element set of colours giving adjacent vertices different colours (for $k=0$ this forces $V=\emptyset$). All graphs are simple (no loops, no multiple edges).