Winning Angel strategies are monotone in power
ProvedAngelDevil.angelWins_monoangel-problemcombinatoricsgame-theory
For natural-number powers p ≤ q, if a single power-p Angel strategy survives against every Devil, then a power-q Angel has a winning strategy as well.
The game histories and Devil actions are unchanged when only the permitted jump radius increases.
Preamble
import Definitions.Def_AngelDevil_Game
Formal statement
theorem AngelDevil.angelWins_mono {p q : Nat} (hpq : p ≤ q) (h : AngelDevil.AngelWins p) : AngelDevil.AngelWins q := by sorrySource
Andras Mathe, The Angel of power 2 wins (2007), Theorem 4.6 and Section 1 game definition; https://doi.org/10.1017/S0963548306008303. Elementary consequence of the Chebyshev jump rule, not a separately numbered theorem.