Angel–Devil: complete integer-power classification

Lean now proves AngelWins p ↔ 2 ≤ p: one Devil defeats every power-one Angel, and every power at least two has a winning Angel strategy. The classification is Proved on Prove2Me.

This combines the known Berlekamp king-capture argument, as presented in Kutz 2004, Section 1.1, with the completed formalization of Andras Mathe, The Angel of power 2 wins, Combinatorics, Probability and Computing 16 (2007), 363–374. Paper DOI.

The original main theorem is Proved on Prove2Me and proved in the closed local Lean library. This formalizes a published result; it claims no new mathematical solution and no independent peer review.

Verified result

• AngelDevil.power_one_devil_wins — one Devil strategy defeats every power-one Angel.

• AngelDevil.power_ge_two_wins — every integer power at least two wins.

• AngelDevil.angelWins_iff_two_le — exact classification for all natural-number powers, including zero.

• AngelDevil.devilWins_iff_le_one — complementary classification in the closed local library.

• AngelDevil.power_two_wins : AngelDevil.AngelWins 2 — one power-two strategy survives against every Devil in the original infinite-board game.

• AngelDevil.power_two_beats_nice_devil : AngelDevil.NiceAngelWins 2 — one explicit strategy survives and escapes every finite box against every Nice Devil.

• The original Theorem 2.7 reduction is also proved, using finite-game determinacy, compactness, reduced journeys and confinement transfer.

• 228 local theorems checked, with only propext, Classical.choice and Quot.sound in their axiom dependencies; no sorryAx or custom axioms.

• Zero open leaves in both the original theorem graph and the complete classification graph. All six extension proofs are ACCEPTED; the latter graph has 37 nodes and 66 edges. The geometric no-return proof is ACCEPTED and actually imports the proved Claim 4.2 perimeter bound.

Classification audit · Closed classification

Original live main theorem · Completion audit · Closed local assembly

Reproduce local checks

Install elan and the pinned Lean toolchain. From a fresh checkout, in PowerShell:

$env:MATHLIB_NO_CACHE_ON_UPDATE = '1'
lake update
lake exe cache get Mathlib.Combinatorics.Compactness Mathlib.Algebra.Order.BigOperators.Group.Finset Mathlib.Data.Fintype.Prod Mathlib.Data.Fintype.Fin Mathlib.Tactic.FinCases
python scripts/verify.py

Lean is pinned to v4.33.1 and Mathlib to 0df444a360eaa60ab8c11dca51a86af692955474, matching the platform environment. The verifier builds Solutions.PowerClassification, checks the exact types of the original mission targets and the new classification, and audits the axioms of the closed proof library. It separately elaborates the original reference statements.

Theorems/ contains platform statement mirrors with sorry, including mirrors of results now proved on the server. These are excluded from the closed local library. Files packaging platform reductions import those mirrors for protocol compatibility; compiling such a package alone is not a closed local proof. Use Solutions.PowerClassification and scripts/verify.py for the full closed proof. Solutions.Completed remains the original power-two assembly.

Proof route

For power one, a kernel-checked five-burn line-guard certificate supplies the local barrier strategy. Preblocked corners let four guards confine the king to a finite square. Burning a fresh square each round then forces finite failure. The formal proof uses deliberately loose radius-100 constants; no optimal capture time is claimed. See the classification audit.

The Nice strategy uses the paper's octagonal corner convention, with exactly two wall transitions per turn. Each transition moves the outside square by at most one king step. Nice protection preserves earlier empty squares, so the first repeated wall would be the initial wall. A first contact with the x-axis would yield a finite frozen boundary cycle whose lower length bound exceeds the connected-component perimeter upper bound. Therefore no return occurs, and a finite-box argument proves escape. Theorem 2.7 then gives the original unrestricted Angel theorem. See the geometric proof explanation and implementation/source comparison.

Source, mission and publication

• Source provenance and checksum. The downloaded author manuscript is retained locally in papers/; PDF/text are not redistributed.
• Source-to-model audit and original independent blind read-backs.
• Local validation and current status.
• Unified Prove2Me mission: Angel-Devil: Complete Integer-Power Classification, public, main goal Proved. The original mission was upgraded in place on 2026-10-19; all four source milestones are completed. The original power-two target remains a milestone. Mission metadata · Milestone readback. The original proposal 8632c949-8a1d-477d-b87b-ad737965860b remains Reviewed.

Formalization of already public work is public by default. Original mathematical results must stay private until the owner explicitly authorizes publication.