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

USA Mathematical Olympiad 1993, Problem 4

The sequence aₙ of odd positive integers is defined as follows: a₁ = r, a₂ = s, and aₙ is the greatest odd divisor of aₙ₋₁ + aₙ₋₂. Show that, for sufficiently large n, aₙ is constant and find this constant (in terms of r and s).

Imports (4)

Imported by 1 file

Compfiles.lean

determine Usa1993P4.constant_value The constant value that the sequence eventually takes line 30 source
Source documentation
The constant value that the sequence eventually takes.

no axioms what this means
Statement uses: Nat
Proof uses: Nat.gcd
```
determine constant_value (r s : ℕ) : ℕ := Nat.gcd r s
…
```
theorem Usa1993P4.ordCompl_two_mul Dividing out all factors of two from 2 * m yields m when m is odd line 35 source
Source documentation
Dividing out all factors of two from 2 * m yields m when m is odd.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, HDiv.hDiv, HMul.hMul, OfNat.ofNat, HPow.hPow, Finsupp, Nat.factorization
Proof uses: Ne, HAdd.hAdd, Nat.Prime.factorization_self, Nat.prime_two, Not, Dvd.dvd, Iff.mpr, Even, Nat.not_even_iff_odd, even_iff_two_dvd, Nat.factorization_eq_zero_of_not_dvd, Eq.mpr, id, congrArg, Nat.factorization_mul, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false and 2 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem ordCompl_two_mul {m : ℕ} (hm : Odd m) : ordCompl[2] (2 * m) = m := by
…
```
theorem Usa1993P4.odd_and_pos Every term of the sequence is odd and positive line 54 source
Source documentation
Every term of the sequence is odd and positive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization, And, LT.lt
Proof uses: Nat.twoStepInduction, Eq.mpr, id, congrArg, And.intro, HMul.hMul, Ne, Not, Dvd.dvd, Nat.not_dvd_ordCompl, Nat.prime_two, Iff.mp, Even, Nat.not_even_iff_odd, even_iff_two_dvd, Nat.ordCompl_pos
52 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem odd_and_pos (n : ℕ) : Odd (a n) ∧ 0 < a n := by
…
```
theorem Usa1993P4.le_half Each term is at most half the sum of the two previous terms line 72 source
Source documentation
Each term is at most half the sum of the two previous terms.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization, LE.le
Proof uses: LT.lt, And, Usa1993P4.odd_and_pos, Ne, Dvd.dvd, Even.two_dvd, Odd.add_odd, Nat.Prime.factorization_pos_of_dvd, Nat.prime_two, pow_le_pow_right₀, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, HMul.hMul, Trans.trans, Nat.mul_le_mul, Eq.mp, congrArg and 5 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem le_half (n : ℕ) : a (n + 2) ≤ (a (n + 1) + a n) / 2 := by
…
```
theorem Usa1993P4.descent If two consecutive terms differ, the maximum of the pair strictly decreases two steps later line 92 source
Source documentation
If two consecutive terms differ, the maximum of the pair strictly decreases two steps later.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization, Ne, LT.lt, Max.max
Proof uses: LE.le, Usa1993P4.le_half
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem descent (n : ℕ) (hne : a n ≠ a (n + 1)) :
    max (a (n + 2)) (a (n + 3)) < max (a n) (a (n + 1)) := by
…
```
theorem Usa1993P4.eventual_eq Some two consecutive terms are eventually equal line 99 source
Source documentation
Some two consecutive terms are eventually equal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization, Exists
Proof uses: Classical.byContradiction, Not, LE.le, Max.max, HMul.hMul, Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, congr, MulZeroClass.mul_zero, zero_add, add_zero, LT.lt, Usa1993P4.descent, Eq.mp, Ne, id and 4 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem eventual_eq : ∃ n, a n = a (n + 1) := by
…
```
theorem Usa1993P4.stable Once two consecutive terms agree, the sequence is constant from then on line 117 source
Source documentation
Once two consecutive terms agree, the sequence is constant from then on.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization
Proof uses: Nat.twoStepInduction, of_eq_true, Eq.trans, True, congrFun', congrArg, add_zero, eq_self, Eq.symm, And.left, LT.lt, Usa1993P4.odd_and_pos, rfl, Eq.mpr, id, Eq.mp, HMul.hMul, two_mul, Usa1993P4.ordCompl_two_mul
43 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem stable (n : ℕ) (h : a n = a (n + 1)) (k : ℕ) : a (n + k) = a n := by
…
```
Mentions: h
theorem Usa1993P4.gcd_invariant The gcd of two consecutive terms is preserved by the recurrence line 131 source
Source documentation
The gcd of two consecutive terms is preserved by the recurrence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization, Nat.gcd
Proof uses: LT.lt, And, Usa1993P4.odd_and_pos, Ne, HMul.hMul, Nat.ordProj_mul_ordCompl_eq_self, Nat.Coprime, Nat.Coprime.pow_left, Iff.mpr, Nat.coprime_two_left, Nat.Coprime.gcd_mul_left_cancel_right, Eq.mpr, id, congrArg, Eq.symm, Nat.gcd_self_add_right, Nat.gcd_comm, Eq.refl
33 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem gcd_invariant (n : ℕ) :
    Nat.gcd (a (n + 1)) (a (n + 2)) = Nat.gcd (a n) (a (n + 1)) := by
…
```
theorem Usa1993P4.gcd_eq The gcd of any two consecutive terms equals gcd r s line 145 source
Source documentation
The gcd of any two consecutive terms equals gcd r s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization, Nat.gcd
Proof uses: Nat.recAux, id, Eq.mpr, congrArg, Eq.refl, Eq.symm, Usa1993P4.gcd_invariant
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem gcd_eq (n : ℕ) : Nat.gcd (a n) (a (n + 1)) = Nat.gcd r s := by
…
```
problem Usa1993P4.usa1993_p4 line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization, Exists, LE.le, Usa1993P4.constant_value
Proof uses: Usa1993P4.eventual_eq, Nat.gcd, Usa1993P4.gcd_eq, Exists.intro, Nat.exists_eq_add_of_le, Eq.mpr, id, congrArg, Usa1993P4.stable, Eq.mp, Nat.gcd_self, Eq.symm, Eq.refl
32 instances, coercions and auxiliary constants left out.

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