Graph minors, the Hadwiger number and Wagner planarity

Setting. Every declaration in this file lives in the SimpleGraph namespace. $V$ and $W$ are arbitrary types (possibly infinite, in arbitrary universes); no finiteness or decidability is assumed unless stated. A simple graph on a type is, as in Mathlib, an irreflexive symmetric adjacency relation; $u \sim_G v$ denotes adjacency in $G$.

Structure Minor H G. For a simple graph $H$ on $W$ and a simple graph $G$ on $V$, a minor witness of $H$ in $G$ consists of exactly the following data and conditions:

1. Branch sets. A function $B : W \to \mathcal P(V)$, $w \mapsto B_w \subseteq V$.
2. Pairwise disjointness. For all $w_1, w_2 \in W$ with $w_1 \neq w_2$: $B_{w_1} \cap B_{w_2} = \emptyset$.
3. Connectedness. For every $w \in W$, the induced subgraph $G[B_w]$ (vertex set $B_w$; two vertices of $B_w$ are adjacent iff they are adjacent in $G$) is connected in Mathlib's sense, which means both that $B_w \neq \emptyset$ and that any two vertices $u, v \in B_w$ are joined by a walk $u = v_0 \sim_G v_1 \sim_G \dots \sim_G v_k = v$ ($k \ge 0$ allowed) all of whose vertices lie in $B_w$.
4. Edge lifting. For all $w_1, w_2 \in W$: if $w_1 \sim_H w_2$, then there exist $v_1 \in B_{w_1}$ and $v_2 \in B_{w_2}$ with $v_1 \sim_G v_2$.

Nothing else is required: the branch sets need not cover $V$; no condition is imposed when $w_1 \not\sim_H w_2$ (edges of $G$ between $B_{w_1}$ and $B_{w_2}$ are allowed); if $W$ is empty, $B$ is the empty function and conditions 2–4 hold vacuously, so every graph $G$ admits a minor witness of the graph with no vertices. In the rest of the file "Nonempty (Minor H G)" means that at least one such witness exists; below I abbreviate this as "$H$ is a minor of $G$", always in exactly this sense.

hadwigerNumber G. Defined only when $V$ is a finite type (Fintype V), using classical decidability. It is the natural number

i.e. the largest $r$ with $0 \le r \le |V|$ such that $K_r$ — the complete graph on $\mathrm{Fin}\,r = \{0,\dots,r-1\}$, in which $i \sim j \iff i \neq j$ — is a minor of $G$ in the above sense, with the convention that the result is $0$ when no $r \in \{1,\dots,|V|\}$ qualifies. Since $r = 0$ always qualifies (empty vertex type, vacuous conditions), the value is exactly $\max\{\, r \le |V| : K_r \text{ is a minor of } G \,\}$; values $r > |V|$ are never examined.

K5. The complete graph on $\mathrm{Fin}\,5$: five vertices, all ten pairs of distinct vertices adjacent.

K33. Mathlib's completeBipartiteGraph (Fin 3) (Fin 3): the vertex type is the disjoint union $\mathrm{Fin}\,3 \sqcup \mathrm{Fin}\,3$ (six vertices, each tagged "left" or "right"), and $v \sim w$ iff ($v$ is left and $w$ is right) or ($v$ is right and $w$ is left). There are no edges inside a side; all nine left–right pairs are adjacent.

IsWagnerPlanar G. For a simple graph $G$ on an arbitrary type $V$ (no finiteness assumed), the proposition

Unfolded: there is no family $(B_w)_{w \in \mathrm{Fin}\,5}$ of pairwise disjoint subsets of $V$, each nonempty and connected inside $G$, such that for every two distinct indices $w_1 \ne w_2$ some vertex of $B_{w_1}$ is $G$-adjacent to some vertex of $B_{w_2}$; and there is no family $(B_w)_{w \in \mathrm{Fin}\,3 \sqcup \mathrm{Fin}\,3}$ of pairwise disjoint subsets of $V$, each nonempty and connected inside $G$, such that for every left index $w_1$ and every right index $w_2$ some vertex of $B_{w_1}$ is $G$-adjacent to some vertex of $B_{w_2}$. No other notion of planarity (embeddings in the plane, Euler's formula, etc.) appears in the definition.