`Compfiles/Imo2014P2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

10 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2014, Problem 2

Let $n \ge 2$ be an integer. Consider an $n \times n$ chessboard consisting of $n^2$ unit squares. A configuration of $n$ rooks on this board is peaceful if every row and every column contains exactly one rook. Find the greatest positive integer $k$ such that, for each peaceful configuration of $n$ rooks, there is a $k \times k$ square which does not contain a rook on any of its $k^2$ unit squares.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2014P2.HasEmptySquare A peaceful configuration of n rooks is a permutation σ: the rook in row i sits in column σ i line 36 source
Source documentation
A peaceful configuration of n rooks is a permutation σ: the rook in row i sits in column σ i. Such a configuration has a rook-free k × k square if there is a block of k consecutive rows and k consecutive columns (fitting on the board) containing no rook.

standard axioms: Quot.sound what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: Exists, And, LE.le, HAdd.hAdd, LT.lt, Not
8 instances, coercions and auxiliary constants left out.
```
def HasEmptySquare (σ : Equiv.Perm (Fin n)) (k : ℕ) : Prop :=
…
```
lemma Imo2014P2.hasEmptySquare_mono An empty k × k square contains an empty j × j square whenever j ≤ k line 44 source
Source documentation
An empty k × k square contains an empty j × j square whenever j ≤ k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, LE.le, Imo2014P2.HasEmptySquare
Proof uses: Exists, And, HAdd.hAdd, LT.lt, Not, Exists.intro, And.intro, And.left
14 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma hasEmptySquare_mono {σ : Equiv.Perm (Fin n)} {j k : ℕ}
    (hjk : j ≤ k) (h : HasEmptySquare σ k) : HasEmptySquare σ j := by
…
```
Mentions: h, Imo2014P2.HasEmptySquare
lemma Imo2014P2.sqrt_bounds ⌊√(n-1)⌋² < n ≤ (⌊√(n-1)⌋+1)² line 50 source
Source documentation
⌊√(n-1)⌋² < n ≤ (⌊√(n-1)⌋+1)².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, And, LT.lt, HMul.hMul, Nat.sqrt, HSub.hSub, HAdd.hAdd
Proof uses: And.intro, HPow.hPow, Nat.sqrt_le', Nat.succ, Nat.lt_succ_sqrt'
23 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma sqrt_bounds (hn : 2 ≤ n) :
    Nat.sqrt (n - 1) * Nat.sqrt (n - 1) < n ∧
      n ≤ (Nat.sqrt (n - 1) + 1) * (Nat.sqrt (n - 1) + 1) := by
…
```
lemma Imo2014P2.exists_empty_square Existence (lower bound): every peaceful configuration has an empty ⌊√(n-1)⌋ × ⌊√(n-1)⌋ square line 65 source
Source documentation
Existence (lower bound): every peaceful configuration has an empty ⌊√(n-1)⌋ × ⌊√(n-1)⌋ square.
Following Evan Chen: let R be the rook in the top row, in column col₀, and stack k squares of size k × k directly below it. The k columns of that stack contain k rooks in total, but R's rook sits at row 0, above the stack — so the stack holds at most k - 1 rooks among k disjoint squares, and one of them is empty.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Equiv.Perm, Fin, Imo2014P2.HasEmptySquare, Nat.sqrt, HSub.hSub
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, LT.lt, HMul.hMul, And.left, HAdd.hAdd, Imo2014P2.sqrt_bounds, Iff.mpr, Nat.le_sqrt, Nat.mul_le_mul_left, Fin.mk, Fin.isLt, Min.min, min_le_right, And, And.intro, min_le_left and 73 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 97 steps
Open to load the checked before-and-after goal states.
```
lemma exists_empty_square (hn : 2 ≤ n) (σ : Equiv.Perm (Fin n)) :
    HasEmptySquare σ (Nat.sqrt (n - 1)) := by
…
```
Mentions: Imo2014P2.HasEmptySquare
def Imo2014P2.HasRook σ places a rook in every axis-aligned K × K square — exactly the negation of HasEmptySquare line 162 source
Source documentation
σ places a rook in every axis-aligned K × K square — exactly the negation of HasEmptySquare.

standard axioms: Quot.sound what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: LE.le, HAdd.hAdd, Exists, And, LT.lt
8 instances, coercions and auxiliary constants left out.
```
def HasRook {m : ℕ} (σ : Equiv.Perm (Fin m)) (K : ℕ) : Prop :=
…
```
lemma Imo2014P2.covering_restrict Restriction reduction: a rook-covering configuration on an M × M board restricts (top-left, then completed arbitrarily) to one on any smaller N × N board line 171 source
Source documentation
Restriction reduction: a rook-covering configuration on an M × M board restricts (top-left, then completed arbitrarily) to one on any smaller N × N board. The key point: every K × K square of the N × N board lies inside [0,N)², so its witnessing rook already has both coordinates < N and survives the restriction; the arbitrary completion only adds rooks.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Equiv.Perm, Fin, Imo2014P2.HasRook, Exists
Proof uses: dite, LT.lt, Fin.castLE, Fin.mk, Not, Eq, rfl, Set, Set.ofPred, Set.InjOn, Membership.mem, Eq.mp, congrFun', congrArg, congr, of_eq_true, eq_true, Eq.trans, dite_eq_left_of_eq_true, Fin.castLE_injective and 30 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma covering_restrict {K M N : ℕ} (hNM : N ≤ M)
    (τ : Equiv.Perm (Fin M)) (hτ : HasRook τ K) :
    ∃ σ : Equiv.Perm (Fin N), HasRook σ K := by
…
```
Mentions: Imo2014P2.HasRook
lemma Imo2014P2.transpose_covering Base case of the construction: the grid-transpose i ↦ K·(i % K) + i / K is a permutation of the K² × K² board placing a rook in every K × K square line 217 source
Source documentation
Base case of the construction: the grid-transpose i ↦ K·(i % K) + i / K is a permutation of the K² × K² board placing a rook in every K × K square.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Equiv.Perm, Fin, HMul.hMul, Imo2014P2.HasRook
Proof uses: LT.lt, HDiv.hDiv, Iff.mpr, Nat.div_lt_iff_lt_mul, Fin.isLt, HAdd.hAdd, HMod.hMod, Nat.mod_lt, Nat.mul_add_lt_mul_of_lt_of_lt, Fin.mk, Eq, rfl, Function.Involutive, Fin.ext, Eq.mpr, id, congrArg, Nat.mul_add_mod, Nat.mod_eq_of_lt, Nat.mul_add_div and 37 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 106 steps
Open to load the checked before-and-after goal states.
```
lemma transpose_covering (K : ℕ) (hK : 1 ≤ K) :
    ∃ τ : Equiv.Perm (Fin (K * K)), HasRook τ K := by
…
```
Mentions: Imo2014P2.HasRook
lemma Imo2014P2.exists_config_no_square Optimality (upper bound): some peaceful configuration has no empty (⌊√(n-1)⌋+1) × (⌊√(n-1)⌋+1) square line 284 source
Source documentation
Optimality (upper bound): some peaceful configuration has no empty (⌊√(n-1)⌋+1) × (⌊√(n-1)⌋+1) square.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Equiv.Perm, Fin, Not, Imo2014P2.HasEmptySquare, HAdd.hAdd, Nat.sqrt, HSub.hSub
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, HMul.hMul, And.right, LT.lt, Imo2014P2.sqrt_bounds, Imo2014P2.HasRook, Imo2014P2.transpose_covering, Imo2014P2.covering_restrict, Exists.intro, And, False, And.intro
22 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma exists_config_no_square (hn : 2 ≤ n) :
    ∃ σ : Equiv.Perm (Fin n), ¬ HasEmptySquare σ (Nat.sqrt (n - 1) + 1) := by
…
```
Mentions: Imo2014P2.HasEmptySquare
determine Imo2014P2.greatestK line 298 source
no axioms what this means
Statement uses: Nat
Proof uses: Nat.sqrt, HSub.hSub, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
problem Imo2014P2.imo2014_p2 line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, IsGreatest, Set.ofPred, Equiv.Perm, Fin, Imo2014P2.HasEmptySquare, Imo2014P2.greatestK
Proof uses: And.intro, Membership.mem, Set, upperBounds, Imo2014P2.exists_empty_square, id, Decidable.byContradiction, Nat.sqrt, HSub.hSub, Not, HAdd.hAdd, Exists, False, Imo2014P2.exists_config_no_square, Imo2014P2.hasEmptySquare_mono
12 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.