Five-burn preparation of a line guard
ProvedAngelDevil.kingGuard_five_originangel-problemcombinatoricsgame-theory
Starting with no blocked sites on a line, the Devil can prepare a blocked triple above a king in five burns, despite every intervening horizontal displacement being -1, 0, or 1.
The finite strategy predicate records four intervening moves and a final burn that completes the triple. This is the local preparation lemma used to guard a box boundary.
Preamble
import Definitions.Def_AngelDevil_KingGuard
Formal statement
theorem AngelDevil.kingGuard_five_origin : AngelDevil.KingGuard 4 0 ∅ := 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. Finite strategy certificate for Figure 2; index 4 represents five burns.