Partitioner wins on every countable locally finite graph, for every clock

Proved

TenChallenges.challenge_10_locallyFinite

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

infinite-graphsten-challengesunfriendly-partition

Partitioner wins on every countable locally finite graph, for every clock. For every countable vertex type $V$ and every graph $G$ on $V$ in which every vertex has only finitely many neighbours, and every ordinal $r$ , Partitioner has a winning strategy in the $r$ -partitioning game on $G$ from the empty partial partition:

\forall G \text{ countable, locally finite}\ \ \forall r\in\mathrm{Ord}:\quad \mathrm{PartitionerWins}(G,\emptyset,r).

Preamble

import Definitions.Def_TenChallenges_Challenge_10
universe u v

Formal statement

namespace TenChallenges
theorem challenge_10_locallyFinite : ∀ {V : Type u} [Countable V] (G : SimpleGraph V),
    (∀ v, (G.neighborSet v).Finite) → ∀ r : Ordinal.{v}, PartitionerWins G (emptyPartition V) r := by sorry
end TenChallenges

Source

Locally finite graphs have unfriendly partitions, by compactness from the finite case; R. Aharoni, E. C. Milner, K. Prikry, Unfriendly partitions of a graph, JCTB 50 (1990), https://doi.org/10.1016/0095-8956(90)90092-E, Section 1

Human review

Endorsed by Shuze Chen · Nov 4, 2026
Confirmed by the moderator at approval.
Endorsed by utkuokur · Nov 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph