`Compfiles/Usa1996P2.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 1996, Problem 2

Let S be a set of n positive integers. Let P be the set of all integers which are the sum of one or more distinct elements of S. Show that we can find n subsets of P whose union is P such that if a, b belong to the same subset, then a ≤ 2b.

Imports (3)

Imported by 1 file

Compfiles.lean

def Usa1996P2.SubsetSums The set of all sums of one or more distinct elements of S line 29 source
Source documentation
The set of all sums of one or more distinct elements of S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Set
Proof uses: Set.ofPred, Exists, And, LE.le, Finset.Nonempty, Eq, Finset.sum, id
4 instances, coercions and auxiliary constants left out.
```
def SubsetSums (S : Finset ℕ) : Set ℕ :=
…
```
Mentions: S
def Usa1996P2.prefixSum The sum of the m smallest elements of S, taken in increasing order line 37 source
Source documentation
The sum of the m smallest elements of S, taken in increasing order.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Finset.sum, Fin, Finset.card, Finset.filter, LT.lt, Finset.univ, OrderEmbedding, Finset.orderEmbOfFin
16 instances, coercions and auxiliary constants left out.
```
def prefixSum (m : ℕ) : ℕ :=
…
```
lemma Usa1996P2.prefixSum_zero line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Eq, Usa1996P2.prefixSum, OfNat.ofNat
Proof uses: Eq.mpr, Finset.sum, Fin, Finset.card, Finset.filter, LT.lt, Finset.univ, OrderEmbedding, Finset.orderEmbOfFin, id, congrArg, Usa1996P2.prefixSum.eq_1, EmptyCollection.emptyCollection, Finset.filter_false_of_mem, Membership.mem, Nat.not_lt_zero, Finset.sum_empty, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1996P2.prefixSum_succ line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, LT.lt, Finset.card, Eq, Usa1996P2.prefixSum, HAdd.hAdd, OfNat.ofNat, OrderEmbedding, Fin, Finset.orderEmbOfFin, rfl, Fin.mk
Proof uses: Finset.filter, Finset.univ, Insert.insert, Finset.ext, Eq.mpr, Iff, Membership.mem, Or, id, congr, congrArg, Eq.trans, And, True, congrFun', true_and, Iff.intro, Iff.mp, Nat.succ, Nat.lt_succ_iff_lt_or_eq and 15 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Usa1996P2.sum_eq_sum_univ line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Eq, Finset.sum, id, Fin, Finset.card, Finset.univ, OrderEmbedding, Finset.orderEmbOfFin, rfl
Proof uses: Eq.mpr, Finset.map, RelEmbedding.toEmbedding, LE.le, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Finset.map_orderEmbOfFin_univ, Function.Embedding, Finset.sum_map
25 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1996P2.prefixSum_card line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Eq, Usa1996P2.prefixSum, Finset.card, Finset.sum, id
Proof uses: Fin, Finset.filter, LT.lt, Finset.univ, Finset.filter_true_of_mem, Membership.mem, Fin.isLt, Eq.mpr, OrderEmbedding, Finset.orderEmbOfFin, congrArg, Usa1996P2.prefixSum.eq_1, rfl, Usa1996P2.sum_eq_sum_univ, Eq.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa1996P2.sum_eq_sum_filter The sum over a subset A of S reindexed by the increasing enumeration of S line 78 source
Source documentation
The sum over a subset A of S reindexed by the increasing enumeration of S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, LE.le, Eq, Finset.sum, id, Fin, Finset.card, Finset.filter, Membership.mem, OrderEmbedding, Finset.orderEmbOfFin, rfl, Finset.univ
Proof uses: Finset.map, RelEmbedding.toEmbedding, Finset.ext, Eq.mpr, Iff, Exists, And, Function.Embedding, congrFun', congrArg, Eq.trans, funext, True, true_and, Iff.intro, Set, Set.range, Finset.range_orderEmbOfFin, Exists.intro, And.intro and 4 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma sum_eq_sum_filter (A : Finset ℕ) (hA : A ⊆ S) :
    A.sum id =
      ∑ i ∈ Finset.univ.filter (fun i : Fin S.card ↦ S.orderEmbOfFin rfl i ∈ A),
        S.orderEmbOfFin rfl i := by
…
```
Mentions: S
lemma Usa1996P2.prefixSum_succ_lt_two_mul_sum Documented declaration: prefixSum_succ_lt_two_mul_sum line 103 source
Source documentation
The key estimate: a subset sum strictly larger than the sum of the m smallest elements must use some element with index at least m, hence is at least the m-th smallest element, and twice the sum exceeds the m + 1 prefix sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, LE.le, LT.lt, Finset.card, Usa1996P2.prefixSum, Finset.sum, id, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: Eq, Fin, Finset.filter, Membership.mem, OrderEmbedding, Finset.orderEmbOfFin, rfl, Finset.univ, Usa1996P2.sum_eq_sum_filter, Exists, And, Decidable.byContradiction, Not, Iff.mpr, Finset.mem_filter_univ, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq and 11 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma prefixSum_succ_lt_two_mul_sum (A : Finset ℕ) (hAS : A ⊆ S)
    (m : ℕ) (hm : m < S.card) (hx : prefixSum S m < A.sum id) :
    prefixSum S (m + 1) < 2 * A.sum id := by
…
```
Mentions: S, Usa1996P2.prefixSum
problem Usa1996P2.usa1996_p2 line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Membership.mem, LT.lt, OfNat.ofNat, Exists, Fin, Finset.card, Set, And, LE.le, Usa1996P2.SubsetSums, Eq, Set.iUnion, HMul.hMul
Proof uses: Exists.intro, Set.ofPred, Usa1996P2.prefixSum, HAdd.hAdd, And.intro, Set.ext, Eq.mpr, Iff, id, congrFun', congrArg, Iff.intro, Finset.Nonempty, Finset.sum, Finset.sum_pos, Usa1996P2.prefixSum_card, Finset.sum_le_sum_of_subset, le_rfl, Nat.find, Nat.find_spec and 13 more
53 instances, coercions and auxiliary constants left out.

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