`Compfiles/Usa2005P6.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 2005, Problem 6

For a positive integer m, let s(m) denote the sum of the decimal digits of m. A set S of positive integers is k-stable if s(∑_{x∈X} x) = k for any nonempty subset X ⊆ S. For each integer n ≥ 2 let f(n) be the minimal k for which there exists a k-stable set with n integers. Prove that there are constants 0 < C₁ < C₂ with C₁ log₁₀ n ≤ f(n) ≤ C₂ log₁₀ n.

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa2005P6.s The sum of the decimal digits of m line 32 source
Source documentation
The sum of the decimal digits of m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: List.sum, Nat.digits, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def s (m : ℕ) : ℕ := (Nat.digits 10 m).sum
```
def Usa2005P6.IsStable A set S of positive integers is k-stable if the sum of the elements of any nonempty subset X ⊆ S has digit sum equal to k line 36 source
Source documentation
A set S of positive integers is k-stable if the sum of the elements of any nonempty subset X ⊆ S has digit sum equal to k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: And, Membership.mem, LT.lt, OfNat.ofNat, Finset.powerset, Finset.Nonempty, Eq, Usa2005P6.s, Finset.sum
5 instances, coercions and auxiliary constants left out.
```
def IsStable (k : ℕ) (S : Finset ℕ) : Prop :=
…
```
Mentions: S
def Usa2005P6.f f n is the minimal k for which there exists a k-stable set with n integers line 41 source
Source documentation
f n is the minimal k for which there exists a k-stable set with n integers. (That the defining set is nonempty is proved in stable_exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, And, Usa2005P6.IsStable, Eq, Finset.card
1 instances, coercions and auxiliary constants left out.
```
noncomputable def f (n : ℕ) : ℕ := sInf {k | ∃ S : Finset ℕ, IsStable k S ∧ S.card = n}
…
```
Mentions: S, Usa2005P6.IsStable
lemma Usa2005P6.s_zero line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2005P6.s, OfNat.ofNat
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Usa2005P6.s_eq The defining recurrence of the digit sum, valid for all m line 71 source
Source documentation
The defining recurrence of the digit sum, valid for all m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2005P6.s, HAdd.hAdd, HMod.hMod, OfNat.ofNat, HDiv.hDiv
Proof uses: Ne, Or, eq_or_ne, of_eq_true, Eq.trans, True, congr, congrArg, List, Nat.digits, List.nil, List.sum, Nat.digits_zero, Nat.zero_div, add_zero, eq_self, Eq.symm, Eq.mpr, id, Usa2005P6.s.eq_1 and 9 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma s_eq (m : ℕ) : s m = m % 10 + s (m / 10) := by
…
```
Mentions: Usa2005P6.s
lemma Usa2005P6.s_concat The digits of a concatenation are the concatenation of the digits: if c < 10 ^ e then s (10 ^ e * a + c) = s a + s c line 78 source
Source documentation
The digits of a concatenation are the concatenation of the digits: if c < 10 ^ e then s (10 ^ e * a + c) = s a + s c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Eq, Usa2005P6.s, HAdd.hAdd, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', pow_zero, one_mul, add_zero, eq_self, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Eq.mp, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 42 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma s_concat (e a c : ℕ) (hc : c < 10 ^ e) : s (10 ^ e * a + c) = s a + s c := by
…
```
Mentions: Usa2005P6.s
lemma Usa2005P6.s_complement If a + b = 10 ^ e - 1 then the digits of a and b are complementary, so s a + s b = 9 * e line 103 source
Source documentation
If a + b = 10 ^ e - 1 then the digits of a and b are complementary, so s a + s b = 9 * e.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, HSub.hSub, HPow.hPow, OfNat.ofNat, Usa2005P6.s, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, add_zero, MulZeroClass.mul_zero, eq_self, Eq.symm, Eq.mp, congrFun', pow_zero, Nat.sub_self, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 31 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma s_complement (e a b : ℕ) (h : a + b = 10 ^ e - 1) : s a + s b = 9 * e := by
…
```
Mentions: h, Usa2005P6.s
lemma Usa2005P6.s_pow_ten_sub_one line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2005P6.s, HSub.hSub, HPow.hPow, OfNat.ofNat, HMul.hMul
Proof uses: HAdd.hAdd, Usa2005P6.s_complement, Eq.mpr, id, congrArg, add_zero, Eq.refl, Eq.mp, congrFun'
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2005P6.s_add_le Subadditivity of the digit sum line 124 source
Source documentation
Subadditivity of the digit sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2005P6.s, HAdd.hAdd
Proof uses: Nat.recAux, OfNat.ofNat, of_eq_true, Eq.trans, True, congr, congrArg, add_zero, Eq.symm, Eq, Ne, Or, eq_or_ne, zero_add, Eq.mpr, HMod.hMod, HDiv.hDiv, id, Usa2005P6.s_eq, dite and 13 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma s_add_le (a b : ℕ) : s (a + b) ≤ s a + s b := by
…
```
Mentions: Usa2005P6.s
lemma Usa2005P6.s_pos_of_pos The digit sum of a positive integer is positive line 157 source
Source documentation
The digit sum of a positive integer is positive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Usa2005P6.s
Proof uses: Ne, List, Nat.digits, List.nil, Iff.mpr, Nat.digits_ne_nil_iff_ne_zero, ne_of_gt, List.getLast, Nat.getLast_digit_ne_zero, Eq.mpr, id, Eq, congrArg, propext, Nat.one_le_iff_ne_zero, Eq.mp, List.sum, Membership.mem, List.sum_eq_zero_iff_forall_eq_nat, Usa2005P6.s.eq_1 and 1 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma s_pos_of_pos (m : ℕ) (hm : 0 < m) : 1 ≤ s m := by
…
```
Mentions: Usa2005P6.s
lemma Usa2005P6.nine_le_s_of_dvd Every positive multiple of 10 ^ e - 1 has digit sum at least 9 * e line 168 source
Source documentation
Every positive multiple of 10 ^ e - 1 has digit sum at least 9 * e. The proof repeatedly replaces m by m % 10 ^ e + m / 10 ^ e, which preserves divisibility by 10 ^ e - 1 and does not increase the digit sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Dvd.dvd, HSub.hSub, HPow.hPow, HMul.hMul, Usa2005P6.s
Proof uses: Nat.strong_induction_on, Nat.one_le_pow, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Trans.trans, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.natPow_one, Bool.true, Nat.pow_le_pow_right, dite, Eq, Nat.casesAuxOn, False.elim, Eq.mp, False, Eq.trans and 25 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma nine_le_s_of_dvd (e : ℕ) (he : 1 ≤ e) :
    ∀ m : ℕ, 0 < m → (10 ^ e - 1) ∣ m → 9 * e ≤ s m := by
…
```
Mentions: Usa2005P6.s
lemma Usa2005P6.sum_Icc_id The Gauss sum `1 + 2 + line 215 source
Source documentation
The Gauss sum 1 + 2 + ... + n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, HMul.hMul, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Finset.sum_congr, EmptyCollection.emptyCollection, Finset, Finset.Icc_eq_empty_of_lt, LT.lt, eq_self, Membership.mem, Eq.refl, MulZeroClass.zero_mul, zero_add, mul_one, Insert.insert, Finset.ext and 40 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma sum_Icc_id (n : ℕ) : ∑ i ∈ Finset.Icc 1 n, i = n * (n + 1) / 2 := by
…
```
lemma Usa2005P6.construction Upper bound (construction).* If n * (n + 1) / 2 < 10 ^ e then {10^e - 1, 2 * (10^e - 1), ..., n * (10^e - 1)} is a 9 * e-stable set of n positive integers line 231 source
Source documentation
Upper bound (construction). If n * (n + 1) / 2 < 10 ^ e then {10^e - 1, 2 * (10^e - 1), ..., n * (10^e - 1)} is a 9 * e-stable set of n positive integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HDiv.hDiv, HMul.hMul, HAdd.hAdd, HPow.hPow, And, Usa2005P6.IsStable, Finset.image, HSub.hSub, Finset.Icc, Eq, Finset.card
Proof uses: Nat.one_le_pow, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Trans.trans, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.natPow_one, Nat.pow_le_pow_right, Function.Injective, Nat.mul_right_cancel, And.intro, Membership.mem, Finset, Finset.powerset, Finset.Nonempty, Usa2005P6.s, Finset.sum and 37 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
lemma construction (n e : ℕ) (he : 1 ≤ e) (h : n * (n + 1) / 2 < 10 ^ e) :
    IsStable (9 * e) ((Finset.Icc 1 n).image (· * (10 ^ e - 1))) ∧
    ((Finset.Icc 1 n).image (· * (10 ^ e - 1))).card = n := by
…
```
Mentions: h, Usa2005P6.IsStable
lemma Usa2005P6.stable_lower Documented declaration: stable_lower line 287 source
Source documentation
Lower bound. If S is k-stable and 10 ^ e ≤ S.card + 1, then 9 * e ≤ k: among the S.card + 1 ≥ 10 ^ e prefix sums of an arbitrary ordering of S, two agree modulo 10 ^ e - 1, and their difference is a nonempty subset sum that is a positive multiple of 10 ^ e - 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Usa2005P6.IsStable, HPow.hPow, HAdd.hAdd, Finset.card, HMul.hMul
Proof uses: Membership.mem, LT.lt, Finset.powerset, Finset.Nonempty, Eq, Usa2005P6.s, Finset.sum, Nat.one_le_pow, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, HSub.hSub, Trans.trans, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.natPow_one, Nat.pow_le_pow_right, List and 63 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 76 steps
Open to load the checked before-and-after goal states.
```
lemma stable_lower (k e : ℕ) (he : 1 ≤ e) (S : Finset ℕ) (hS : IsStable k S)
    (hn : 10 ^ e ≤ S.card + 1) : 9 * e ≤ k := by
…
```
Mentions: S, Usa2005P6.IsStable
lemma Usa2005P6.stable_exists The set defining f n is nonempty: the construction with e = Nat.log 10 (n * (n + 1) / 2) + 1 works line 366 source
Source documentation
The set defining f n is nonempty: the construction with e = Nat.log 10 (n * (n + 1) / 2) + 1 works.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Finset, And, Usa2005P6.IsStable, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Nat.log, HDiv.hDiv, Eq, Finset.card
Proof uses: Exists.intro, Finset.image, HSub.hSub, HPow.hPow, Finset.Icc, Usa2005P6.construction, LT.lt, Nat.succ, Nat.lt_pow_succ_log_self, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mp, congrArg, Nat.succ_eq_add_one
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma stable_exists (n : ℕ) :
    ∃ S : Finset ℕ, IsStable (9 * (Nat.log 10 (n * (n + 1) / 2) + 1)) S ∧ S.card = n := by
…
```
Mentions: S, Usa2005P6.IsStable
lemma Usa2005P6.f_spec line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Finset, And, Usa2005P6.IsStable, Usa2005P6.f, Eq, Finset.card
Proof uses: Membership.mem, Set, Set.ofPred, InfSet.sInf, Nat.sInf_mem, Exists.intro, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Nat.log, HDiv.hDiv, Usa2005P6.stable_exists
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2005P6.f_le line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Finset, And, Usa2005P6.IsStable, Eq, Finset.card, LE.le, Usa2005P6.f
Proof uses: Nat.sInf_le, Set.ofPred
1 instances, coercions and auxiliary constants left out.
lemma Usa2005P6.one_le_f Every stable set has stability constant at least 1, hence 1 ≤ f n line 382 source
Source documentation
Every stable set has stability constant at least 1, hence 1 ≤ f n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa2005P6.f
Proof uses: Finset, And, Usa2005P6.IsStable, Eq, Finset.card, Exists, Usa2005P6.f_spec, Membership.mem, LT.lt, Finset.powerset, Finset.Nonempty, Usa2005P6.s, Finset.sum, Eq.mpr, id, congrArg, Eq.symm, propext, Finset.card_pos, Iff.mpr and 4 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma one_le_f (n : ℕ) (hn : 1 ≤ n) : 1 ≤ f n := by
…
```
Mentions: Usa2005P6.f
lemma Usa2005P6.f_lower The lower bound for f n coming from the pigeonhole argument line 393 source
Source documentation
The lower bound for f n coming from the pigeonhole argument.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HPow.hPow, HAdd.hAdd, HMul.hMul, Usa2005P6.f
Proof uses: Finset, And, Usa2005P6.IsStable, Eq, Finset.card, Exists, Usa2005P6.f_spec, Usa2005P6.stable_lower, Eq.mpr, id, congrArg
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma f_lower (n e : ℕ) (he : 1 ≤ e) (hn : 10 ^ e ≤ n + 1) : 9 * e ≤ f n := by
…
```
Mentions: Usa2005P6.f
lemma Usa2005P6.f_upper The upper bound for f n coming from the explicit construction line 398 source
Source documentation
The upper bound for f n coming from the explicit construction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Usa2005P6.f, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Nat.log, HDiv.hDiv
Proof uses: Nat.sInf_le, Set.ofPred, Exists, Finset, And, Usa2005P6.IsStable, Eq, Finset.card, Usa2005P6.stable_exists
15 instances, coercions and auxiliary constants left out.
```
lemma f_upper (n : ℕ) : f n ≤ 9 * (Nat.log 10 (n * (n + 1) / 2) + 1) :=
…
```
Mentions: Usa2005P6.f
problem Usa2005P6.usa2005_p6 line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Nat, LE.le, HMul.hMul, Real.logb, Usa2005P6.f
Proof uses: HDiv.hDiv, Eq.mpr, HPow.hPow, id, Eq, congrArg, propext, Real.le_logb_iff_rpow_le, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, Nat.cast_zero, Decidable.byContradiction, Not, pow_lt_pow_left₀, Eq.mp and 155 more
176 instances, coercions and auxiliary constants left out.

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