Finite graphs are $\alpha$-well-quasi-ordered under minors for every ordinal $\alpha$

TenChallenges.challenge_06. The theorem asserts

where $r$ ranges over all ordinals (of the lowest universe, forced by the graph types living in Type), and statement_06 r is

The declaration carries no proof in the file: its proof term is the placeholder sorry. Every ingredient is unfolded below.

Ordinal division and remainder. r / 2 and r % 2 are Mathlib's ordinal division and remainder: $r/2 = \sup\{\, q : 2\cdot q \le r \,\}$ and $r \bmod 2 = r - 2\cdot(r/2)$ (ordinal subtraction). Together these make $r/2$ the unique ordinal $q$ and $r \bmod 2$ the unique ordinal $s$ with $r = 2\cdot q + s$ and $s < 2$, so $r \bmod 2 \in \{0, 1\}$. Multiplication is ordinal multiplication with $2$ on the left ($2 \cdot q$ is "$q$ copies of two points"): $2\cdot 0 = 0$, $2 \cdot n = 2n$ for finite $n$, and $2\cdot\lambda = \lambda$ for every limit ordinal $\lambda$. Concretely, writing $r$ uniquely as $r = \lambda + n$ with $\lambda$ either $0$ or a limit ordinal and $n \in \mathbb N$, one has $r/2 = \lambda + \lfloor n/2 \rfloor$ and $r \bmod 2 = n \bmod 2$. So the first branch applies iff $n$ is even (level $\lambda + n/2$) and the second iff $n$ is odd (level $\lambda + (n-1)/2$). Examples: $r=0 \mapsto$ level $0$, planar; $r=1 \mapsto$ level $0$, all finite graphs; $r=2 \mapsto$ level $1$, planar; $r=3 \mapsto$ level $1$, all finite graphs; $r=\omega \mapsto$ level $\omega$, planar; $r=\omega+1 \mapsto$ level $\omega$, all finite graphs; $r=\omega+2 \mapsto$ level $\omega+1$, planar.

The two base types and relations (from item TenChallenges_AlphaWQO, which builds on item TenChallenges_Minor).

• FiniteGraph is the type of pairs $(n, G)$ with $n \in \mathbb N$ (including $n = 0$) and $G$ a simple graph (irreflexive symmetric adjacency) on $\mathrm{Fin}\,n = \{0, \dots, n-1\}$; elements are pairs, not isomorphism classes. The relation $\preceq_{\mathrm{fin}}$ (FiniteGraph.MinorLE) is: $(n, G) \preceq_{\mathrm{fin}} (m, H)$ iff there exists a minor witness of $G$ in $H$, namely a family $(B_w)_{w \in \mathrm{Fin}\,n}$ of subsets of $\mathrm{Fin}\,m$ with (i) $B_{w_1} \cap B_{w_2} = \emptyset$ whenever $w_1 \neq w_2$; (ii) each $B_w$ nonempty and any two of its vertices joined by a walk of $H$ all of whose vertices lie in $B_w$; (iii) for every edge $w_1 \sim_G w_2$ there are $v_1 \in B_{w_1}$ and $v_2 \in B_{w_2}$ with $v_1 \sim_H v_2$. Nothing is required for non-edges of $G$, and the $B_w$ need not cover $\mathrm{Fin}\,m$. No reflexivity or transitivity of $\preceq_{\mathrm{fin}}$ is assumed or used.
• PlanarGraph is the subtype of those $(n, G) \in$ FiniteGraph such that there is no minor witness of $K_5$ (the complete graph on $\mathrm{Fin}\,5$, all pairs of distinct vertices adjacent) in $G$ and no minor witness of $K_{3,3}$ (vertex type $\mathrm{Fin}\,3 \sqcup \mathrm{Fin}\,3$, exactly the left–right pairs adjacent) in $G$ — "planar" means only this (Wagner-style) condition, nothing about embeddings. The relation $\preceq_{\mathrm{planar}}$ (PlanarGraph.MinorLE) is $\preceq_{\mathrm{fin}}$ applied to the underlying pairs.

The hierarchy. For a type $Q$ and an ordinal $o$, $V^*_o(Q)$ (VStar Q o) is defined by transfinite recursion: $V^*_0(Q) = Q$; $V^*_{o+1}(Q)$ is the type of nonempty subsets of $V^*_o(Q)$; and for $o$ a limit ordinal ($o \neq 0$ and not a successor) $V^*_o(Q)$ is the disjoint union $\sum_{\beta < o} V^*_\beta(Q)$ (formally indexed by the canonical well-ordered type of order type $o$, each index $i$ standing for the ordinal $\beta = \operatorname{typein}(i) < o$), whose elements are tagged pairs $(i, x)$ with $x \in V^*_\beta(Q)$.

The game relation. For a base relation $\le$ on $Q$, the heterogeneous relation $X \le^*_{a,b} Y$ (leStar le a X b Y, with $X \in V^*_a(Q)$ and $Y \in V^*_b(Q)$) is defined by recursion on $a$ and then on $b$, by exactly these clauses:

• $a = 0$, $b = 0$ ($X, Y \in Q$): $\ X \le Y$.
• $a = 0$, $b = \beta + 1$: $\ \exists\, y \in Y,\ X \le^*_{0,\beta} y$.
• $a = 0$, $b$ limit, $Y = (i, y)$, $\beta = \operatorname{typein}(i)$: $\ X \le^*_{0,\beta} y$.
• $a = \alpha+1$, $b = 0$: $\ \forall\, x \in X,\ x \le^*_{\alpha,0} Y$.
• $a = \alpha+1$, $b = \beta+1$: $\ \forall\, x \in X,\ \exists\, y \in Y,\ x \le^*_{\alpha,\beta} y$.
• $a = \alpha+1$, $b$ limit, $Y = (i, y)$, $\beta = \operatorname{typein}(i)$: $\ X \le^*_{\alpha+1,\beta} y$.
• $a$ limit, $X = (i, x)$, $\alpha' = \operatorname{typein}(i)$: $\ x \le^*_{\alpha',b} Y$ (for every $b$ and $Y$).

The well-quasi-order condition. IsWQO of a relation $R$ on a type $T$ means: for every sequence $f : \mathbb N \to T$ there exist $i < j$ with $R(f_i, f_j)$ (strict $i<j$; no axioms on $R$). IsAlphaWQO le a means IsWQO of the relation $X \mapsto Y \mapsto X \le^*_{a,a} Y$ on $V^*_a(Q)$ (both sides at the same level $a$).

What the universal quantifier amounts to. For $r \bmod 2 = 0$ the claim is: for every sequence $f : \mathbb N \to V^*_{r/2}(\mathrm{PlanarGraph})$ there exist $i<j$ with $f_i \le^*_{r/2,\,r/2} f_j$ (with $\le\ =\ \preceq_{\mathrm{planar}}$ at the bottom); for $r \bmod 2 = 1$ it is: for every sequence $f : \mathbb N \to V^*_{r/2}(\mathrm{FiniteGraph})$ there exist $i<j$ with $f_i \le^*_{r/2,\,r/2} f_j$ (with $\le\ =\ \preceq_{\mathrm{fin}}$ at the bottom). Every ordinal $q = \lambda + k$ ($\lambda$ zero or a limit, $k \in \mathbb N$) arises as $r/2$ both from $r = \lambda + 2k$ (remainder $0$) and from $r = \lambda + 2k + 1$ (remainder $1$). Hence the statement "for all $r$" is equivalent to: for every ordinal $q$, both $\mathrm{IsAlphaWQO}(\preceq_{\mathrm{planar}}, q)$ and $\mathrm{IsAlphaWQO}(\preceq_{\mathrm{fin}}, q)$ hold. In particular it includes, at $q = 0$: every sequence of finite Wagner-planar graphs, and every sequence of finite simple graphs, has $i<j$ with the $i$-th a minor of the $j$-th; at $q = 1$: every sequence $S_0, S_1, \dots$ of nonempty sets of such graphs has $i<j$ with every $G \in S_i$ a minor of some $H \in S_j$; and so on through all successor and limit levels $q$, including those of uncountable cofinality, with the limit-level comparison obtained by discarding the tags and comparing the underlying elements at their own (possibly different) levels by the clauses above.