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

9 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1997, Problem 1

Let p₁, p₂, p₃, ... be the prime numbers listed in increasing order, and let x₀ be a real number between 0 and 1. For positive integer k, define

xₖ = 0, if xₖ₋₁ = 0, xₖ = {pₖ / xₖ₋₁}, if xₖ₋₁ ≠ 0,

where {x} denotes the fractional part of x. (The fractional part of x is given by x - ⌊x⌋, where ⌊x⌋ is the greatest integer less than or equal to x.)

Find, with proof, all x₀ satisfying 0 < x₀ < 1 for which the sequence x₀, x₁, x₂, ... eventually becomes 0.

Imports (8)

Imported by 1 file

Compfiles.lean

def Usa1997P1.seq The recursion from the problem, parametrized by the sequence p : ℕ → ℕ of positive integers used as numerators, where p k is used at step k + 1 line 44 source
Source documentation
The recursion from the problem, parametrized by the sequence p : ℕ → ℕ of positive integers used as numerators, where p k is used at step k + 1. The problem instantiates p to Nat.nth Nat.Prime, the increasing enumeration of the primes, so that p k is the (k + 1)-th prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
2 instances, coercions and auxiliary constants left out.
```
noncomputable def seq (p : ℕ → ℕ) (x₀ : ℝ) : ℕ → ℝ
  | 0 => x₀
  | k + 1 => if seq p x₀ k = 0 then 0 else Int.fract ((p k : ℝ) / seq p x₀ k)

/-- The answer to the problem: the sequence eventually becomes zero exactly
for the rational numbers in the open interval (0, 1). -/
```
Mentions: answer
determine Usa1997P1.solution_set The answer to the problem: the sequence eventually becomes zero exactly for the rational numbers in the open interval (0, 1) line 50 source
Source documentation
The answer to the problem: the sequence eventually becomes zero exactly for the rational numbers in the open interval (0, 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Inter.inter, Set.Ioo, OfNat.ofNat, Set.range, Rat
8 instances, coercions and auxiliary constants left out.
```
determine solution_set : Set ℝ := Set.Ioo 0 1 ∩ Set.range ((↑) : ℚ → ℝ)
…
```
lemma Usa1997P1.seq_zero line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Usa1997P1.seq, OfNat.ofNat
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Usa1997P1.seq_succ line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Usa1997P1.seq, HAdd.hAdd, OfNat.ofNat, ite, Int.fract, HDiv.hDiv
Proof uses: rfl
17 instances, coercions and auxiliary constants left out.
lemma Usa1997P1.seq_shift Shifting the starting value by one step is the same as shifting the sequence of numerators line 62 source
Source documentation
Shifting the starting value by one step is the same as shifting the sequence of numerators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Usa1997P1.seq, HAdd.hAdd, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma seq_shift (p : ℕ → ℕ) (x₀ : ℝ) :
    ∀ k : ℕ, seq (fun n ↦ p (n + 1)) (seq p x₀ 1) k = seq p x₀ (k + 1)
  | 0 => rfl
  | k + 1 => by
    rw [seq_succ (fun n ↦ p (n + 1)) (seq p x₀ 1) k, seq_shift p x₀ k,
      seq_succ p x₀ (k + 1)]

/-- First direction: starting from a positive rational `a / b`, the sequence
reaches zero, because the numerator strictly decreases at each nonzero step.
(The values `p k` only need to be positive integers; primality is irrelevant
for this direction.) -/
```
Mentions: Usa1997P1.seq, Usa1997P1.seq_succ
lemma Usa1997P1.terminates_of_rat First direction: starting from a positive rational a / b, the sequence reaches zero, because the numerator strictly decreases at each nonzero step line 73 source
Source documentation
First direction: starting from a positive rational a / b, the sequence reaches zero, because the numerator strictly decreases at each nonzero step. (The values p k only need to be positive integers; primality is irrelevant for this direction.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, Eq, Real, Usa1997P1.seq, HDiv.hDiv
Proof uses: Nat.strong_induction_on, Ne, Iff.mpr, Nat.cast_ne_zero, LT.lt.ne', div_ne_zero, HMod.hMod, HMul.hMul, Eq.mpr, ite, Int.fract, id, congrArg, HAdd.hAdd, Usa1997P1.seq_succ, Usa1997P1.seq_zero, ite_eq_right, Nat.cast_mul, of_eq_true, Eq.trans and 48 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma terminates_of_rat :
    ∀ a : ℕ, 0 < a → ∀ p : ℕ → ℕ, (∀ k, 0 < p k) →
      ∀ b : ℕ, 0 < b → ∃ k, seq p ((a : ℝ) / b) k = 0 := by
…
```
Mentions: Usa1997P1.seq
lemma Usa1997P1.rat_cast_of_seq_succ Second direction: if the term at step k + 1 is rational, then so is the term at step k line 102 source
Source documentation
Second direction: if the term at step k + 1 is rational, then so is the term at step k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, Exists, Rat, Eq, Usa1997P1.seq, HAdd.hAdd
Proof uses: dite, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, Rat.cast_zero, eq_self, Not, Ne, Iff.mpr, Nat.cast_ne_zero, LT.lt.ne', HDiv.hDiv, div_ne_zero, Int.floor, Eq.mpr, Int.fract, id and 69 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma rat_cast_of_seq_succ (p : ℕ → ℕ) (hp : ∀ k, 0 < p k) (x₀ : ℝ) (k : ℕ)
    (h : ∃ q : ℚ, seq p x₀ (k + 1) = (q : ℝ)) :
    ∃ q : ℚ, seq p x₀ k = (q : ℝ) := by
…
```
Mentions: h, Usa1997P1.seq
lemma Usa1997P1.rat_cast_of_seq If some term of the sequence is rational, then the starting value is rational (by downward induction) line 131 source
Source documentation
If some term of the sequence is rational, then the starting value is rational (by downward induction).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, Exists, Rat, Eq, Usa1997P1.seq
10 instances, coercions and auxiliary constants left out.
```
lemma rat_cast_of_seq (p : ℕ → ℕ) (hp : ∀ k, 0 < p k) (x₀ : ℝ) :
    ∀ k : ℕ, (∃ q : ℚ, seq p x₀ k = (q : ℝ)) → ∃ q : ℚ, x₀ = (q : ℝ)
  | 0, h => h
  | k + 1, h => rat_cast_of_seq p hp x₀ k (rat_cast_of_seq_succ p hp x₀ k h)

snip end
```
Mentions: Usa1997P1.seq, h, Usa1997P1.rat_cast_of_seq_succ
problem Usa1997P1.usa1997_p1 line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Iff, Exists, Nat, Eq, Usa1997P1.seq, Nat.nth, Nat.Prime, Usa1997P1.solution_set
Proof uses: LT.lt, Nat.Prime.pos, Nat.nth_mem_of_infinite, Nat.infinite_setOfPred_prime, Iff.intro, And.intro, Set.range, Rat, Usa1997P1.rat_cast_of_seq, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, Rat.cast_zero, eq_self, Eq.symm, Iff.mp, Rat.cast_pos and 19 more
66 instances, coercions and auxiliary constants left out.

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