Well-quasi-orders, the cumulative hierarchy $V^*_\alpha(Q)$, $\alpha$-well-quasi-ordering, finite and planar graphs under minors

Setting. $Q$ is a type in a universe $u$ and all ordinals are taken in the same universe $u$. The file imports item TenChallenges_Minor; its notions are unfolded where used. $\mathbb N = \{0,1,2,\dots\}$.

IsWQO le. For an arbitrary binary relation $\le$ on $Q$ (written $x \le y$ for le x y; no reflexivity, transitivity or antisymmetry is assumed anywhere in the file):

$$\forall f : \mathbb N \to Q,\ \ \exists\, i, j \in \mathbb N,\ \ i < j \ \wedge\ f_i \le f_j .$$

The inequality $i<j$ is strict. If $Q$ is empty the condition holds vacuously (there is no sequence).

VStar Q o. A type $V^*_o(Q)$ (in universe $u$) for every ordinal $o$, defined by transfinite recursion on $o$ (Ordinal.limitRecOn, whose zero / successor / limit clauses are exactly the three rules below):

• $V^*_0(Q) = Q$.
• $V^*_{o+1}(Q) = \{\, S \subseteq V^*_o(Q) \;:\; S \neq \emptyset \,\}$, the type of nonempty subsets of level $o$ (every successor ordinal is of the form $o+1$, so this covers every successor level).
• For $o$ a limit ordinal (meaning $o \neq 0$ and $o$ is not a successor): $V^*_o(Q) = \sum_{i \in o^{\mathsf T}} V^*_{\operatorname{typein}(i)}(Q)$, where $o^{\mathsf T}$ (o.ToType) is Mathlib's canonical well-ordered type of order type $o$ and $\operatorname{typein}(i) < o$ is the ordinal position of $i$ in it (the order type of $\{ j \in o^{\mathsf T} : j < i \}$); as $i$ ranges over $o^{\mathsf T}$, $\operatorname{typein}(i)$ ranges bijectively over all ordinals $\beta < o$. So an element of a limit level is a tagged pair $(i, x)$ with $x \in V^*_\beta(Q)$, $\beta = \operatorname{typein}(i) < o$: the disjoint union of all strictly lower levels.

The theorems VStar_zero, VStar_succ (stated with Order.succ o, which for ordinals is $o+1$) and VStar_limit (hypothesis: $o$ is a limit ordinal) assert precisely these three equalities of types. Edge cases: if $Q$ is empty then every level is empty (no nonempty subset of an empty type exists, and a disjoint union of empty types is empty); if $Q$ is nonempty then every level is nonempty.

leStar le a. For an ordinal $a$, a function $V^*_a(Q) \to \big(\forall b,\ V^*_b(Q) \to \mathrm{Prop}\big)$. Write $X \le^*_{a,b} Y$ for leStar le a X b Y, where $X \in V^*_a(Q)$ and $Y \in V^*_b(Q)$; this is a heterogeneous relation between elements of possibly different levels $a$ and $b$. It is defined by transfinite recursion on $a$ and, inside each case, by transfinite recursion on $b$. The casts in the code only transport elements along the three type equalities above, so $X$ and $Y$ are read through them below. The complete case list is:

Case $a = 0$ ($X \in Q$):

• $b = 0$ ($Y \in Q$): $\ X \le^*_{0,0} Y \iff X \le Y$ (the base relation).
• $b = \beta+1$ ($Y$ a nonempty subset of $V^*_\beta(Q)$): $\ X \le^*_{0,\beta+1} Y \iff \exists\, y \in Y,\ X \le^*_{0,\beta} y$.
• $b$ a limit, $Y = (i, y)$ with $y \in V^*_\beta(Q)$, $\beta = \operatorname{typein}(i) < b$: $\ X \le^*_{0,b} Y \iff X \le^*_{0,\beta} y$.

Case $a = \alpha+1$ ($X$ a nonempty subset of $V^*_\alpha(Q)$):

• $b = 0$ ($Y \in Q$): $\ X \le^*_{\alpha+1,0} Y \iff \forall\, x \in X,\ x \le^*_{\alpha,0} Y$.
• $b = \beta+1$ ($Y$ a nonempty subset of $V^*_\beta(Q)$): $\ X \le^*_{\alpha+1,\beta+1} Y \iff \forall\, x \in X,\ \exists\, y \in Y,\ x \le^*_{\alpha,\beta} y$. (The recursive value for level $\beta$ on the right with the same $X$ is available but not used in this clause.)
• $b$ a limit, $Y = (i, y)$ with $y \in V^*_\beta(Q)$, $\beta = \operatorname{typein}(i) < b$: $\ X \le^*_{\alpha+1,b} Y \iff X \le^*_{\alpha+1,\beta} y$.

Case $a$ a limit, $X = (i, x)$ with $x \in V^*_{\alpha'}(Q)$, $\alpha' = \operatorname{typein}(i) < a$: for every ordinal $b$ and every $Y \in V^*_b(Q)$, $\ X \le^*_{a,b} Y \iff x \le^*_{\alpha',b} Y$.

Each clause refers to the relation only at a strictly smaller level on at least one side, so the recursion is well-founded. Features visible in the clauses: a limit-level tag is simply discarded on whichever side it occurs; on the left the quantifier is always $\forall$ over the elements of a successor-level set, on the right always $\exists$; when one side is at level $0$ the other side is unwrapped alone (so $X \le^*_{1,0} Y$ for $X \subseteq Q$ nonempty and $Y \in Q$ means $\forall x \in X,\ x \le Y$, and $X \le^*_{0,1} Y$ for $X \in Q$ and $Y \subseteq Q$ nonempty means $\exists y \in Y,\ X \le y$); at $(0,0)$ the base relation is applied.

IsAlphaWQO le a. For a relation $\le$ on $Q$ and an ordinal $a$: IsWQO of the relation $X \mapsto Y \mapsto X \le^*_{a,a} Y$ on the type $V^*_a(Q)$, i.e.

$$\forall f : \mathbb N \to V^*_a(Q),\ \ \exists\, i<j,\ \ f_i \le^*_{a,a} f_j .$$

For $a = 0$ this is IsWQO le itself. For $a = 1$ it says: every sequence $S_0, S_1, \dots$ of nonempty subsets of $Q$ has $i<j$ with $\forall x \in S_i\ \exists y \in S_j,\ x \le y$. If $Q$ is empty the condition holds vacuously for every $a$.

FiniteGraph. The type $\sum_{n \in \mathbb N} \mathrm{SimpleGraph}(\mathrm{Fin}\,n)$: an element is a pair $(n, G)$ with $n \in \mathbb N$ (including $n = 0$, the graph with no vertices) and $G$ a simple graph on $\mathrm{Fin}\,n = \{0,\dots,n-1\}$. Elements are pairs, not isomorphism classes: isomorphic graphs with different vertex counts, or different isomorphic graphs on the same $\mathrm{Fin}\,n$, are distinct elements.

FiniteGraph.MinorLE G H. For $G = (n, G')$ and $H = (m, H')$: the proposition that there exists a minor witness of $G'$ in $H'$ in the sense of item TenChallenges_Minor, i.e. a family $(B_w)_{w \in \mathrm{Fin}\,n}$ of subsets of $\mathrm{Fin}\,m$ such that (i) $B_{w_1} \cap B_{w_2} = \emptyset$ whenever $w_1 \neq w_2$; (ii) each $B_w$ is nonempty and any two of its vertices are joined by a walk of $H'$ all of whose vertices lie in $B_w$; (iii) whenever $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$. The relation reads "$G$ is a minor of $H$" (first argument the minor, second the host). The element $(0, \emptyset)$ is a minor of everything, and $(n, G')$ with $n > m$ is never a minor of $(m, H')$.

PlanarGraph. The subtype $\{(n, G) \in \mathrm{FiniteGraph} : G \text{ satisfies `IsWagnerPlanar`}\}$, i.e. those $(n, G)$ such that there is no minor witness of $K_5$ (the complete graph on $\mathrm{Fin}\,5$) in $G$ and no minor witness of $K_{3,3}$ (completeBipartiteGraph (Fin 3) (Fin 3): vertex type $\mathrm{Fin}\,3 \sqcup \mathrm{Fin}\,3$, exactly the left–right pairs adjacent) in $G$. No embedding-based notion of planarity is involved; $(0, \emptyset)$ belongs to this type.

PlanarGraph.MinorLE G H. For $G, H$ in PlanarGraph: FiniteGraph.MinorLE applied to the underlying pairs, i.e. the underlying graph of $G$ is a minor of the underlying graph of $H$ (minor witness exactly as above).