Complete classification by integer Angel power
ProvedAngelDevil.angelWins_iff_two_leangel-problemcombinatoricsgame-theory
In the standard infinite-board game against a Devil that burns at most one square per round, the Angel has a winning strategy exactly for natural-number powers p ≥ 2.
The negative cases are p=0 and p=1. The zero-power case is included because the formal parameter ranges over all natural numbers. This combines the known king-capture result with Mathe's power-two theorem and monotonicity.
Preamble
import Definitions.Def_AngelDevil_Game
Formal statement
theorem AngelDevil.angelWins_iff_two_le (p : Nat) : AngelDevil.AngelWins p ↔ 2 ≤ p := by sorry
Source
Martin Kutz, The Angel Problem, Positional Games, and Digraph Roots (2004), Chapter 1, Section 1.1, pp. 2-3, Figures 1-3. https://people.mpi-inf.mpg.de/alumni/d1/2009/mkutz/diss/kutz_angel.pdf. Andras Mathe, The Angel of power 2 wins (2007), Theorem 4.6 and Section 1 game definition; https://doi.org/10.1017/S0963548306008303. Logical combination of these published results.