Partitioner wins on every finite graph, for every clock
ProvedTenChallenges.challenge_10_finiteinfinite-graphsten-challengesunfriendly-partition
Partitioner wins on every finite graph, for every clock. For every finite vertex type , every graph on and every ordinal , Partitioner has a winning strategy in the -partitioning game on from the empty partial partition:
Preamble
import Definitions.Def_TenChallenges_Challenge_10 universe u v
Formal statement
namespace TenChallenges
theorem challenge_10_finite : ∀ {V : Type u} [Finite V] (G : SimpleGraph V) (r : Ordinal.{v}),
PartitionerWins G (emptyPartition V) r := by sorry
end TenChallengesSource
Every finite graph has an unfriendly partition (a partition with the maximum number of crossing edges); e.g. R. Aharoni, E. C. Milner, K. Prikry, Unfriendly partitions of a graph, JCTB 50 (1990), introduction, https://doi.org/10.1016/0095-8956(90)90092-E; game form from the Ten Challenges website, challenge 10
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.