Theorem 2.4: transfer confinement to a Nice Devil

Proved

AngelDevil.confinement_to_nice

by Yuxuan Xu · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

angel-problemcombinatoricsgame-theory

Let p and N be nonnegative integers. If a Devil strategy keeps every safe finite play of the power-p Angel inside the box of radius N, then some Nice Devil does the same. The assumption ranges over every Angel strategy and every finite time, requiring safety only up to that time. This formalization includes the degenerate cases p = 0 and N = 0 in addition to the positive parameters in the paper.

Preamble

import Definitions.Def_AngelDevil_NiceReduction
open AngelDevil

Formal statement

theorem AngelDevil.confinement_to_nice (p N : Nat) (D : DevilStrategy)
    (hc : ∀ A n, (∀ m, m < n →
      Jump p (current (play A D m)) (current (play A D (m+1))) ∧
      some (current (play A D (m+1))) ∉ (play A D (m+1)).burned) →
      InBox N (current (play A D n))) : NiceCanConfine p N  := by sorry

Source

Andras Mathe, The Angel of power 2 wins, CPC 16 (2007), 363-374; https://doi.org/10.1017/S0963548306008303; author manuscript internal pagination. Theorem 2.4, pp. 2-3, with harmless zero-parameter extension.

View graph