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

12 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2008, Problem 5

Three nonnegative real numbers r₁, r₂, r₃ are written on a blackboard. These numbers have the property that there exist integers a₁, a₂, a₃, not all zero, satisfying a₁r₁ + a₂r₂ + a₃r₃ = 0. We are permitted to perform the following operation: find two numbers x, y on the blackboard with x ≤ y, then erase y and write y − x in its place. Prove that after a finite number of such operations, we can end up with at least one 0 on the blackboard.

Imports (4)

Imported by 1 file

Compfiles.lean

abbrev Usa2008P5.Step One legal operation of the game: choose two distinct positions i and j with r j ≤ r i, erase the number r i and write r i - r j in its place line 34 source
Source documentation
One legal operation of the game: choose two distinct positions i and j with r j ≤ r i, erase the number r i and write r i - r j in its place.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real
Proof uses: Exists, And, Ne, LE.le, Eq, Function.update, HSub.hSub
6 instances, coercions and auxiliary constants left out.
```
abbrev Step (r r' : Fin 3 → ℝ) : Prop :=
…
```
abbrev Usa2008P5.weight The weight of a coefficient vector: the sum of the absolute values line 50 source
Source documentation
The weight of a coefficient vector: the sum of the absolute values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Int
Proof uses: Finset.sum, Finset.univ, Int.natAbs
4 instances, coercions and auxiliary constants left out.
```
abbrev weight (a : Fin 3 → ℤ) : ℕ := ∑ l, (a l).natAbs
```
lemma Usa2008P5.insert_eq_univ line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Eq, Finset, Insert.insert, Singleton.singleton, Finset.univ
Proof uses: Finset.eq_univ_of_card, Eq.mpr, Finset.card, Fintype.card, HAdd.hAdd, id, congrArg, Finset.card_insert_of_notMem, of_eq_true, Not, Membership.mem, Eq.trans, False, True, Or, congr, eq_false, or_self, not_false_eq_true, Finset.card_pair and 2 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P5.sum3 line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Fin, OfNat.ofNat, Nat, Ne, Eq, Finset.sum, Finset.univ, HAdd.hAdd
Proof uses: Eq.mpr, Insert.insert, Finset, Singleton.singleton, id, congrArg, Eq.symm, Usa2008P5.insert_eq_univ, Finset.sum_insert, of_eq_true, Not, Membership.mem, Eq.trans, False, True, Or, congr, eq_false, or_self, not_false_eq_true and 3 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P5.weight_eq_three line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Int, Eq, Usa2008P5.weight, HAdd.hAdd, Int.natAbs
Proof uses: Usa2008P5.sum3
5 instances, coercions and auxiliary constants left out.
lemma Usa2008P5.move_lemma One step of the first phase of the strategy: if r k ≤ r i, we may erase r i writing r i - r k, and update the coefficients accordingly line 73 source
Source documentation
One step of the first phase of the strategy: if r k ≤ r i, we may erase r i writing r i - r k, and update the coefficients accordingly. The new coefficients still give a zero-sum relation, are not all zero, and their weight strictly decreases, provided that (a k + a i).natAbs < (a k).natAbs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Int, Ne, LE.le, Eq, HAdd.hAdd, HMul.hMul, LT.lt, Int.natAbs, Exists, And, Usa2008P5.Step
Proof uses: Function.update, Function.update_of_ne, Function.update_self, HSub.hSub, Ne.symm, Exists.intro, And.intro, rfl, dite, Eq.mpr, id, congrArg, Iff.mpr, sub_nonneg, Not, propext, Function.ne_iff, congrFun', Int.cast_add, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt and 53 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma move_lemma {r : Fin 3 → ℝ} {a : Fin 3 → ℤ} {i j k : Fin 3}
    (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k)
    (hnn : ∀ l, 0 ≤ r l) (hle : r k ≤ r i)
    (hsum : (a i : ℝ) * r i + (a j : ℝ) * r j + (a k : ℝ) * r k = 0)
    (hane : a i ≠ 0) (hdec : (a k + a i).natAbs < (a k).natAbs) :
    ∃ r' : Fin 3 → ℝ, Step r r' ∧ (∀ l, 0 ≤ r' l) ∧
      ∃ a' : Fin 3 → ℤ, a' ≠ 0 ∧
        (a' i : ℝ) * r' i + (a' j : ℝ) * r' j + (a' k : ℝ) * r' k = 0 ∧
        (a' i).natAbs + (a' j).natAbs + (a' k).natAbs <
          (a i).natAbs + (a j).natAbs + (a k).natAbs := by
…
```
Mentions: Usa2008P5.Step
lemma Usa2008P5.phase1_pos Documented declaration: phase1_pos line 109 source
Source documentation
The first phase of the strategy, under the normalization 0 < a i where i is the position of the largest number: there is always a legal move after which the weight of the coefficients strictly decreases.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Int, Ne, LT.lt, Eq, HAdd.hAdd, HMul.hMul, Exists, And, Usa2008P5.Step, LE.le, Finset.sum, Finset.univ, Usa2008P5.weight
Proof uses: Or, lt_or_gt_of_ne, abs, lt_or_ge, Int.natAbs, Eq.mpr, id, congrArg, Eq.symm, propext, Int.ofNat_lt, Int.natCast_natAbs, add_comm, Usa2008P5.move_lemma, Ne.symm, LT.lt.le, le_of_lt, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl and 78 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 143 steps
Open to load the checked before-and-after goal states.
```
lemma phase1_pos {r : Fin 3 → ℝ} {a : Fin 3 → ℤ} {i j k : Fin 3}
    (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k)
    (hrj : r j < r i) (hrk : r k < r j) (hpos : ∀ l, 0 < r l)
    (hai : 0 < a i) (haj : a j ≠ 0) (hak : a k ≠ 0)
    (hsum : (a i : ℝ) * r i + (a j : ℝ) * r j + (a k : ℝ) * r k = 0) :
    ∃ r' : Fin 3 → ℝ, Step r r' ∧ (∀ l, 0 ≤ r' l) ∧
      ∃ a' : Fin 3 → ℤ, a' ≠ 0 ∧ (∑ l, (a' l : ℝ) * r' l = 0) ∧ weight a' < weight a := by
…
```
Mentions: Usa2008P5.Step, Usa2008P5.weight
lemma Usa2008P5.phase1_core The first phase of the strategy: as long as no coefficient is zero, there is a legal move after which the weight of the coefficients strictly decreases line 242 source
Source documentation
The first phase of the strategy: as long as no coefficient is zero, there is a legal move after which the weight of the coefficients strictly decreases.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Int, Ne, LT.lt, Eq, HAdd.hAdd, HMul.hMul, Exists, And, Usa2008P5.Step, LE.le, Finset.sum, Finset.univ, Usa2008P5.weight
Proof uses: Or, lt_or_gt_of_ne, Neg.neg, Eq.mpr, id, congrFun', congrArg, congr, Int.cast_neg, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 58 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma phase1_core {r : Fin 3 → ℝ} {a : Fin 3 → ℤ} {i j k : Fin 3}
    (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k)
    (hrj : r j < r i) (hrk : r k < r j) (hpos : ∀ l, 0 < r l)
    (hai : a i ≠ 0) (haj : a j ≠ 0) (hak : a k ≠ 0)
    (hsum : (a i : ℝ) * r i + (a j : ℝ) * r j + (a k : ℝ) * r k = 0) :
    ∃ r' : Fin 3 → ℝ, Step r r' ∧ (∀ l, 0 ≤ r' l) ∧
      ∃ a' : Fin 3 → ℤ, a' ≠ 0 ∧ (∑ l, (a' l : ℝ) * r' l = 0) ∧ weight a' < weight a := by
…
```
Mentions: Usa2008P5.Step, Usa2008P5.weight
lemma Usa2008P5.euclid The subtractive Euclidean algorithm on one pair of positions line 269 source
Source documentation
The subtractive Euclidean algorithm on one pair of positions. If the values at positions i and j are positive integer multiples p * t and q * t of a common positive real t, then by repeatedly erasing the larger of the two we can reach a board containing 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Real, Eq, HAdd.hAdd, LE.le, LT.lt, Ne, HMul.hMul, Exists, And, Relation.ReflTransGen, Usa2008P5.Step
Proof uses: Nat.strong_induction_on, Or, lt_trichotomy, Eq.mpr, id, congrArg, mul_le_mul_of_nonneg_right, cast, Eq.symm, LT.lt.le, Function.update, HSub.hSub, rfl, Exists.intro, And.intro, Ne.symm, dite, Function.update_self, Iff.mpr, sub_nonneg and 48 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
```
lemma euclid : ∀ n : ℕ, ∀ (r : Fin 3 → ℝ) (t : ℝ) (i j : Fin 3) (p q : ℕ),
    p + q = n → (∀ l, 0 ≤ r l) → 0 < t → i ≠ j → 0 < p → 0 < q →
    r i = (p : ℝ) * t → r j = (q : ℝ) * t →
    ∃ r' : Fin 3 → ℝ, Relation.ReflTransGen Step r r' ∧ ∃ l, r' l = 0 := by
…
```
Mentions: Usa2008P5.Step
lemma Usa2008P5.phase2 Documented declaration: phase2 line 336 source
Source documentation
The second phase of the strategy: if some coefficient is zero, then the other two coefficients are nonzero and the corresponding numbers have a rational ratio, so the Euclidean algorithm finishes the game.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Int, Ne, LT.lt, Eq, HAdd.hAdd, HMul.hMul, Exists, And, Relation.ReflTransGen, Usa2008P5.Step
Proof uses: Or, Membership.mem, Finset, Insert.insert, Singleton.singleton, Eq.mpr, Finset.univ, id, congrArg, Usa2008P5.insert_eq_univ, Finset.mem_univ, Eq.mp, Eq.trans, False, Iff.mp, mul_eq_zero, zero_add, MulZeroClass.zero_mul, Int.cast_zero, add_zero and 99 more
167 instances, coercions and auxiliary constants left out.

Tactic trace: 93 steps
Open to load the checked before-and-after goal states.
```
lemma phase2 {r : Fin 3 → ℝ} {a : Fin 3 → ℤ} {i j k : Fin 3}
    (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k)
    (hpos : ∀ l, 0 < r l) (ha : a ≠ 0) (hak : a k = 0)
    (hsum : (a i : ℝ) * r i + (a j : ℝ) * r j + (a k : ℝ) * r k = 0) :
    ∃ r' : Fin 3 → ℝ, Relation.ReflTransGen Step r r' ∧ ∃ l, r' l = 0 := by
…
```
Mentions: Usa2008P5.Step
lemma Usa2008P5.key The key lemma, proved by strong induction on the weight of the coefficient vector: one can always reach a board containing 0 line 421 source
Source documentation
The key lemma, proved by strong induction on the weight of the coefficient vector: one can always reach a board containing 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Real, Int, Eq, Usa2008P5.weight, LE.le, Ne, Finset.sum, Finset.univ, HMul.hMul, Exists, And, Relation.ReflTransGen, Usa2008P5.Step
Proof uses: Nat.strong_induction_on, LT.lt, dite, Exists.intro, And.intro, Relation.ReflTransGen.refl, Not, Function.update, HSub.hSub, Relation.ReflTransGen.single, le_of_eq, Eq.symm, rfl, Eq.mpr, id, congrArg, Function.update_self, sub_self, Eq.refl, lt_of_le_of_ne' and 36 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 112 steps
Open to load the checked before-and-after goal states.
```
lemma key : ∀ n : ℕ, ∀ (r : Fin 3 → ℝ) (a : Fin 3 → ℤ),
    weight a = n → (∀ l, 0 ≤ r l) → a ≠ 0 → (∑ l, (a l : ℝ) * r l) = 0 →
    ∃ r' : Fin 3 → ℝ, Relation.ReflTransGen Step r r' ∧ ∃ l, r' l = 0 := by
…
```
Mentions: Usa2008P5.weight, Usa2008P5.Step
problem Usa2008P5.usa2008_p5 line 502 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, LE.le, Int, Ne, Eq, Finset.sum, Finset.univ, HMul.hMul, Exists, And, Relation.ReflTransGen, Usa2008P5.Step
Proof uses: Usa2008P5.key, Usa2008P5.weight, rfl
28 instances, coercions and auxiliary constants left out.