AdditivelyComplete.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 10 curated AI-written annotations and 7190 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 project documentation, Formal Conjectures paper, arXiv v1

14 declarations, 0 contain sorry, 0 declared as axioms

Sequences whose partial sums are dominated by the next term

If A : ℕ → ℕ is strictly increasing from index n₀ on and A 0 + ⋯ + A (m - 1) ≤ A (m + 1) for m ≥ n₀, then removing infinitely many terms from A destroys completeness. This is the argument of Graham [Gr64d] for the sequence n ↦ fib n - (-1) ^ n: once three terms A m₁ < A m₂ < A m are removed, the remaining terms below A (m + 1) sum to at most A (m + 1) - 2, so A (m + 1) - 1 is not a sum of distinct remaining terms.

Imports (7)

Imported by 2 files

def subsetSums The set of subset sums of a set A ⊆ M line 33 source
Source documentation
The set of subset sums of a set A ⊆ M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set
Proof uses: Set.ofPred, Exists, Finset, And, LE.le, Eq, Finset.sum
3 instances, coercions and auxiliary constants left out.
```
def subsetSums (A : Set M) : Set M :=
…
```
theorem subsetSums_mono If A ⊆ B, then subsetSums A ⊆ subsetSums B line 38 source
Source documentation
If A ⊆ B, then subsetSums A ⊆ subsetSums B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, LE.le, subsetSums
Proof uses: Membership.mem, Finset, And, Eq, Finset.sum, Exists.intro, And.intro, LE.le.trans, And.left, And.right
12 instances, coercions and auxiliary constants left out.
```
theorem subsetSums_mono {A B : Set M} (h : A ⊆ B) : subsetSums A ⊆ subsetSums B :=
…
```
Mentions: subsetSums
def subseqSums' The set of subset sums of a sequence ℕ → M, where repetition is allowed line 42 source
Source documentation
The set of subset sums of a sequence ℕ → M, where repetition is allowed.

standard axioms: Quot.sound, propext what this means
Statement uses: AddCommMonoid, Nat, Set
Proof uses: Set.ofPred, Exists, Finset, Eq, Finset.sum
```
def subseqSums' (A : ℕ → M) : Set M :=
…
```
def IsAddComplete A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A line 48 source
Source documentation
A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Set
Proof uses: Filter.Eventually, Membership.mem, subsetSums, Filter.atTop
1 instances, coercions and auxiliary constants left out.
```
def IsAddComplete (A : Set M) : Prop :=
…
```
theorem IsAddComplete.mono If A ⊆ B and A is complete, then B is also complete line 53 source
Source documentation
If A ⊆ B and A is complete, then B is also complete.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Set, LE.le, IsAddComplete
Proof uses: Filter.mp_mem, Filter.atTop, Set.ofPred, Membership.mem, subsetSums, Filter.univ_mem', id, subsetSums_mono
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem IsAddComplete.mono {A B : Set M} (h : A ⊆ B) (ha : IsAddComplete A) : IsAddComplete B := by
…
```
Mentions: IsAddComplete
def IsAddStronglyComplete A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A line 58 source
Source documentation
A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Set
Proof uses: Set.Finite, IsAddComplete, SDiff.sdiff
1 instances, coercions and auxiliary constants left out.
```
def IsAddStronglyComplete (A : Set M) : Prop :=
…
```
theorem IsAddStronglyComplete.isAddComplete A strongly complete set is complete line 62 source
Source documentation
A strongly complete set is complete.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Set, IsAddStronglyComplete, IsAddComplete
Proof uses: Eq.mp, SDiff.sdiff, EmptyCollection.emptyCollection, congrArg, Set.sdiff_empty, Set.finite_empty
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem IsAddStronglyComplete.isAddComplete {A : Set M} (hA : IsAddStronglyComplete A) :
    IsAddComplete A := by simpa using hA Set.finite_empty
```
Mentions: IsAddStronglyComplete, IsAddComplete
theorem IsAddStronglyComplete.mono If A ⊆ B and A is strongly complete, then B is also strongly complete line 66 source
Source documentation
If A ⊆ B and A is strongly complete, then B is also strongly complete.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Set, LE.le, IsAddStronglyComplete
Proof uses: Set.Finite, IsAddComplete.mono, SDiff.sdiff
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem IsAddStronglyComplete.mono {A B : Set M} (h : A ⊆ B) (ha : IsAddStronglyComplete A) :
    IsAddStronglyComplete B := fun C hC => (ha hC).mono (by grind)
```
Mentions: IsAddStronglyComplete
def IsAddStronglyCompleteNatSeq A sequence A is strongly complete if fun m => A (n + m) is still complete for all n line 70 source
Source documentation
A sequence A is strongly complete if fun m => A (n + m) is still complete for all n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Nat
Proof uses: IsAddComplete, Set.range, HAdd.hAdd
2 instances, coercions and auxiliary constants left out.
```
def IsAddStronglyCompleteNatSeq (A : ℕ → M) : Prop :=
…
```
theorem IsAddStronglyCompleteNatSeq.isAddComplete A strongly complete sequence is complete line 74 source
Source documentation
A strongly complete sequence is complete.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Nat, IsAddStronglyCompleteNatSeq, IsAddComplete, Set.range
Proof uses: Eq.mp, HAdd.hAdd, OfNat.ofNat, congrArg, Set, funext, zero_add
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem IsAddStronglyCompleteNatSeq.isAddComplete {A : ℕ → M}
    (hA : IsAddStronglyCompleteNatSeq A) :
    IsAddComplete (Set.range A) := by simpa using hA 0
…
```
Mentions: IsAddStronglyCompleteNatSeq, IsAddComplete
theorem IsAddStronglyCompleteNatSeq.of_isAddStronglyComplete If the range of a sequence A is strongly complete, then A is strongly complete line 80 source
Source documentation
If the range of a sequence A is strongly complete, then A is strongly complete.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Nat, IsAddStronglyComplete, Set.range, IsAddStronglyCompleteNatSeq
Proof uses: IsAddComplete.mono, SDiff.sdiff, Set, Finset, Finset.image, Classical.propDecidable, Eq, Finset.range, HAdd.hAdd, Membership.mem, Not, Exists.intro, HSub.hSub, Finset.finite_toSet
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem IsAddStronglyCompleteNatSeq.of_isAddStronglyComplete {A : ℕ → M}
    (h : IsAddStronglyComplete (.range A)) : IsAddStronglyCompleteNatSeq A :=
…
```
Mentions: IsAddStronglyComplete, IsAddStronglyCompleteNatSeq
theorem IsAddStronglyCompleteNatSeq.isAddStronglyComplete If A is strongly complete and the preimage of each element is finite, then the range of A is strongly complete line 87 source
Source documentation
If A is strongly complete and the preimage of each element is finite, then the range of A is strongly complete.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Nat, IsAddStronglyCompleteNatSeq, Set.Finite, Set.preimage, Singleton.singleton, Set, IsAddStronglyComplete, Set.range
Proof uses: LE.le, Finset, Set.Finite.toFinset, Set.Finite.preimage', Membership.mem, Finset.range, Exists, IsAddComplete, SDiff.sdiff, Finset.exists_nat_subset_range, IsAddComplete.mono, HAdd.hAdd, OfNat.ofNat, Eq, And.intro, Not, Exists.intro, Set.Iio, Eq.mp, congrArg and 3 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem IsAddStronglyCompleteNatSeq.isAddStronglyComplete {A : ℕ → M}
    (h : IsAddStronglyCompleteNatSeq A) (hA : ∀ m, (A ⁻¹' {m}).Finite) :
    IsAddStronglyComplete (.range A) := by
…
```
Mentions: IsAddStronglyCompleteNatSeq, IsAddStronglyComplete
def IsAddCompleteNatSeq' A sequence A is complete if every sufficiently large element of M is a sum of (not necessarily distinct) terms of A line 100 source
Source documentation
A sequence A is complete if every sufficiently large element of M is a sum of (not necessarily distinct) terms of A.

standard axioms: Quot.sound, propext what this means
Statement uses: AddCommMonoid, Preorder, Nat
Proof uses: Filter.Eventually, Membership.mem, Set, subseqSums', Filter.atTop
1 instances, coercions and auxiliary constants left out.
```
def IsAddCompleteNatSeq' (A : ℕ → M) : Prop :=
…
```
theorem not_isAddComplete_range_diff_of_sum_range_le Let A : ℕ → ℕ be strictly increasing from index n₀ on, with A 0 + ⋯ + A (m - 1) ≤ A (m + 1) for all m ≥ n₀ line 114 source
Source documentation
Let A : ℕ → ℕ be strictly increasing from index n₀ on, with A 0 + ⋯ + A (m - 1) ≤ A (m + 1) for all m ≥ n₀. Then Set.range A \ B is not complete for any infinite B ⊆ Set.range A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, StrictMono, HAdd.hAdd, LE.le, Finset.sum, Finset.range, OfNat.ofNat, Set, Set.range, Set.Infinite, Not, IsAddComplete, SDiff.sdiff
Proof uses: Set.preimage, Set.Finite, Set.Finite.subset, Set.image, Set.Finite.image, Membership.mem, Eq, Exists.intro, And, And.intro, rfl, HSub.hSub, id, StrictMono.id_le, Eq.mp, congrArg, Decidable.byContradiction, Iff, LT.lt, Exists and 36 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
```
theorem not_isAddComplete_range_diff_of_sum_range_le {A : ℕ → ℕ} {n₀ : ℕ}
    (hA : StrictMono fun k => A (n₀ + k))
    (hsum : ∀ m, n₀ ≤ m → ∑ i ∈ Finset.range m, A i ≤ A (m + 1))
    {B : Set ℕ} (hB : B ⊆ Set.range A) (hB' : B.Infinite) :
    ¬ IsAddComplete (Set.range A \ B) := by
…
```
Mentions: IsAddComplete