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

5 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2006, Problem 2

For a given positive integer k find, in terms of k, the minimum value of N for which there is a set of 2k + 1 distinct positive integers that has sum greater than N but every subset of size k has sum at most N / 2.

Imports (13)

Imported by 1 file

Compfiles.lean

determine Usa2006P2.solution line 38 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow
9 instances, coercions and auxiliary constants left out.
lemma Usa2006P2.two_mul_sum_ge Documented declaration: two_mul_sum_ge line 49 source
Source documentation
Lower bound for the sum of a finset of natural numbers bounded below: if every element of J is at least a, then the sum of J is at least the sum of the J.card smallest allowed values a, a+1, .... Equivalently 2 * ∑ j ∈ J, j ≥ J.card * (2 * a + (J.card - 1)); we use this formulation to avoid truncated subtraction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Membership.mem, LE.le, HAdd.hAdd, HMul.hMul, Finset.card, OfNat.ofNat, HPow.hPow, Finset.sum
Proof uses: Finset.strongInductionOn, LT.lt, dite, Finset.Nonempty, Finset.max', Eq, rfl, Finset.max'_mem, Finset.erase, Finset.erase_ssubset, Finset.mem_of_mem_erase, Finset.card_erase_add_one, Finset.add_sum_erase, Finset.Ico, Finset.card_le_card, Finset.le_max', And.right, Ne, Eq.mp, And and 98 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma two_mul_sum_ge (J : Finset ℕ) (a : ℕ) (hJ : ∀ j ∈ J, a ≤ j) :
    J.card * (2 * a) + J.card ^ 2 ≤ 2 * ∑ j ∈ J, j + J.card := by
…
```
lemma Usa2006P2.two_mul_sum_le Documented declaration: two_mul_sum_le line 81 source
Source documentation
Upper bound for the sum of a finset of natural numbers bounded above: if every element of J is at most b, then the sum of J is at most the sum of the J.card largest allowed values b, b-1, .... Equivalently 2 * ∑ j ∈ J, j ≤ J.card * (2 * b + 1 - J.card); we use this formulation to avoid truncated subtraction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Membership.mem, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.sum, HPow.hPow, Finset.card
Proof uses: Finset.strongInductionOn, LT.lt, dite, Finset.Nonempty, Finset.min', Eq, rfl, Finset.min'_mem, Finset.erase, Finset.erase_ssubset, Finset.mem_of_mem_erase, Finset.card_erase_add_one, Finset.add_sum_erase, Finset.Ioc, Finset.card_le_card, Finset.min'_le, And.right, Ne, Eq.mp, And and 98 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma two_mul_sum_le (J : Finset ℕ) (b : ℕ) (hJ : ∀ j ∈ J, j ≤ b) :
    2 * ∑ j ∈ J, j + J.card ^ 2 ≤ 2 * (J.card * b) + J.card := by
…
```
lemma Usa2006P2.two_mul_sum_Icc_one Twice the sum `1 + 2 + line 109 source
Source documentation
Twice the sum 1 + 2 + ... + n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, Finset.sum, Finset.Icc, HAdd.hAdd
Proof uses: Nat.recAux, Eq.mpr, EmptyCollection.emptyCollection, Finset, id, congrArg, Finset.Icc_eq_empty, Finset.sum_empty, Eq.refl, Finset.sum_Icc_succ_top, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 18 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma two_mul_sum_Icc_one (n : ℕ) :
    2 * ∑ i ∈ Finset.Icc 1 n, i = n * (n + 1) := by
…
```
problem Usa2006P2.usa2006_p2 We formalise "every subset of size k has sum at most N / 2" as 2 * ∑ x ∈ t, x ≤ N, which is equivalent for natural numbers line 123 source
Source comment
We formalise "every subset of size k has sum at most N / 2" as `2 * ∑ x ∈ t, x ≤ N`, which is equivalent for natural numbers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, IsLeast, Set.ofPred, Exists, Finset, And, Eq, Finset.card, HAdd.hAdd, HMul.hMul, Membership.mem, Finset.sum, LE.le, Usa2006P2.solution
Proof uses: id, And.intro, Set, HPow.hPow, lowerBounds, Exists.intro, Finset.image, Finset.Icc, Eq.mpr, congrArg, Finset.card_image_of_injOn, HSub.hSub, Nat.card_Icc, Iff.mp, Finset.mem_image, Eq.mp, propext, Finset.mem_Icc, Finset.sum_image, Finset.sum_add_distrib and 130 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 115 steps
Open to load the checked before-and-after goal states.
```
problem usa2006_p2 (k : ℕ) (hk : 0 < k) :
    IsLeast {N : ℕ | ∃ s : Finset ℕ, s.card = 2 * k + 1 ∧ (∀ x ∈ s, 0 < x) ∧
        N < ∑ x ∈ s, x ∧ ∀ t ⊆ s, t.card = k → 2 * ∑ x ∈ t, x ≤ N}
      (solution k) := by
…
```
Mentions: Usa2006P2.solution