`Compfiles/Imo2021P5.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

16 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2021, Problem 5

Two squirrels, Bushy and Jumpy, have collected 2001 walnuts for winter. Jumpy numbers the walnuts from 1 to 2021, and digs 2021 little holes in a circular pattern around their favorite tree. The next morning, Jumpy notices that Bushy had placed one walnut into each hole, but had paid no attention to the numbering. Unhappy, Jumpy decides to reorder the walnuts by performing a sequence of 2021 moves. In the kth move, Jump swaps the positions of the two walnuts adjacent to walnut k.

Prove that there exists a value of k such that, on the kth move, Jumpy swaps some walnuts a and b such that a < k < b.

Imports (4)

Imported by 1 file

Compfiles.lean

abbrev Imo2021P5.Position The arrangement of walnuts, as an equiv from holes to walnuts (0-based) line 39 source
Source documentation
The arrangement of walnuts, as an equiv from holes to walnuts (0-based).

no axioms what this means
Proof uses: Equiv, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
```
abbrev Position : Type := Fin 2021 ≃ Fin 2021
```
def Imo2021P5.Position.swapped The numbers of the walnuts swapped in move k (0-based), given the position line 42 source
Source documentation
The numbers of the walnuts swapped in move k (0-based), given the position.

standard axioms: Quot.sound, propext what this means
Statement uses: Imo2021P5.Position, Fin, OfNat.ofNat, Nat, Prod
Proof uses: Prod.mk, HSub.hSub, Equiv, Equiv.symm, HAdd.hAdd
11 instances, coercions and auxiliary constants left out.
```
def Position.swapped (p : Position) (k : Fin 2021) : Fin 2021 × Fin 2021 :=
…
```
Mentions: Imo2021P5.Position
def Imo2021P5.move A single move, on a pair of position and move number line 46 source
Source documentation
A single move, on a pair of position and move number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Imo2021P5.Position, Fin, OfNat.ofNat, Nat
Proof uses: Prod.mk, Equiv.trans, Prod.fst, Equiv.swap, Imo2021P5.Position.swapped, Prod.snd, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.
```
def move (p : Position × Fin 2021) : Position × Fin 2021 :=
…
```
Mentions: Imo2021P5.Position
def Imo2021P5.Position.nth The position after n moves line 50 source
Source documentation
The position after n moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2021P5.Position, Fin, OfNat.ofNat, Nat
Proof uses: Prod.fst, Nat.iterate, Prod, Imo2021P5.move, Prod.mk
5 instances, coercions and auxiliary constants left out.
```
def Position.nth (p : Position) (n : Fin 2021) : Position := (move^[n] (p, 0)).1
…
```
Mentions: Imo2021P5.Position, Imo2021P5.move
def Imo2021P5.coloring After j moves, color hole x red iff the walnut in it has number < j; otherwise the hole is black line 56 source
Source documentation
After j moves, color hole x red iff the walnut in it has number < j; otherwise the hole is black.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2021P5.Position, Nat, Fin, OfNat.ofNat, Bool
Proof uses: Decidable.decide, LT.lt, Prod.fst, Nat.iterate, Prod, Imo2021P5.move, Prod.mk
10 instances, coercions and auxiliary constants left out.
```
def coloring (p : Position) (j : ℕ) (x : Fin 2021) : Bool :=
…
```
Mentions: Imo2021P5.Position
def Imo2021P5.blackPairs The number (mod 2) of adjacent pairs of holes that are both black line 60 source
Source documentation
The number (mod 2) of adjacent pairs of holes that are both black.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Bool, ZMod
Proof uses: Finset.sum, Finset.univ, HMul.hMul, cond, HAdd.hAdd
25 instances, coercions and auxiliary constants left out.
```
def blackPairs (c : Fin 2021 → Bool) : ZMod 2 :=
…
```
theorem Imo2021P5.fin_val_one line 63 source
standard axioms: propext what this means
Statement uses: Eq, Nat, OfNat.ofNat, Fin
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
theorem Imo2021P5.fin_sub_one_add_one line 65 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, HAdd.hAdd, HSub.hSub
Proof uses: sub_add_cancel
12 instances, coercions and auxiliary constants left out.
theorem Imo2021P5.fin_sub_one_ne_self line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, HSub.hSub
Proof uses: Eq, congrArg
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2021P5.fin_add_one_ne_self line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, HAdd.hAdd
Proof uses: Eq, congrArg
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2021P5.fin_sub_one_ne_add_one line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, HSub.hSub, HAdd.hAdd
Proof uses: Eq, congrArg
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2021P5.iterate_snd The second component of the iterated move state is the move number line 86 source
Source documentation
The second component of the iterated move state is the move number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2021P5.Position, Nat, Eq, OfNat.ofNat, Prod.snd, Fin, Nat.iterate, Prod, Imo2021P5.move, Prod.mk, HMod.hMod
Proof uses: Nat.recAux, Eq.refl, Eq.mpr, HAdd.hAdd, id, congrArg, Nat.succ, Function.iterate_succ_apply', Fin.val_add, Imo2021P5.fin_val_one
16 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem iterate_snd (p : Position) (j : ℕ) : ((move^[j] (p, 0)).2).val = j % 2021 := by
…
```
Mentions: Imo2021P5.Position, Imo2021P5.move
theorem Imo2021P5.iterate_fst_succ One step of the move process on the position component line 95 source
Source documentation
One step of the move process on the position component.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2021P5.Position, Nat, LT.lt, OfNat.ofNat, Eq, Prod.fst, Fin, Nat.iterate, Prod, Imo2021P5.move, HAdd.hAdd, Prod.mk, Equiv.trans, Equiv.swap, HSub.hSub, Equiv, Equiv.symm, Fin.mk
Proof uses: Prod.snd, Fin.ext, Eq.mpr, HMod.hMod, id, congrArg, Imo2021P5.iterate_snd, Nat.mod_eq_of_lt, Nat.succ, Function.iterate_succ_apply', Eq.rec, Eq.refl, Eq.trans, Prod.ext, rfl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem iterate_fst_succ (p : Position) (j : ℕ) (hj : j < 2021) :
    (move^[j + 1] (p, 0)).1 = (move^[j] (p, 0)).1.trans
      (Equiv.swap
        ((move^[j] (p, 0)).1 ((move^[j] (p, 0)).1.symm ⟨j, hj⟩ - 1))
        ((move^[j] (p, 0)).1 ((move^[j] (p, 0)).1.symm ⟨j, hj⟩ + 1))) := by
…
```
Mentions: Imo2021P5.Position, Imo2021P5.move
theorem Imo2021P5.blackPairs_update Flipping one black hole to red, where the two neighbors have the same color, does not change the number of black-black adjacent pairs, mod 2 line 108 source
Source documentation
Flipping one black hole to red, where the two neighbors have the same color, does not change the number of black-black adjacent pairs, mod 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Bool, Eq, Bool.false, HSub.hSub, HAdd.hAdd, Ne, ZMod, Imo2021P5.blackPairs, Function.update, Bool.true
Proof uses: id, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, cond, congrArg, Eq.symm, propext, sub_eq_zero, Finset.sum_sub_distrib, Insert.insert, Finset, Singleton.singleton, Finset.sum_subset, Finset.subset_univ, Membership.mem, Not, And.left, Eq.mp and 33 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
theorem blackPairs_update (c : Fin 2021 → Bool) (h : Fin 2021)
    (hh : c h = false) (hn : c (h - 1) = c (h + 1))
    (h1 : h - 1 ≠ h) (h2 : h + 1 ≠ h) :
    blackPairs (Function.update c h true) = blackPairs c := by
…
```
Mentions: h, Imo2021P5.blackPairs
theorem Imo2021P5.coloring_succ Documented declaration: coloring_succ line 143 source
Source documentation
If there is no good move, then after move j the coloring is the previous coloring with the hole of walnut j flipped from black to red, and the two neighbors of that hole have the same color.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2021P5.Position, Nat, LT.lt, OfNat.ofNat, Fin, Not, Or, And, Prod.fst, Imo2021P5.Position.swapped, Imo2021P5.Position.nth, Prod.snd, Eq, Bool, Imo2021P5.coloring, HAdd.hAdd, Function.update, Equiv, Equiv.symm, Nat.iterate and 7 more
Proof uses: Eq.mpr, id, congrArg, rfl, Equiv.trans, Equiv.swap, Imo2021P5.iterate_fst_succ, Eq.mp, Eq.symm, Eq.refl, Equiv.apply_symm_apply, Ne, Imo2021P5.fin_sub_one_ne_self, Imo2021P5.fin_add_one_ne_self, Imo2021P5.fin_sub_one_ne_add_one, Equiv.injective, Iff, Fin.ext, Eq.trans, congr and 17 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 84 steps
Open to load the checked before-and-after goal states.
```
theorem coloring_succ (p : Position) (j : ℕ) (hj : j < 2021)
    (H : ∀ k : Fin 2021,
      ¬((((p.nth k).swapped k).1 < k ∧ k < ((p.nth k).swapped k).2) ∨
        (((p.nth k).swapped k).2 < k ∧ k < ((p.nth k).swapped k).1))) :
    (∀ x, coloring p (j + 1) x =
        Function.update (coloring p j) ((move^[j] (p, 0)).1.symm ⟨j, hj⟩) true x) ∧
      coloring p j ((move^[j] (p, 0)).1.symm ⟨j, hj⟩) = false ∧
      coloring p j ((move^[j] (p, 0)).1.symm ⟨j, hj⟩ - 1) =
        coloring p j ((move^[j] (p, 0)).1.symm ⟨j, hj⟩ + 1) := by
…
```
Mentions: Imo2021P5.Position, Imo2021P5.coloring, Imo2021P5.move
problem Imo2021P5.imo2021_p5 line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2021P5.Position, Exists, Fin, OfNat.ofNat, Nat, Or, And, LT.lt, Prod.fst, Imo2021P5.Position.swapped, Imo2021P5.Position.nth, Prod.snd
Proof uses: Decidable.byContradiction, Not, Exists.intro, Eq, ZMod, Imo2021P5.blackPairs, Imo2021P5.coloring, HAdd.hAdd, Bool, Function.update, Equiv, Equiv.symm, Nat.iterate, Prod, Imo2021P5.move, Prod.mk, Fin.mk, Bool.true, Bool.false, HSub.hSub and 47 more
75 instances, coercions and auxiliary constants left out.

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