Basic.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

22 declarations, 0 contain sorry, 0 declared as axioms

Maximal Sidon sets in an interval.

We follow the convention that IsMaximalSidonSetIn A N means A ⊆ {1, …, N} is Sidon and is inclusion-maximal among subsets of Set.Icc 1 N with the Sidon property.

Imports (3)

Imported by 2 files

def IsProductFree line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Mul, Set
Proof uses: Disjoint, HMul.hMul
8 instances, coercions and auxiliary constants left out.
theorem isProductFree_iff line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Mul, Set, Iff, IsProductFree, Membership.mem, Not, HMul.hMul
Proof uses: Eq.mpr, Eq, id, congrFun', congrArg, Eq.trans, Disjoint, forall_congr, And, Exists, implies_congr, Eq.refl, Iff.intro, Aesop.BuiltinRules.not_intro, of_eq_true, False, True, eq_false, not_false_eq_true
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def allUniqueSums allUniqueSums A is the set of elements in α that can be written as the sum of exactly one unordered pair of elements from A line 49 source
Source documentation
allUniqueSums A is the set of elements in α that can be written as the sum of exactly one unordered pair of elements from A.

no axioms what this means
Statement uses: AddCommMonoid, Set
Proof uses: Set.ofPred, Exists, Prod, And, Membership.mem, Prod.fst, Prod.snd, Eq, HAdd.hAdd, Or
5 instances, coercions and auxiliary constants left out.
```
def allUniqueSums (A : Set α) : Set α :=
…
```
def HasNoUniqueRepresentation Documented declaration: HasNoUniqueRepresentation line 58 source
Source documentation
A set A has no unique representation in its sumset A + A if for every pair of elements a₁, a₂ ∈ A, there exist another pair of elements b₁, b₂ ∈ A such that a₁ + a₂ = b₁ + b₂ and {a₁, a₂} ≠ {b₁, b₂}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Finset
Proof uses: Eq, Set, allUniqueSums, EmptyCollection.emptyCollection
3 instances, coercions and auxiliary constants left out.
```
def HasNoUniqueRepresentation {α : Type*} [AddCommMonoid α] (A : Finset α) : Prop :=
…
```
def IsSyndetic A set $A$ of natural numbers is said to have bounded gaps if there exists an integer $p$ such that $A ∩ [n, n + 1, ..., n + p]$ is nonempty for all $n$ line 63 source
Source documentation
A set $A$ of natural numbers is said to have bounded gaps if there exists an integer $p$ such that $A ∩ [n, n + 1, ..., n + p]$ is nonempty for all $n$.

no axioms what this means
Statement uses: Set, Nat
Proof uses: Exists, Set.Nonempty, Inter.inter, Set.Icc, HAdd.hAdd
4 instances, coercions and auxiliary constants left out.
```
def IsSyndetic (A : Set ℕ) : Prop := ∃ p, ∀ n, (A ∩ .Icc n (n + p)).Nonempty
```
def IsSidon A Sidon set is a set, such that such that all pairwise sums of elements are distinct apart from coincidences forced by the commutativity of addition line 67 source
Source documentation
A Sidon set is a set, such that such that all pairwise sums of elements are distinct apart from coincidences forced by the commutativity of addition.

no axioms what this means
Statement uses: AddCommMonoid, Set
Proof uses: Membership.mem, Eq, HAdd.hAdd, Or, And
5 instances, coercions and auxiliary constants left out.
```
def IsSidon (A : Set α) : Prop := ∀ᵉ (i₁ ∈ A) (j₁ ∈ A) (i₂ ∈ A) (j₂ ∈ A),
…
```
lemma Set.IsSidon.avoids_isAPOfLength_three line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.IsAPOfLength, OfNat.ofNat, ENat, LE.le, Set.ncard, Inter.inter
Proof uses: Eq, Set.encard, Exists, Set.ofPred, And, LT.lt, HAdd.hAdd, HMul.hMul, Eq.mp, Eq.trans, Set.IsAPOfLengthWith, congrArg, funext, HSMul.hSMul, propext, exists_prop_congr, Iff.of_eq, Eq.refl, of_eq_true, True and 97 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem Set.IsSidon.subset line 90 source
no axioms what this means
Statement uses: AddCommMonoid, Set, IsSidon, LE.le
Proof uses: Membership.mem, Eq, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.
theorem Set.IsSidon.insert line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Set, IsRightCancelAdd, IsLeftCancelAdd, IsSidon, Iff, Union.union, Singleton.singleton, Or, Membership.mem, And, Ne, HAdd.hAdd
Proof uses: dite, Classical.propDecidable, Iff.intro, Or.inl, Eq.mpr, Insert.insert, id, Eq, congrArg, Set.union_singleton, Set.insert_eq_of_mem, Not, Or.inr, And.intro, Or.elim, False, of_eq_true, Eq.trans, True, congrFun' and 24 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
def Set.IsMaximalSidonSetIn IsMaximalSidonSetIn A N means A ⊆ {1, …, N} is Sidon and cannot be extended within {1, …, N} while remaining Sidon line 133 source
Source documentation
IsMaximalSidonSetIn A N means A ⊆ {1, …, N} is Sidon and cannot be extended within {1, …, N} while remaining Sidon.

standard axioms: propext what this means
Statement uses: Set, Nat
Proof uses: And, LE.le, Set.Icc, OfNat.ofNat, IsSidon, Membership.mem, Not, Union.union, Singleton.singleton
7 instances, coercions and auxiliary constants left out.
```
def IsMaximalSidonSetIn (A : Set ℕ) (N : ℕ) : Prop :=
…
```
theorem Set.IsMaximalSidonSetIn.subset If A is a maximal Sidon set in {1, …, N}, then A ⊆ {1, …, N} line 140 source
Source documentation
If A is a maximal Sidon set in {1, …, N}, then A ⊆ {1, …, N}.

standard axioms: propext what this means
Statement uses: Set, Nat, Set.IsMaximalSidonSetIn, LE.le, Set.Icc, OfNat.ofNat
Proof uses: And.left, And, IsSidon, Membership.mem, Not, Union.union, Singleton.singleton
10 instances, coercions and auxiliary constants left out.
```
theorem subset {A : Set ℕ} {N : ℕ} (hA : IsMaximalSidonSetIn A N) :
    A ⊆ Set.Icc 1 N := hA.1
```
Mentions: Set.IsMaximalSidonSetIn
theorem Set.IsMaximalSidonSetIn.isSidon If A is a maximal Sidon set in {1, …, N}, then A is Sidon line 144 source
Source documentation
If A is a maximal Sidon set in {1, …, N}, then A is Sidon.

standard axioms: propext what this means
Statement uses: Set, Nat, Set.IsMaximalSidonSetIn, IsSidon
Proof uses: And.left, Membership.mem, Set.Icc, OfNat.ofNat, Not, Union.union, Singleton.singleton, And.right, LE.le, And
8 instances, coercions and auxiliary constants left out.
```
theorem isSidon {A : Set ℕ} {N : ℕ} (hA : IsMaximalSidonSetIn A N) : IsSidon A := hA.2.1
```
Mentions: Set.IsMaximalSidonSetIn, IsSidon
theorem Set.IsMaximalSidonSetIn.maximal Maximality condition unpacked line 147 source
Source documentation
Maximality condition unpacked.

standard axioms: propext what this means
Statement uses: Set, Nat, Set.IsMaximalSidonSetIn, Membership.mem, Set.Icc, OfNat.ofNat, Not, IsSidon, Union.union, Singleton.singleton
Proof uses: And.right, LE.le, And
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem maximal {A : Set ℕ} {N : ℕ} (hA : IsMaximalSidonSetIn A N) {x : ℕ}
    (hx : x ∈ Set.Icc 1 N) (hxA : x ∉ A) : ¬ IsSidon (A ∪ {x}) := hA.2.2 hx hxA
…
```
Mentions: Set.IsMaximalSidonSetIn, IsSidon
instance Finset.(instance at line 156) line 156 source
def Finset.maxSidonSubsetCard The maximum size of a Sidon set in the supplied Finset line 163 source
Source documentation
The maximum size of a Sidon set in the supplied Finset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Finset, DecidableEq, Nat
Proof uses: Finset.sup, Finset.filter, IsSidon, Finset.powerset, Finset.card
6 instances, coercions and auxiliary constants left out.
```
def maxSidonSubsetCard (A : Finset α) [DecidableEq α] : ℕ :=
…
```
theorem Finset.IsSidon.insert_ge_max' If A is finite Sidon, then A ∪ {s} is also Sidon provided s ≥ A.max + 1 line 167 source
Source documentation
If A is finite Sidon, then A ∪ {s} is also Sidon provided s ≥ A.max + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, IsSidon, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.max', Union.union, Set, Singleton.singleton
Proof uses: Membership.mem, LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, Exists.intro, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.neg_congr and 77 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem IsSidon.insert_ge_max' {A : Finset ℕ} (h : A.Nonempty) (hA : IsSidon (A : Set ℕ)) {s : ℕ}
    (hs : 2 * A.max' h + 1 ≤ s) :
    IsSidon (A ∪ {s}) := by
…
```
Mentions: IsSidon
theorem Finset.IsSidon.exists_insert line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, IsSidon, Exists, And, Not, Membership.mem, Union.union, Set, Singleton.singleton
Proof uses: Exists.intro, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.max', And.intro, mt, LE.le, Finset.le_max', Iff.mpr, LT.lt, not_le, Finset.max'_lt_iff, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg and 62 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Finset.IsSidon.exists_insert_ge line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, IsSidon, Exists, And, GE.ge, Not, Membership.mem, Union.union, Set, Singleton.singleton
Proof uses: Exists.intro, ite, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.max', And.intro, dite, Eq.mpr, id, Eq, congrFun', congrArg, if_pos, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg and 74 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def Finset.greedySidon.go Given a finite Sidon set A and a lower bound m, go finds the smallest number m' ≥ m such that A ∪ {m'} is Sidon line 198 source
Source documentation
Given a finite Sidon set A and a lower bound m, go finds the smallest number m' ≥ m such that A ∪ {m'} is Sidon. If A is empty then this returns the value m. Note that the lower bound is required to avoid 0 being a contender in some cases.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, IsSidon, Subtype, And, GE.ge, Not, Membership.mem, Union.union, Singleton.singleton
Proof uses: dite, Finset.Nonempty, Exists, Subtype.mk, Nat.find
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def greedySidon.go (A : Finset ℕ) (hA : IsSidon (A : Set ℕ)) (m : ℕ) :
    {m' : ℕ // m' ≥ m ∧ m' ∉ A ∧ IsSidon (↑(A ∪ {m'}) : Set ℕ)} :=
…
```
Mentions: IsSidon
def Finset.greedySidon.aux Main search loop for generating the greedy Sidon sequence line 211 source
Source documentation
Main search loop for generating the greedy Sidon sequence. The return value for step n is the finite set of numbers generated so far, a proof that it is Sidon, and the greatest element of the finite set at that point. This is initialised at {1}, then greedySidon.go is called iteratively using the lower bound max + 1 to find the next smallest Sidon preserving number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Subtype, Finset, IsSidon
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def greedySidon.aux (n : ℕ) : ({A : Finset ℕ // IsSidon (A : Set ℕ)} × ℕ) :=
…
```
Mentions: IsSidon
def Finset.greedySidon greedySidon is the sequence obtained by the initial set $\{1\}$ and iteratively obtaining the next smallest integer that preserves the Sidon property of the set line 223 source
Source documentation
greedySidon is the sequence obtained by the initial set $\{1\}$ and iteratively obtaining the next smallest integer that preserves the Sidon property of the set. This gives the sequence 1, 2, 4, 8, 13, 21, 31, ....

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Prod.snd, Subtype, Finset, IsSidon, Finset.greedySidon.aux
3 instances, coercions and auxiliary constants left out.
```
def greedySidon (n : ℕ) : ℕ := greedySidon.aux n |>.2
```
Mentions: Finset.greedySidon.aux
def Finset.greedySidonBelow The greedy Sidon set in {1, …, N}: starting from ∅, iterate through 1, …, N and include x if and only if A ∪ {x} remains Sidon line 228 source
Source documentation
The greedy Sidon set in {1, …, N}: starting from ∅, iterate through 1, …, N and include x if and only if A ∪ {x} remains Sidon. Alternatively, this is precisely the set of elements in the greedy Sidon sequence that are ≤ N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.filter, LE.le, IsSidon, Prod.fst, Subtype, Finset.greedySidon.aux
6 instances, coercions and auxiliary constants left out.
```
def greedySidonBelow (N : ℕ) : Finset ℕ :=
…
```