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

21 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2003, Problem 3

Let n be a positive integer. For every sequence of integers A = (a₀, a₁, a₂, . . . , aₙ) satisfying 0 ≤ aᵢ ≤ i, for i = 0, . . . , n, we define another sequence t(A) = (t(a₀), t(a₁), t(a₂), . . . , t(aₙ)) by setting t(aᵢ) to be the number of terms in the sequence A that precede the term aᵢ and are different from aᵢ. Show that, starting from any sequence A as above, fewer than n applications of the transformation t lead to a sequence B such that t(B) = B.

Imports (3)

Imported by 1 file

Compfiles.lean

def Usa2003P3.t The transformation t: t a i is the number of terms of a that precede the i-th term and are different from it line 39 source
Source documentation
The transformation t: t a i is the number of terms of a that precede the i-th term and are different from it.
We model the sequence A = (a₀, a₁, …, aₙ) as a function ℕ → ℕ where only the values at 0, 1, …, n are constrained. The problem prescribes integer values, but the constraint 0 ≤ aᵢ allows us to work with natural numbers throughout.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Finset.filter, Ne, Eq, Finset.range
2 instances, coercions and auxiliary constants left out.
```
def t (a : ℕ → ℕ) : ℕ → ℕ :=
…
```
lemma Usa2003P3.t_def line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2003P3.t, Finset.card, Finset.filter, Ne, Finset.range
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Usa2003P3.t_zero line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2003P3.t, OfNat.ofNat
Proof uses: Eq.mpr, Finset.card, Finset.filter, Ne, Finset.range, id, congrArg, Usa2003P3.t_def, EmptyCollection.emptyCollection, Finset, Finset.range_zero, Finset.filter_empty, Finset.card_empty, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P3.t_le line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2003P3.t
Proof uses: Eq.mpr, Finset.card, Finset.filter, Ne, Eq, Finset.range, id, congrArg, Usa2003P3.t_def, le_trans, Finset.card_filter_le, Eq.le, Finset.card_range
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P3.t_eq_zero_of line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Eq, Usa2003P3.t, OfNat.ofNat
Proof uses: Finset, Finset.filter, Ne, Finset.range, EmptyCollection.emptyCollection, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.filter_eq_empty_iff, of_eq_true, Eq.trans, False, True, congrFun', Eq.mp, Finset.mem_range, eq_self and 6 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P3.one_le_t_of line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Ne, LE.le, OfNat.ofNat, Usa2003P3.t
Proof uses: Eq.mpr, Finset.card, Finset.filter, Eq, Finset.range, id, congrArg, Usa2003P3.t_def, Iff.mpr, Finset.Nonempty, Finset.card_pos, Exists, And, Membership.mem, Finset, propext, Finset.filter_nonempty_iff, Exists.intro, And.intro, Finset.mem_range
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P3.le_t If a is admissible at position i, then a i ≤ t a i line 82 source
Source documentation
If a is admissible at position i, then a i ≤ t a i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2003P3.t
Proof uses: Eq.mpr, Finset.card, Finset.filter, Ne, Eq, Finset.range, id, congrArg, Usa2003P3.t_def, dite, OfNat.ofNat, Nat.zero_le, Not, Finset, Membership.mem, And, propext, Finset.mem_filter, LT.lt, Finset.mem_range and 9 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma le_t (a : ℕ → ℕ) (i : ℕ) (h : ∀ j ≤ i, a j ≤ j) : a i ≤ t a i := by
…
```
Mentions: h, Usa2003P3.t
lemma Usa2003P3.iter_succ line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.iterate, Usa2003P3.t, HAdd.hAdd, OfNat.ofNat
Proof uses: Function.iterate_succ_apply'
3 instances, coercions and auxiliary constants left out.
lemma Usa2003P3.iter_t_zero line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.iterate, Usa2003P3.t, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Usa2003P3.iter_succ, Usa2003P3.t_zero
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P3.iter_t_le line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Nat.iterate, Usa2003P3.t, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, Usa2003P3.iter_succ, Usa2003P3.t_le
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P3.iter_mono_succ line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Nat.iterate, Usa2003P3.t, HAdd.hAdd
Proof uses: Eq, Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, Eq.mpr, id, congrArg, Usa2003P3.iter_succ, Usa2003P3.le_t, Usa2003P3.iter_t_le, Eq.symm
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P3.iter_ge_of_le line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Nat.iterate, Usa2003P3.t, OfNat.ofNat
Proof uses: Nat.le_induction, le_trans, HAdd.hAdd, Usa2003P3.iter_mono_succ
7 instances, coercions and auxiliary constants left out.
lemma Usa2003P3.iter_ge_two_of_le line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Nat.iterate, Usa2003P3.t, OfNat.ofNat
Proof uses: Nat.le_induction, le_trans, HAdd.hAdd, Usa2003P3.iter_mono_succ
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P3.iter_congr The values t^[m] a j for j ≤ i only depend on the values a j for j ≤ i line 123 source
Source documentation
The values t^[m] a j for j ≤ i only depend on the values a j for j ≤ i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, Nat.iterate, Usa2003P3.t
Proof uses: Nat.recAux, Eq.mpr, HAdd.hAdd, OfNat.ofNat, id, congrArg, Usa2003P3.iter_succ, Finset.card, Finset.filter, Ne, Finset.range, Usa2003P3.t_def, Finset, Eq.rec, Eq.refl, Finset.filter_congr, Membership.mem, le_trans, le_of_lt, Eq.mp and 5 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma iter_congr {a b : ℕ → ℕ} {i : ℕ} (h : ∀ j ≤ i, a j = b j) :
    ∀ m, ∀ j ≤ i, t^[m] a j = t^[m] b j := by
…
```
Mentions: h, Usa2003P3.t
lemma Usa2003P3.iter_stable_add Once a whole initial segment is stable, it stays stable line 140 source
Source documentation
Once a whole initial segment is stable, it stays stable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, Nat.iterate, Usa2003P3.t, HAdd.hAdd, OfNat.ofNat
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Eq.symm, add_assoc, Usa2003P3.iter_succ, Finset.card, Finset.filter, Ne, Finset.range, Usa2003P3.t_def, Finset, Eq.rec, Eq.refl, Finset.filter_congr, Membership.mem, le_trans, le_of_lt, Eq.mp and 5 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma iter_stable_add (a : ℕ → ℕ) {N p : ℕ}
    (h : ∀ i ≤ N, t^[p] a i = t^[p+1] a i) :
    ∀ q, ∀ i ≤ N, t^[p+q] a i = t^[p+q+1] a i := by
…
```
Mentions: h, Usa2003P3.t
lemma Usa2003P3.iter_eq_zero If the first k terms of a are all zero, they stay zero forever line 159 source
Source documentation
If the first k terms of a are all zero, they stay zero forever.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Eq, OfNat.ofNat, Nat.iterate, Usa2003P3.t, HAdd.hAdd
Proof uses: Nat.recAux, id, Usa2003P3.t_eq_zero_of, Eq.mpr, congrArg, lt_trans, Eq.refl, Usa2003P3.iter_succ
9 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma iter_eq_zero {a : ℕ → ℕ} {k : ℕ} (hz : ∀ i < k, a i = 0) :
    ∀ m, ∀ i < k, t^[m+1] a i = 0 := by
…
```
Mentions: Usa2003P3.t
lemma Usa2003P3.range_add_filter_card Counting elements m < j + k with p m, when p holds on all of [0, k) line 177 source
Source documentation
Counting elements m < j + k with p m, when p holds on all of [0, k).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidablePred, LT.lt, Eq, Finset.card, Finset.filter, Finset.range, HAdd.hAdd
Proof uses: Disjoint, Finset, Finset.map, Function.Embedding.mk, add_left_injective, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, And, Function.Embedding, Exists, False, Eq.mp, Finset.mem_map, Finset.mem_range, Union.union and 19 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma range_add_filter_card (p : ℕ → Prop) [DecidablePred p] (j k : ℕ)
    (hk : ∀ m < k, p m) :
    ((Finset.range (j+k)).filter p).card
      = k + ((Finset.range j).filter (fun l => p (l + k))).card := by
…
```
lemma Usa2003P3.comm1 The key commutation relation for the case a₁ = 1: with bⱼ = t a (j+1) - 1, iterating t on b simulates iterating t on a, shifted by one index line 216 source
Source documentation
The key commutation relation for the case a₁ = 1: with bⱼ = t a (j+1) - 1, iterating t on b simulates iterating t on a, shifted by one index.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Nat.iterate, Usa2003P3.t, HAdd.hAdd, Eq, HSub.hSub
Proof uses: Nat.recAux, id, le_rfl, Eq.mpr, congrArg, Usa2003P3.iter_succ, Finset.card, Finset.filter, Ne, Finset.range, Usa2003P3.t_def, Finset, Finset.filter_congr, Membership.mem, Eq.mp, LT.lt, propext, Finset.mem_range, Iff.intro, Usa2003P3.iter_t_zero and 3 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma comm1 {a : ℕ → ℕ} {n : ℕ}
    (hP1 : ∀ i, 1 ≤ i → i ≤ n → ∀ m, 1 ≤ m → 1 ≤ t^[m] a i) :
    ∀ m, ∀ j, j + 1 ≤ n →
      t^[m] (fun j => t a (j+1) - 1) j + 1 = t^[m+1] a (j+1) := by
…
```
Mentions: Usa2003P3.t
lemma Usa2003P3.comm2 The key commutation relation for the case a₀ = a₁ = ⋯ = aₖ₋₁ = 0 < aₖ: with cⱼ = t^[2] a (j+k) - k, iterating t on c simulates iterating t on a, shifted by k indices line 256 source
Source documentation
The key commutation relation for the case a₀ = a₁ = ⋯ = aₖ₋₁ = 0 < aₖ: with cⱼ = t^[2] a (j+k) - k, iterating t on c simulates iterating t on a, shifted by k indices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Eq, Nat.iterate, Usa2003P3.t, HAdd.hAdd, HSub.hSub
Proof uses: Nat.recAux, id, Eq.mpr, congrArg, Usa2003P3.iter_succ, Finset.card, Finset.filter, Ne, Finset.range, Usa2003P3.t_def, Finset, Finset.filter_congr, Membership.mem, Eq.mp, propext, Finset.mem_range, Iff.intro, add_right_comm, Usa2003P3.range_add_filter_card
28 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma comm2 {a : ℕ → ℕ} {n k : ℕ} (hk1 : 1 ≤ k)
    (hz : ∀ m, ∀ i < k, t^[m+1] a i = 0)
    (hge : ∀ i, k ≤ i → i ≤ n → ∀ m, k ≤ t^[m+2] a i) :
    ∀ m, ∀ j, j + k ≤ n →
      t^[m] (fun j => t^[2] a (j+k) - k) j + k = t^[m+2] a (j+k) := by
…
```
Mentions: Usa2003P3.t
theorem Usa2003P3.main_aux The main induction: after n-1 applications of t, the sequence is stable line 294 source
Source documentation
The main induction: after n-1 applications of t, the sequence is stable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Nat.iterate, Usa2003P3.t, HSub.hSub
Proof uses: Nat.strongRecOn, LT.lt, dite, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Or, id, Eq.mpr, congrArg, Usa2003P3.t_zero, Eq.symm, Usa2003P3.t_eq_zero_of, Iff.mp, Nat.lt_one_iff, Not, le_rfl, Usa2003P3.le_t and 59 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 236 steps (first 200 of 236)
Open to load the checked before-and-after goal states.
```
theorem main_aux (n : ℕ) : 1 ≤ n → ∀ a : ℕ → ℕ, (∀ i ≤ n, a i ≤ i) →
    ∀ i ≤ n, t^[n-1] a i = t^[n] a i := by
…
```
Mentions: Usa2003P3.t
problem Usa2003P3.usa2003_p3 USA Mathematical Olympiad 2003, Problem 3 line 484 source
Source documentation
USA Mathematical Olympiad 2003, Problem 3

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Exists, And, Eq, Nat.iterate, Usa2003P3.t, HAdd.hAdd
Proof uses: Exists.intro, HSub.hSub, And.intro, Eq.mpr, id, congrArg, Nat.sub_one_add_one_eq_of_pos, Usa2003P3.main_aux
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
problem usa2003_p3 (n : ℕ) (hn : 0 < n) (a : ℕ → ℕ) (ha : ∀ i ≤ n, a i ≤ i) :
    ∃ k, k < n ∧ ∀ i ≤ n, t^[k] a i = t^[k+1] a i := by
…
```
Mentions: Usa2003P3.t