Claim 2.6: allowed journeys remain allowed after reduction

Proved

AngelDevil.reducedJourney_allowed

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

angel-problemcombinatoricsgame-theory

For every nonnegative integer power, every Devil strategy and every finite journey allowed against its Nice transformation, the reduced journey is allowed against the original Devil. Allowedness includes both bounded jumps and avoidance of all earlier Devil selections. The statement also covers power zero.

Preamble

import Definitions.Def_AngelDevil_NiceReduction
open AngelDevil

Formal statement

theorem AngelDevil.reducedJourney_allowed (p : Nat) (D : DevilStrategy) (h : List Point)
    (ha : Allowed p (niceReduction p D) h) : Allowed p D (reducedJourney p h)  := 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. Claim 2.6, p. 3.

View graph