Partitioner wins the $r$-partitioning game on every countable graph, for every ordinal $r$

Setting and notation. Throughout, $V$ is an arbitrary type (the vertex set) living in a universe $u$; $V$ may be empty, finite or infinite. $G$ is a simple graph on $V$, i.e. a binary adjacency relation $v \sim_G w$ on $V$ that is symmetric and irreflexive (no loops, no multiple edges, and no further restriction: a vertex may have infinitely many neighbours). $N_G(v) = \{\, w \in V : v \sim_G w \,\}$ is the set of neighbours of $v$. A partial 2-colouring is any function $f : V \to \{\bot, \mathsf T, \mathsf F\}$, where $\bot$ means "no colour assigned" and $\mathsf T, \mathsf F$ are the two Boolean colours; for a Boolean $b$, $\bar b$ denotes its negation ($\bar{\mathsf T} = \mathsf F$, $\bar{\mathsf F} = \mathsf T$). $|X|$ denotes the cardinality of $X$ as a cardinal number (in universe $u$), so it may be infinite, and $\le$ between cardinalities means existence of an injection. Ordinals $\alpha, \beta, r$ range over the ordinals of a second universe $v$, independent of $u$; $\beta < \alpha$ is the usual strict well-ordering of ordinals.

Theorem challenge_10. The theorem asserts

that is, fully unfolded:

Countable means there exists an injective map $V \to \mathbb N$ (so $V$ may be countably infinite, finite, or empty). The simple graph $G$ is arbitrary subject only to being symmetric and irreflexive (vertices may have infinitely many neighbours; nothing else is assumed). Here $f_\emptyset$ is the all-uncoloured partial colouring, $f_\emptyset(v) = \bot$ for every $v$, and $W(G, f, \alpha)$ ("Partitioner wins from $(f,\alpha)$") is the proposition defined by well-founded recursion on the ordinal $\alpha$ by

where the legal-response predicate $L$ is the conjunction

and unfriendly at $v$ means

i.e. $v$ is coloured by $g$ and, comparing cardinal numbers (possibly infinite), the neighbours of $v$ with the same colour as $v$ are no more numerous than the neighbours with the opposite colour; uncoloured neighbours count on neither side. Spelled out, $W(G,f,\alpha)$ says: for every vertex $v$ whatsoever (coloured or not; the same vertex may be chosen repeatedly) and every ordinal $\beta$ strictly below $\alpha$ (all of them, not only a predecessor), there is a partial colouring $g$, which may depend on both $v$ and $\beta$, that keeps every colour already assigned by $f$, colours only finitely many vertices in total, is unfriendly at $v$ (nothing is required at other vertices, and $g$ need not differ from $f$), and from which the same property holds again with clock $\beta$. Since the clocks strictly decrease, every such sequence of challenges is finite, and $W(G,g,0)$ holds unconditionally (there is no $\beta < 0$).

The statement is polymorphic in the two universe levels $u$ (where the vertex types live) and $v$ (where the ordinals live): it is a family of assertions, one for every choice of these levels, and the quantifier over $r$ ranges over all ordinals of universe $v$, with no bound. Edge cases literally included: for $r = 0$ the assertion is trivially true; for empty $V$ it is trivially true for every $r$; for every $r > 0$ and every nonempty countable $V$ and every simple graph on it, it demands a finite-domain colouring unfriendly at any challenged vertex, and then recursively for every smaller clock. The declaration's proof is left as a placeholder (it is stated, not proved); this read-back concerns only the statement.