Challenge 6: the $(r/2)$-well-quasi-ordering statement, alternating between planar and all finite graphs

TenChallenges.statement_06 r. A proposition depending on an ordinal $r$. (The ordinal lives in the lowest universe: the graph types used below are in Type, which forces the universe of Ordinal.) It is

an if-then-else on propositions (decided classically); 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$).

Putting it together. statement_06 r asserts: if $r \bmod 2 = 0$, then 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$, where $\le^*$ is built from $\le\ =\ \preceq_{\mathrm{planar}}$; otherwise ($r \bmod 2 = 1$), 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$, where $\le^*$ is built from $\le\ =\ \preceq_{\mathrm{fin}}$. For instance, statement_06 0 says that every sequence $(n_0, G_0), (n_1, G_1), \dots$ of finite Wagner-planar graphs has $i<j$ with $G_i$ a minor of $G_j$ (minor witness as above); statement_06 1 says the same for every sequence of all finite simple graphs; statement_06 2 says that every sequence $S_0, S_1, \dots$ of nonempty sets of finite Wagner-planar graphs has $i<j$ such that every $G \in S_i$ is a minor of some $H \in S_j$; statement_06 3 says the same for nonempty sets of arbitrary finite graphs; and statement_06 \omega concerns sequences of tagged pairs $(i, x)$ with $x$ at some finite level $k$ over planar graphs, compared by first discarding both tags and then applying the clauses above at the two (possibly different) finite levels.