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

15 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2009, Problem 6

Let $s_1, s_2, s_3, \ldots$ be an infinite, nonconstant sequence of rational numbers, meaning it is not the case that $s_1 = s_2 = s_3 = \ldots$. Suppose that $t_1, t_2, t_3, \ldots$ is also an infinite, nonconstant sequence of rational numbers with the property that $(s_i - s_j)(t_i - t_j)$ is an integer for all $i$ and $j$. Prove that there exists a rational number $r$ such that $(s_i - s_j) r$ and $(t_i - t_j)/r$ are integers for all $i$ and $j$.

Imports (8)

Imported by 1 file

Compfiles.lean

def Usa2009P6.IsInt The predicate that a rational number is an integer line 37 source
Source documentation
The predicate that a rational number is an integer.

standard axioms: Quot.sound, propext what this means
Statement uses: Rat
Proof uses: Exists, Int, Eq
2 instances, coercions and auxiliary constants left out.
```
def IsInt (x : ℚ) : Prop := ∃ k : ℤ, x = k
```
lemma Usa2009P6.IsInt.of_int line 39 source
standard axioms: Quot.sound, propext what this means
Statement uses: Int, Usa2009P6.IsInt, Rat
Proof uses: Exists.intro, Eq, rfl
4 instances, coercions and auxiliary constants left out.
lemma Usa2009P6.IsInt.add line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat, Usa2009P6.IsInt, HAdd.hAdd
Proof uses: Int, Eq, Exists.intro, Eq.mpr, id, congrArg, Int.cast_add, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2009P6.IsInt.sub line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat, Usa2009P6.IsInt, HSub.hSub
Proof uses: Int, Eq, Exists.intro, Eq.mpr, id, congrArg, Int.cast_sub, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2009P6.IsInt.val_nonneg An integer has nonnegative p-adic valuation line 52 source
Source documentation
An integer has nonnegative p-adic valuation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat, Usa2009P6.IsInt, Nat, LE.le, Int, OfNat.ofNat, padicValRat
Proof uses: Eq, Eq.mpr, padicValInt, id, congrArg, padicValRat.of_int, Nat.cast_nonneg, Eq.symm
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma IsInt.val_nonneg {x : ℚ} (hx : IsInt x) (p : ℕ) : 0 ≤ padicValRat p x := by
…
```
Mentions: Usa2009P6.IsInt
lemma Usa2009P6.isInt_of_val_nonneg A rational number whose p-adic valuation is nonnegative for every prime p is an integer line 59 source
Source documentation
A rational number whose p-adic valuation is nonnegative for every prime p is an integer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat, Nat, Nat.Prime, LE.le, Int, OfNat.ofNat, padicValRat, Usa2009P6.IsInt
Proof uses: Eq, Rat.den, Decidable.byContradiction, Not, And, Dvd.dvd, Exists, False, Nat.exists_prime_and_dvd, padicValInt, Rat.num, Eq.mpr, Or, id, congrArg, propext, padicValInt.eq_zero_iff, Or.inr, Int.natAbs, Iff.mp and 30 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma isInt_of_val_nonneg {q : ℚ} (h : ∀ p : ℕ, p.Prime → 0 ≤ padicValRat p q) : IsInt q := by
…
```
Mentions: h, Usa2009P6.IsInt
lemma Usa2009P6.isInt_of_mul_add_int Key integrality step: if a * b and n * a + b are integers (with n a nonzero integer), then b (and hence n * a) is an integer line 88 source
Source documentation
Key integrality step: if a * b and n * a + b are integers (with n a nonzero integer), then b (and hence n * a) is an integer. This is the p-adic heart of the proof that every tᵢ is an integer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Ne, OfNat.ofNat, Rat, Usa2009P6.IsInt, HMul.hMul, HAdd.hAdd, And
Proof uses: Classical.byContradiction, Not, Nat, Nat.Prime, LT.lt, padicValRat, Exists, False, Usa2009P6.isInt_of_val_nonneg, Eq.mp, LE.le, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Fact, Fact.mk, Eq and 91 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
```
lemma isInt_of_mul_add_int {n : ℤ} (hn : n ≠ 0) {a b : ℚ}
    (h1 : IsInt (a * b)) (h2 : IsInt ((n : ℚ) * a + b)) :
    IsInt b ∧ IsInt ((n : ℚ) * a) := by
…
```
Mentions: Usa2009P6.IsInt
def Usa2009P6.seqGcd The gcd of |T 0|, |T 1|, ..., |T k| line 142 source
Source documentation
The gcd of |T 0|, |T 1|, ..., |T k|.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: Finset.gcd, Finset.range, HAdd.hAdd, OfNat.ofNat, Int.natAbs
6 instances, coercions and auxiliary constants left out.
```
def seqGcd (T : ℕ → ℤ) (k : ℕ) : ℕ := (Finset.range (k + 1)).gcd fun i => (T i).natAbs
```
lemma Usa2009P6.seqGcd_dvd line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, Dvd.dvd, Usa2009P6.seqGcd, Int.natAbs
Proof uses: Finset.gcd_dvd, Finset.range, HAdd.hAdd, OfNat.ofNat, Iff.mpr, Membership.mem, Finset, LT.lt, Finset.mem_range, Nat.lt_succ_of_le
12 instances, coercions and auxiliary constants left out.
lemma Usa2009P6.seqGcd_ne_zero line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, Ne, OfNat.ofNat, Usa2009P6.seqGcd
Proof uses: Eq, Iff.mp, Int.natAbs, Int.natAbs_eq_zero, Nat.eq_zero_of_zero_dvd, Eq.rec, Dvd.dvd, Usa2009P6.seqGcd_dvd
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2009P6.seqGcd_succ_le line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, Ne, OfNat.ofNat, Usa2009P6.seqGcd, HAdd.hAdd
Proof uses: Nat.le_of_dvd, Nat.pos_of_ne_zero, Usa2009P6.seqGcd_ne_zero, Finset.dvd_gcd, Finset.range, Int.natAbs, Membership.mem, Finset, Usa2009P6.seqGcd_dvd, le_trans, Iff.mp, LT.lt, Nat.succ, Nat.lt_succ_iff, Finset.mem_range, Nat.le_succ
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2009P6.gcd_seq Documented declaration: gcd_seq line 161 source
Source documentation
Any sequence of integers containing a nonzero term has a greatest common divisor: a positive natural d dividing every term, and such that for every prime p the p-adic valuation of d is attained at some nonzero term of the sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Ne, OfNat.ofNat, Exists, And, Dvd.dvd, Nat.Prime, Eq, padicValInt, padicValNat
Proof uses: Antitone, Usa2009P6.seqGcd, HAdd.hAdd, antitone_nat_of_succ_le, Usa2009P6.seqGcd_succ_le, Nat.add, Nat.le_add_right, Set.Nonempty, Set.range, Set.range_nonempty, InfSet.sInf, Membership.mem, Set, Nat.sInf_mem, LE.le, le_antisymm, Trans.trans, rfl, Nat.sInf_le, Exists.intro and 42 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
lemma gcd_seq (T : ℕ → ℤ) {b : ℕ} (hb : T b ≠ 0) :
    ∃ d : ℕ, d ≠ 0 ∧ (∀ i, (d : ℤ) ∣ T i) ∧
      ∀ p : ℕ, p.Prime → ∃ j, T j ≠ 0 ∧ padicValInt p (T j) = padicValNat p d := by
…
```
lemma Usa2009P6.s_val_ge The key valuation bound: if tⱼ is a nonzero integer of p-adic valuation e (the minimum among the t's), then every sᵢ has p-adic valuation at least -e line 219 source
Source documentation
The key valuation bound: if tⱼ is a nonzero integer of p-adic valuation e (the minimum among the t's), then every sᵢ has p-adic valuation at least -e.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Int, LE.le, OfNat.ofNat, Rat, Usa2009P6.IsInt, HMul.hMul, HAdd.hAdd, Ne, Eq, padicValRat, Neg.neg
Proof uses: Fact, Fact.mk, Or, eq_or_ne, Eq.mpr, id, congrArg, Eq.trans, padicValRat.zero, Iff.mpr, neg_nonpos, Decidable.byContradiction, Not, Usa2009P6.IsInt.val_nonneg, Exists.intro, rfl, padicValRat.mul, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl and 73 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
```
lemma s_val_ge {p : ℕ} (hp : p.Prime) {e : ℤ} (he : 0 ≤ e) {sj tj si ti : ℚ}
    (hstj : IsInt (sj * tj)) (hsti : IsInt (si * ti))
    (hcross : IsInt (si * tj + sj * ti)) (htj : tj ≠ 0) (htjv : padicValRat p tj = e) :
    -e ≤ padicValRat p si := by
…
```
Mentions: Usa2009P6.IsInt
lemma Usa2009P6.normalized The heart of the problem, for normalized sequences: s a = t a = 0, s b = 1 and t b = n for a nonzero integer n line 280 source
Source documentation
The heart of the problem, for normalized sequences: s a = t a = 0, s b = 1 and t b = n for a nonzero integer n. Then r = d, the gcd of all the tᵢ (which are integers), works.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat, Int, Ne, OfNat.ofNat, Eq, Usa2009P6.IsInt, HMul.hMul, HSub.hSub, Exists, And, HDiv.hDiv
Proof uses: Exists.intro, Eq.mp, congrArg, sub_zero, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right and 83 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
lemma normalized {s t : ℕ → ℚ} {a b : ℕ} {n : ℤ} (hn : n ≠ 0)
    (hsa : s a = 0) (hta : t a = 0) (hsb : s b = 1) (htb : t b = n)
    (h : ∀ i j, IsInt ((s i - s j) * (t i - t j))) :
    ∃ r : ℚ, r ≠ 0 ∧ (∀ i, IsInt (s i * r)) ∧ (∀ i, IsInt (t i / r)) := by
…
```
Mentions: h, Usa2009P6.IsInt
problem Usa2009P6.usa2009_p6 line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat, Not, Eq, Exists, Int, HMul.hMul, HSub.hSub, And, Ne, OfNat.ofNat, HDiv.hDiv
Proof uses: Classical.byContradiction, False, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Or, Iff.mp, mul_eq_zero, binderNameHint, forall_congr, absurd, sub_eq_zero, Ne.ne_or_ne, Eq.rec, Eq.mpr, id, sub_self, MulZeroClass.zero_mul and 103 more
110 instances, coercions and auxiliary constants left out.

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