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

16 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2007, Problem 1

Let n be a positive integer. Define a sequence by setting a₁ = n and, for each k > 1, letting aₖ be the unique integer in the range 0 ≤ aₖ ≤ k - 1 for which a₁ + a₂ + ··· + aₖ is divisible by k. (For instance, when n = 9 the obtained sequence is 9, 1, 2, 0, 3, 3, 3, ....) Prove that for any n the sequence a₁, a₂, ... eventually becomes constant.

Imports (6)

Imported by 1 file

Compfiles.lean

def Usa2007P1.s The partial sums `s n k = a n 0 + a n 1 + line 35 source
Source documentation
The partial sums s n k = a n 0 + a n 1 + ... + a n k of the sequence of the problem, defined directly: s n 0 = n, and s n (k + 1) is the smallest multiple of k + 2 which is ≥ s n k.

no axioms what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.
```
def s (n : ℕ) : ℕ → ℕ
  | 0 => n
  | (k + 1) => s n k + (k + 2 - s n k % (k + 2)) % (k + 2)

/-- The sequence of the problem, with indices shifted by one so that `a n 0 = n`:
for `k ≥ 1`, `a n k` is the unique integer in `[0, k]` for which `k + 1` divides
`s n k = a n 0 + ... + a n k`. -/
```
Mentions: Usa2007P1.a
def Usa2007P1.a The sequence of the problem, with indices shifted by one so that a n 0 = n: for k ≥ 1, a n k is the unique integer in [0, k] for which k + 1 divides `s n k = a n 0 + line 42 source
Source documentation
The sequence of the problem, with indices shifted by one so that a n 0 = n: for k ≥ 1, a n k is the unique integer in [0, k] for which k + 1 divides s n k = a n 0 + ... + a n k.

no axioms what this means
Statement uses: Nat
Proof uses: Usa2007P1.s.match_1, Unit, HSub.hSub, Usa2007P1.s, HAdd.hAdd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def a (n : ℕ) : ℕ → ℕ
  | 0 => n
  | (k + 1) => s n (k + 1) - s n k

snip begin

-- sanity check against the example given in the problem statement
```
Mentions: Usa2007P1.s
example Usa2007P1.(example at line 49) line 49 source
Source comment
sanity check against the example given in the problem statement
```
example : a 9 0 = 9 ∧ a 9 1 = 1 ∧ a 9 2 = 2 ∧ a 9 3 = 0 ∧ a 9 4 = 3 ∧
    a 9 5 = 3 ∧ a 9 6 = 3 := by
…
```
Mentions: Usa2007P1.a
lemma Usa2007P1.s_succ line 53 source
no axioms what this means
Statement uses: Nat, Eq, Usa2007P1.s, HAdd.hAdd, OfNat.ofNat, HMod.hMod, HSub.hSub
Proof uses: rfl
10 instances, coercions and auxiliary constants left out.
lemma Usa2007P1.a_succ line 56 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Usa2007P1.a, HAdd.hAdd, OfNat.ofNat, HMod.hMod, HSub.hSub, Usa2007P1.s
Proof uses: Nat.add_sub_cancel_left
14 instances, coercions and auxiliary constants left out.
lemma Usa2007P1.s_succ_eq_add_a line 60 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Usa2007P1.s, HAdd.hAdd, OfNat.ofNat, Usa2007P1.a
Proof uses: Eq.mpr, HMod.hMod, HSub.hSub, id, congrArg, Usa2007P1.a_succ, Usa2007P1.s_succ, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P1.a_succ_lt line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Usa2007P1.a, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, HMod.hMod, HSub.hSub, Usa2007P1.s, id, Eq, congrArg, Usa2007P1.a_succ, Nat.mod_lt
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P1.dvd_s line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, HAdd.hAdd, OfNat.ofNat, Usa2007P1.s
Proof uses: Nat.recAux, one_dvd, Eq.mpr, Eq, HMod.hMod, id, congrArg, propext, Nat.dvd_iff_mod_eq_zero, HSub.hSub, Usa2007P1.s_succ, Nat.add_mod, Nat.mod_mod, LT.lt, Eq.symm, Eq.refl, Nat.mod_lt, GT.gt, Or, Nat.eq_zero_or_pos and 9 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
def Usa2007P1.b The average `b n k = (a n 0 + line 82 source
Source documentation
The average b n k = (a n 0 + ... + a n k) / (k + 1), a nonnegative integer.

no axioms what this means
Statement uses: Nat
Proof uses: HDiv.hDiv, Usa2007P1.s, HAdd.hAdd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def b (n k : ℕ) : ℕ := s n k / (k + 1)
```
Mentions: Usa2007P1.s
lemma Usa2007P1.s_eq line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2007P1.s, HMul.hMul, HAdd.hAdd, OfNat.ofNat, Usa2007P1.b
Proof uses: id, Eq.mpr, HDiv.hDiv, congrArg, mul_comm, Nat.div_mul_cancel, Usa2007P1.dvd_s, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P1.b_succ_le line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2007P1.b, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq, Usa2007P1.s, Usa2007P1.a, Usa2007P1.s_succ_eq_add_a, LT.lt, Usa2007P1.a_succ_lt, HMul.hMul, Usa2007P1.s_eq, Decidable.byContradiction, Not, Iff.mp, not_le, Nat.mul_le_mul_left, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr and 24 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P1.b_eventually_const line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, GE.ge, Eq, Usa2007P1.b
Proof uses: Antitone, antitone_nat_of_succ_le, Usa2007P1.b_succ_le, InfSet.sInf, Set.range, Membership.mem, Set, Nat.sInf_mem, Set.range_nonempty, Exists.intro, le_antisymm, Eq.mpr, LE.le, id, congrArg, Nat.sInf_le, rfl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P1.sum_a The partial sums of a n are indeed given by s n line 108 source
Source documentation
The partial sums of a n are indeed given by s n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, Usa2007P1.a, Usa2007P1.s
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Finset.sum_range_one, Eq.refl, Finset.sum_range_succ, Usa2007P1.s_succ_eq_add_a
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma sum_a (n k : ℕ) : ∑ i ∈ Finset.range (k + 1), a n i = s n k := by
…
```
Mentions: Usa2007P1.a, Usa2007P1.s
lemma Usa2007P1.dvd_sum_a a n satisfies the divisibility requirement of the problem statement line 115 source
Source documentation
a n satisfies the divisibility requirement of the problem statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, HAdd.hAdd, OfNat.ofNat, Finset.sum, Finset.range, Usa2007P1.a
Proof uses: Eq.mpr, Usa2007P1.s, id, Eq, congrArg, Usa2007P1.sum_a, Usa2007P1.dvd_s
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_sum_a (n k : ℕ) : (k + 1) ∣ ∑ i ∈ Finset.range (k + 1), a n i := by
…
```
Mentions: Usa2007P1.a
lemma Usa2007P1.a_le a n satisfies the range requirement of the problem statement line 120 source
Source documentation
a n satisfies the range requirement of the problem statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa2007P1.a
Proof uses: Eq, Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, Ne, Iff.mp, LT.lt, Nat.lt_succ_iff, Usa2007P1.a_succ_lt, Eq.symm
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma a_le (n : ℕ) {k : ℕ} (hk : 1 ≤ k) : a n k ≤ k := by
…
```
Mentions: Usa2007P1.a
problem Usa2007P1.usa2007_p1 line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, GE.ge, Eq, Usa2007P1.a
Proof uses: Usa2007P1.b, Usa2007P1.b_eventually_const, Exists.intro, HAdd.hAdd, Nat.succ, Nat.exists_eq_succ_of_ne_zero, Ne, Usa2007P1.s, HMul.hMul, Eq.mpr, id, congrArg, Usa2007P1.s_eq, Eq.refl, Trans.trans, HSub.hSub, rfl, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 22 more
35 instances, coercions and auxiliary constants left out.

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