Prove2Me

Claim 4.2: boundary bound for connected squares

Proved
AngelDevil.connectedSquares_perimeter

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

angel-problemcombinatoricsgame-theory

Let SS be a finite nonempty set of integer unit squares, connected by shared sides, and let P(S)P(S) count all unit boundary sides, including boundaries of holes. Then

P(S)≤2∣S∣+2.P(S) \le 2|S|+2.

This is the connected-square perimeter estimate used in the wall-counting argument for the Angel strategy.

Preamble
import Definitions.Def_AngelDevil_SquareBoundary
Formal statement
theorem AngelDevil.connectedSquares_perimeter {s : Finset AngelDevil.Point} (h : AngelDevil.SquaresConnected s) : AngelDevil.squarePerimeter s ≤ 2 * s.card + 2 := by sorry
Source
Mathe, The Angel of power 2 wins (2007), https://doi.org/10.1017/S0963548306008303, author manuscript p. 6, Definition 4.1 and Claim 4.2.

View graph