Preservation of a guarded box against a chess king
ProvedAngelDevil.king_box_stepangel-problemcombinatoricsgame-theory
Suppose the king is strictly inside the box [-100,100]^2, its corner boundary segments are blocked, and each side has a line guard whose preparation fits the remaining distance. Then there is a single square in the box for the Devil to block such that every subsequent legal king move preserves these conditions.
This formal invariant implements the four-side confinement argument; the constants are deliberately loose, not an optimal capture bound.
Preamble
import Definitions.Def_AngelDevil_KingGuard
Formal statement
theorem AngelDevil.king_box_step (p : AngelDevil.Point) (B : Finset AngelDevil.Point) (h : AngelDevil.KingBoxReady p B) : ∃ z ∈ AngelDevil.kingBoard, ∀ q, AngelDevil.Jump 1 p q → q ∉ insert z B → AngelDevil.KingBoxReady q (insert z B) := 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. Implementation of Figure 3 with radius 100 and seven-site corner arms, rather than the illustrated constants.