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

27 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2000, Problem 3

Let n ≥ 2 be a positive integer and λ a positive real number. Initially there are n fleas on a horizontal line, not all at the same point. We define a move as choosing two fleas at some points A and B, with A to the left of B, and letting the flea from A jump over the flea from B to the point C so that BC/AB = λ.

Determine all values of λ such that, for any point M on the line and for any initial position of the n fleas, there exists a sequence of moves that will take them all to the right of M.

Imports (7)

Imported by 1 file

Compfiles.lean

def Imo2000P3.Move Documented declaration: Move line 41 source
Source documentation
A single move with jump ratio lam: flea i, sitting at some point A = x i, jumps over flea j at B = x j (with A to the left of B) and lands at the point C = B + lam * (B - A), so that BC / AB = lam. All other fleas stay put.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Fin
Proof uses: Exists, And, LT.lt, Eq, Function.update, HAdd.hAdd, HMul.hMul, HSub.hSub
8 instances, coercions and auxiliary constants left out.
```
def Move (lam : ℝ) {n : ℕ} (x y : Fin n → ℝ) : Prop :=
…
```
def Imo2000P3.Reachable Reachable lam x y means that configuration y can be reached from configuration x by a finite sequence of moves with jump ratio lam line 46 source
Source documentation
Reachable lam x y means that configuration y can be reached from configuration x by a finite sequence of moves with jump ratio lam.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Fin
Proof uses: Relation.ReflTransGen, Imo2000P3.Move
```
def Reachable (lam : ℝ) {n : ℕ} (x y : Fin n → ℝ) : Prop :=
…
```
def Imo2000P3.AllRightOf Documented declaration: AllRightOf line 52 source
Source documentation
The property of lam in the problem: starting from any initial configuration in which the fleas are not all at the same point, for every point M on the line there is a finite sequence of moves taking all the fleas strictly to the right of M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Fin, Exists, Ne, And, Imo2000P3.Reachable, LT.lt
1 instances, coercions and auxiliary constants left out.
```
def AllRightOf {n : ℕ} (lam : ℝ) : Prop :=
…
```
def Imo2000P3.rightmost The position of the rightmost flea line 59 source
Source documentation
The position of the rightmost flea.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real
Proof uses: iSup
1 instances, coercions and auxiliary constants left out.
```
noncomputable def rightmost {n : ℕ} (x : Fin n → ℝ) : ℝ := ⨆ i, x i
```
def Imo2000P3.leftmost The position of the leftmost flea line 62 source
Source documentation
The position of the leftmost flea.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real
Proof uses: iInf
1 instances, coercions and auxiliary constants left out.
```
noncomputable def leftmost {n : ℕ} (x : Fin n → ℝ) : ℝ := ⨅ i, x i
```
def Imo2000P3.potential Gerhard Woeginger's potential function: the sum of the distances of the fleas from the rightmost flea line 66 source
Source documentation
Gerhard Woeginger's potential function: the sum of the distances of the fleas from the rightmost flea.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real
Proof uses: Finset.sum, Finset.univ, HSub.hSub, Imo2000P3.rightmost
4 instances, coercions and auxiliary constants left out.
```
noncomputable def potential {n : ℕ} (x : Fin n → ℝ) : ℝ := ∑ i, (rightmost x - x i)
…
```
Mentions: Imo2000P3.rightmost
lemma Imo2000P3.bddAbove_range line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, BddAbove, Set.range
Proof uses: Set.Finite.bddAbove, Set.finite_range
11 instances, coercions and auxiliary constants left out.
lemma Imo2000P3.bddBelow_range line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, BddBelow, Set.range
Proof uses: Set.Finite.bddBelow, Set.finite_range
11 instances, coercions and auxiliary constants left out.
lemma Imo2000P3.le_rightmost line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, LE.le, Imo2000P3.rightmost
Proof uses: le_ciSup, Imo2000P3.bddAbove_range
3 instances, coercions and auxiliary constants left out.
lemma Imo2000P3.leftmost_le line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, LE.le, Imo2000P3.leftmost
Proof uses: ciInf_le, Imo2000P3.bddBelow_range
3 instances, coercions and auxiliary constants left out.
lemma Imo2000P3.exists_eq_rightmost line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nonempty, Fin, Real, Exists, Eq, Imo2000P3.rightmost
Proof uses: And, Membership.mem, Finset, Finset.univ, LE.le, Finset.exists_max_image, Finset.univ_nonempty, Exists.intro, le_antisymm, Imo2000P3.le_rightmost, ciSup_le, Finset.mem_univ
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P3.exists_eq_leftmost line 89 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nonempty, Fin, Real, Exists, Eq, Imo2000P3.leftmost
Proof uses: And, Membership.mem, Finset, Finset.univ, LE.le, Finset.exists_min_image, Finset.univ_nonempty, Exists.intro, le_antisymm, le_ciInf, Finset.mem_univ, Imo2000P3.leftmost_le
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P3.potential_eq line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Eq, Imo2000P3.potential, HSub.hSub, HMul.hMul, Imo2000P3.rightmost, Finset.sum, Finset.univ
Proof uses: id, Eq.mpr, congrArg, Finset.sum_sub_distrib, HSMul.hSMul, Finset.card, Finset.sum_const, Fintype.card, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, Eq.refl
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P3.potential_nonneg line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, LE.le, OfNat.ofNat, Imo2000P3.potential
Proof uses: Finset.sum_nonneg, HSub.hSub, Imo2000P3.rightmost, Finset.univ, Membership.mem, Finset, Iff.mpr, sub_nonneg, Imo2000P3.le_rightmost
22 instances, coercions and auxiliary constants left out.
lemma Imo2000P3.exists_lt_rightmost line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, LT.lt, OfNat.ofNat, Imo2000P3.potential, Exists, Imo2000P3.rightmost
Proof uses: Decidable.byContradiction, Not, Eq, Finset.sum_eq_zero, Finset.univ, HSub.hSub, Membership.mem, Finset, Iff.mpr, sub_eq_zero, Eq.symm, le_antisymm, Imo2000P3.le_rightmost, Eq.mp, LE.le, Eq.trans, binderNameHint, forall_congr, False.elim, False and 42 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P3.potential_pos line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Exists, Ne, LT.lt, OfNat.ofNat, Imo2000P3.potential
Proof uses: Imo2000P3.rightmost, Decidable.byContradiction, Not, False, Eq.trans, le_antisymm, Imo2000P3.le_rightmost, Eq.mp, LE.le, binderNameHint, forall_congr, Eq.symm, Finset.sum_pos', HSub.hSub, Finset.univ, Membership.mem, Finset, Iff.mpr, sub_nonneg, Exists.intro and 5 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P3.sum_update line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Eq, Finset.sum, Finset.univ, Function.update, HAdd.hAdd, HSub.hSub
Proof uses: Finset.erase, Finset.sum_congr, rfl, Finset, Membership.mem, Function.update_of_ne, Finset.ne_of_mem_erase, Finset.add_sum_erase, Finset.mem_univ, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul and 44 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P3.rightmost_update_of_le line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nonempty, Fin, Real, LE.le, Eq, Imo2000P3.rightmost, Function.update
Proof uses: le_antisymm, ciSup_le, dite, Eq.mpr, id, congrArg, le_of_eq, Function.update_self, Not, Function.update_of_ne, Imo2000P3.le_rightmost, Eq.mp
13 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2000P3.move_potential_bound The key inequality for the necessity direction: a single move decreases the potential by at least (1 / lam - (n - 1)) times the amount by which the rightmost flea advances line 147 source
Source documentation
The key inequality for the necessity direction: a single move decreases the potential by at least (1 / lam - (n - 1)) times the amount by which the rightmost flea advances.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, LT.lt, Fin, Imo2000P3.Move, HMul.hMul, HSub.hSub, HDiv.hDiv, Imo2000P3.rightmost, Imo2000P3.potential
Proof uses: Nonempty, Nonempty.intro, Fin.mk, Exists, And, Eq, Function.update, HAdd.hAdd, Eq.mpr, id, congrArg, rfl, mul_pos, Iff.mpr, sub_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 110 more
162 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
lemma move_potential_bound (hn : 2 ≤ n) {lam : ℝ} (hlam : 0 < lam)
    {x y : Fin n → ℝ} (h : Move lam x y) :
    (1 / lam - ((n : ℝ) - 1)) * (rightmost y - rightmost x) ≤
      potential x - potential y := by
…
```
Mentions: h, Imo2000P3.Move, Imo2000P3.rightmost, Imo2000P3.potential
lemma Imo2000P3.reachable_potential_bound The inequality of move_potential_bound telescopes along any sequence of moves line 213 source
Source documentation
The inequality of move_potential_bound telescopes along any sequence of moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, LT.lt, Fin, Imo2000P3.Reachable, HMul.hMul, HSub.hSub, HDiv.hDiv, Imo2000P3.rightmost, Imo2000P3.potential
Proof uses: Relation.ReflTransGen.rec, Imo2000P3.Move, Relation.ReflTransGen, of_eq_true, Eq.trans, True, congr, congrArg, Inv.inv, congrFun', one_div, sub_self, MulZeroClass.mul_zero, Imo2000P3.move_potential_bound, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne and 69 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma reachable_potential_bound (hn : 2 ≤ n) {lam : ℝ} (hlam : 0 < lam)
    {x y : Fin n → ℝ} (h : Reachable lam x y) :
    (1 / lam - ((n : ℝ) - 1)) * (rightmost y - rightmost x) ≤
      potential x - potential y := by
…
```
Mentions: h, Imo2000P3.Reachable, Imo2000P3.rightmost, Imo2000P3.potential
lemma Imo2000P3.not_allRightOf_of_lt Necessity: if 0 < lam < 1 / (n - 1), then the rightmost flea stays bounded, so the fleas cannot all be moved arbitrarily far to the right line 226 source
Source documentation
Necessity: if 0 < lam < 1 / (n - 1), then the rightmost flea stays bounded, so the fleas cannot all be moved arbitrarily far to the right.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, LT.lt, HDiv.hDiv, HSub.hSub, Not, Imo2000P3.AllRightOf
Proof uses: Nonempty, Fin, Nonempty.intro, Fin.mk, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, lt_of_lt_of_le, one_lt_two, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HMul.hMul and 89 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma not_allRightOf_of_lt (hn : 2 ≤ n) {lam : ℝ} (hlam : 0 < lam)
    (hlt : lam < 1 / ((n : ℝ) - 1)) : ¬ AllRightOf (n := n) lam := by
…
```
Mentions: Imo2000P3.AllRightOf
lemma Imo2000P3.strat_step One step of Woeginger's strategy: move the leftmost flea over the rightmost flea line 264 source
Source documentation
One step of Woeginger's strategy: move the leftmost flea over the rightmost flea. The rightmost flea advances by at least lam * potential x / (n - 1), and the potential does not decrease.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, HDiv.hDiv, HSub.hSub, Fin, LT.lt, Imo2000P3.potential, Exists, And, Imo2000P3.Move, HAdd.hAdd, Imo2000P3.rightmost, HMul.hMul
Proof uses: Nonempty, Nonempty.intro, Fin.mk, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, lt_of_lt_of_le, one_lt_two, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HPow.hPow, Int.rawCast, inferInstance and 108 more
164 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma strat_step (hn : 2 ≤ n) {lam : ℝ} (hlam : 1 / ((n : ℝ) - 1) ≤ lam)
    (x : Fin n → ℝ) (hp : 0 < potential x) :
    ∃ y, Move lam x y ∧
      rightmost x + lam * potential x / ((n : ℝ) - 1) ≤ rightmost y ∧
      potential x ≤ potential y := by
…
```
Mentions: Imo2000P3.potential, Imo2000P3.Move, Imo2000P3.rightmost
lemma Imo2000P3.phase1 Phase 1 of the strategy: after t moves of strat_step, the rightmost flea has advanced by at least t times the fixed positive amount lam * potential x / (n - 1) line 331 source
Source documentation
Phase 1 of the strategy: after t moves of strat_step, the rightmost flea has advanced by at least t times the fixed positive amount lam * potential x / (n - 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, HDiv.hDiv, HSub.hSub, Fin, LT.lt, Imo2000P3.potential, Exists, And, Imo2000P3.Reachable, HAdd.hAdd, Imo2000P3.rightmost, HMul.hMul
Proof uses: Nat.recAux, Exists.intro, And.intro, Relation.ReflTransGen.refl, Imo2000P3.Move, le_rfl, of_eq_true, Eq.trans, True, congrFun', congrArg, CharP.cast_eq_zero, MulZeroClass.zero_mul, add_zero, Imo2000P3.strat_step, lt_of_lt_of_le, cast, Eq.symm, Nat.cast_one, one_lt_two and 77 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma phase1 (hn : 2 ≤ n) {lam : ℝ} (hlam : 1 / ((n : ℝ) - 1) ≤ lam)
    (x : Fin n → ℝ) (hp : 0 < potential x) (t : ℕ) :
    ∃ y, Reachable lam x y ∧ potential x ≤ potential y ∧
      rightmost x + (t : ℝ) * (lam * potential x / ((n : ℝ) - 1)) ≤ rightmost y := by
…
```
Mentions: Imo2000P3.potential, Imo2000P3.Reachable, Imo2000P3.rightmost
lemma Imo2000P3.phase2 Documented declaration: phase2 line 354 source
Source documentation
Phase 2 of the strategy: if the rightmost flea is already to the right of M, then one can move every remaining flea to the right of M, one at a time, by jumping it over the rightmost flea.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, LT.lt, Fin, Finset.card, Finset.filter, Finset.univ, Imo2000P3.rightmost, Exists, And, Imo2000P3.Reachable
Proof uses: Nat.recAux, Eq, Finset, EmptyCollection.emptyCollection, Iff.mp, Finset.card_eq_zero, Nat.le_zero, Exists.intro, And.intro, Relation.ReflTransGen.refl, Imo2000P3.Move, Not, Membership.mem, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, False, True and 94 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
lemma phase2 (hn : 2 ≤ n) {lam : ℝ} (hlam : 0 < lam) (M : ℝ) :
    ∀ m : ℕ, ∀ y : Fin n → ℝ, (univ.filter fun k => y k ≤ M).card ≤ m →
      M < rightmost y → ∃ z, Reachable lam y z ∧ ∀ l, M < z l := by
…
```
Mentions: Imo2000P3.rightmost, Imo2000P3.Reachable
lemma Imo2000P3.allRightOf_of_ge Documented declaration: allRightOf_of_ge line 421 source
Source documentation
Sufficiency: if 1 / (n - 1) ≤ lam, then Woeginger's strategy (first move the rightmost flea far enough to the right by repeatedly jumping the leftmost flea over it, then jump every other flea over the rightmost flea) takes all fleas to the right of any given point M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, HDiv.hDiv, HSub.hSub, Imo2000P3.AllRightOf
Proof uses: Nonempty, Fin, Nonempty.intro, Fin.mk, LT.lt, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, lt_of_lt_of_le, one_lt_two, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast and 85 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma allRightOf_of_ge (hn : 2 ≤ n) {lam : ℝ} (hlam : 1 / ((n : ℝ) - 1) ≤ lam) :
    AllRightOf (n := n) lam := by
…
```
Mentions: Imo2000P3.AllRightOf
determine Imo2000P3.solution_set line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, Real
Proof uses: Set.Ici, HDiv.hDiv, OfNat.ofNat, HSub.hSub
10 instances, coercions and auxiliary constants left out.
problem Imo2000P3.imo2000_p3 line 447 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, Iff, Membership.mem, Set, Imo2000P3.solution_set, And, LT.lt, Imo2000P3.AllRightOf
Proof uses: HSub.hSub, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, lt_of_lt_of_le, one_lt_two, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HMul.hMul, HPow.hPow, Int.rawCast, inferInstance and 49 more
109 instances, coercions and auxiliary constants left out.

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