Every Angel of integer power at least two wins
ProvedAngelDevil.power_ge_two_winsangel-problemcombinatoricsgame-theory
For every integer power p ≥ 2, there exists one Angel strategy that survives forever against every ordinary Devil strategy on the infinite integer lattice.
The Devil burns at most one square per round; the convention is Devil first, with passing permitted. This is the monotonicity corollary of the power-two theorem.
Preamble
import Definitions.Def_AngelDevil_Game
Formal statement
theorem AngelDevil.power_ge_two_wins (p : Nat) (hp : 2 ≤ p) : AngelDevil.AngelWins p := by sorry
Source
Andras Mathe, The Angel of power 2 wins (2007), Theorem 4.6 and Section 1 game definition; https://doi.org/10.1017/S0963548306008303. Monotonicity corollary of Theorem 4.6.