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

15 declarations, 7 contain sorry, 0 declared as axioms

Green's Open Problem 32

Reference:

[Gr24] Green, Ben. "100 open problems." (2024).
[Sh20] Shakan, George. "A Large Gap in a Dilate of a Set." SIAM Journal on Discrete Mathematics 34.4 (2020): 2553-2555.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

def Green32.HasGap A set $A$ has a gap of length $L$ if there exists $x$ such that $x, x+1, \dots, x+L-1$ are all not in $A$ line 40 source
Source documentation
A set $A$ has a gap of length $L$ if there exists $x$ such that $x, x+1, \dots, x+L-1$ are all not in $A$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, ZMod
Proof uses: Exists, LT.lt, Not, Membership.mem, HAdd.hAdd
14 instances, coercions and auxiliary constants left out.
```
def HasGap {p : ℕ} (A : Finset (ZMod p)) (L : ℕ) : Prop :=
…
```
theorem Green32.hasGap_zero Any set has a gap of length 0 (vacuously true) line 45 source
Source documentation
Any set has a gap of length 0 (vacuously true).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, ZMod, Green32.HasGap, OfNat.ofNat
Proof uses: Exists.intro, LT.lt, Not, Membership.mem, HAdd.hAdd, absurd
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem hasGap_zero {p : ℕ} (A : Finset (ZMod p)) :
    HasGap A 0 := by
…
```
Mentions: Green32.HasGap
theorem Green32.hasGap_empty The empty set has a gap of any length line 51 source
Source documentation
The empty set has a gap of any length.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Green32.HasGap, EmptyCollection.emptyCollection, Finset, ZMod
Proof uses: Exists.intro, LT.lt, Not, Membership.mem, HAdd.hAdd, OfNat.ofNat, of_eq_true, Eq.trans, False, True, congrArg, zero_add, not_false_eq_true
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem hasGap_empty {p : ℕ} (L : ℕ) :
    HasGap (∅ : Finset (ZMod p)) L := by
…
```
Mentions: Green32.HasGap
theorem Green32.not_hasGap_univ The full set in $\mathbb{Z}/p\mathbb{Z}$ has no gap of positive length line 57 source
Source documentation
The full set in $\mathbb{Z}/p\mathbb{Z}$ has no gap of positive length.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, Not, Green32.HasGap, Finset.univ, ZMod, OfNat.ofNat
Proof uses: LT.lt, Membership.mem, Finset, HAdd.hAdd, False, Decidable.byContradiction, False.elim, Eq.mp, Eq.trans, True, congrArg, Nat.cast_zero, add_zero, not_true_eq_false
31 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem not_hasGap_univ {p : ℕ} [NeZero p] :
    ¬ HasGap (Finset.univ : Finset (ZMod p)) 1 := by
…
```
Mentions: Green32.HasGap
theorem Green32.hasGap_concrete Concrete: $\{0\}$ in $\mathbb{Z}/5\mathbb{Z}$ has a gap of length 4 starting at 1 line 65 source
Source documentation
Concrete: $\{0\}$ in $\mathbb{Z}/5\mathbb{Z}$ has a gap of length 4 starting at 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green32.HasGap, OfNat.ofNat, Nat, Singleton.singleton, ZMod, Finset
Proof uses: Exists.intro, LT.lt, Not, Membership.mem, HAdd.hAdd, dite, LE.le, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 2 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem hasGap_concrete :
    HasGap ({(0 : ZMod 5)} : Finset (ZMod 5)) 4 := by
…
```
Mentions: Green32.HasGap
def Green32.HasLargeGapDilate The generalized problem: for a prime line 75 source
Source documentation
The generalized problem: for a prime $p$ and a set $A \subset \mathbb{Z}/p\mathbb{Z}$ of size $\lfloor \omega(p) \rfloor$, is there a dilate of $A$ containing a gap of length $\lfloor 100p/\omega(p) \rfloor$?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Filter.Eventually, Nat.Prime, And, LT.lt, OfNat.ofNat, Finset, ZMod, Eq, Finset.card, Nat.floor, Exists, Units, Green32.HasGap, HSMul.hSMul, HDiv.hDiv, HMul.hMul, Filter.atTop
28 instances, coercions and auxiliary constants left out.
```
def HasLargeGapDilate (ω : ℕ → ℝ) : Prop :=
…
```
theorem Green32.green_32 Let $p$ be a prime and let $A \subset \mathbb{Z}/p\mathbb{Z}$ be a set of size $\lfloor \sqrt{p} \rfloor$ sorry line 86 source
Source documentation
Let $p$ be a prime and let $A \subset \mathbb{Z}/p\mathbb{Z}$ be a set of size $\lfloor \sqrt{p} \rfloor$. Is there a dilate of $A$ containing a gap of length $100\sqrt{p}$?

depends on sorry what this means
Statement uses: Iff, True, Green32.HasLargeGapDilate, Nat, Real.sqrt, Real
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_32 :
    answer(sorry) ↔ HasLargeGapDilate (fun p ↦ Real.sqrt p) := by
…
```
Mentions: Green32.HasLargeGapDilate
theorem Green32.green_32.variants.sh20_general [Sh20, Theorem 1] implies a gap of at least $\lfloor 2p/|A| - 2 \rfloor$ sorry line 92 source
Source documentation
[Sh20, Theorem 1] implies a gap of at least $\lfloor 2p/|A| - 2 \rfloor$.

depends on sorry what this means
Statement uses: Nat, Nat.Prime, Finset, ZMod, LT.lt, OfNat.ofNat, Finset.card, Exists, Units, Green32.HasGap, HSMul.hSMul, Nat.floor, Real, HSub.hSub, HDiv.hDiv, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
62 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_32.variants.sh20_general :
    ∀ (p : ℕ), p.Prime → -- Theorem 1 is for any prime p, not just asymptotically
      ∀ A : Finset (ZMod p), 1 < A.card →
      ∃ c : (ZMod p)ˣ, HasGap (c • A) ⌊2 * (p : ℝ) / A.card - 2⌋₊ := by
…
```
Mentions: c, Green32.HasGap
theorem Green32.green_32.variants.sh20_sqrt [Sh20] has used the polynomial method to show that this is true with 100 replaced by 2 [Gr24] sorry line 106 source
Source documentation
[Sh20] has used the polynomial method to show that this is true with 100 replaced by 2 [Gr24].
Note: More precisely [Sh20, Theorem 1] implies a gap of at least $\lfloor 2p/|A| - 2 \rfloor$. For a set $A$ of size $\lfloor \sqrt{p} \rfloor$, this guarantees a gap of at least $\lfloor 2\sqrt{p} \rfloor - 2$.

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, Nat.Prime, Finset, ZMod, Eq, Finset.card, Nat.floor, Real, Real.sqrt, Exists, Units, Green32.HasGap, HSMul.hSMul, HSub.hSub, HMul.hMul, OfNat.ofNat, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_32.variants.sh20_sqrt :
    ∀ᶠ p in atTop, p.Prime →
      ∀ A : Finset (ZMod p), A.card = ⌊Real.sqrt p⌋₊ →
      ∃ c : (ZMod p)ˣ, HasGap (c • A) (⌊2 * Real.sqrt p⌋₊ - 2) := by
…
```
Mentions: c, Green32.HasGap
theorem Green32.green_32.variants.szemeredi_regime In the regime $\omega(p) \sim c p$, this is Szemerédi's theorem [Gr24] sorry line 114 source
Source documentation
In the regime $\omega(p) \sim c p$, this is Szemerédi's theorem [Gr24].

depends on sorry what this means
Statement uses: Real, And, LT.lt, OfNat.ofNat, Nat, Asymptotics.IsEquivalent, Filter.atTop, HMul.hMul, Green32.HasLargeGapDilate
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_32.variants.szemeredi_regime :
    ∀ c, 0 < c ∧ c < 1 → ∀ ω : ℕ → ℝ, ω ~[atTop] (fun p ↦ c * p) →
      HasLargeGapDilate ω := by
…
```
Mentions: c, Green32.HasLargeGapDilate
theorem Green32.green_32.variants.dirichlet_regime In the regime $\omega(p) \le c \log p$, this is basically Dirichlet's lower bound for the size of Bohr sets [Gr24] sorry line 128 source
Source documentation
In the regime $\omega(p) \le c \log p$, this is basically Dirichlet's lower bound for the size of Bohr sets [Gr24].
The lower bound $101 \le \omega(p)$ makes the set size $\lfloor \omega(p) \rfloor$ exceed $100$. With only $100 < \omega(p)$, a function with $100 < \omega(p) < 101$ asks for sets of size $100$ with a gap of length $p - 1$ in some dilate, which is impossible.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Nat, Filter.Eventually, LE.le, HMul.hMul, Real.log, Filter.atTop, Green32.HasLargeGapDilate
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_32.variants.dirichlet_regime :
    ∃ c > 0, ∀ ω : ℕ → ℝ, (∀ᶠ p in atTop, 101 ≤ ω p ∧ ω p ≤ c * Real.log p) →
      HasLargeGapDilate ω := by
…
```
Mentions: c, Green32.HasLargeGapDilate
theorem Green32.green_32.variants.log_regime Even what happens in the regime $\omega(p) \sim 10 \log p$ is unclear [Gr24] sorry line 135 source
Source documentation
Even what happens in the regime $\omega(p) \sim 10 \log p$ is unclear [Gr24].

depends on sorry what this means
Statement uses: Iff, True, Nat, Real, Asymptotics.IsEquivalent, Filter.atTop, HMul.hMul, OfNat.ofNat, Real.log, Green32.HasLargeGapDilate
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_32.variants.log_regime :
    answer(sorry) ↔
    (∀ ω : ℕ → ℝ, ω ~[atTop] (fun p ↦ 10 * Real.log p) →
      HasLargeGapDilate ω) := by
…
```
Mentions: Green32.HasLargeGapDilate
def Green32.HasCosetHole A set $A$ has a coset hole of size $L$ if there exists a subspace $W$ and a vector $v$ such that the affine space $v + W$ has size at least $L$ and is disjoint from $A$ line 145 source
Source documentation
A set $A$ has a coset hole of size $L$ if there exists a subspace $W$ and a vector $v$ such that the affine space $v + W$ has size at least $L$ and is disjoint from $A$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, 𝔽₂
Proof uses: Exists, Submodule, ZMod, OfNat.ofNat, Fin, And, LE.le, Nat.card, Subtype, Membership.mem, Not, HAdd.hAdd
19 instances, coercions and auxiliary constants left out.
```
def HasCosetHole {n : ℕ} (A : Finset (𝔽₂ n)) (L : ℕ) : Prop :=
…
```
Mentions: 𝔽₂
theorem Green32.hasCosetHole_empty The empty set in $\mathbb{F}_2^n$ has a coset hole (using the trivial subspace) line 151 source
Source documentation
The empty set in $\mathbb{F}_2^n$ has a coset hole (using the trivial subspace).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Green32.HasCosetHole, EmptyCollection.emptyCollection, Finset, 𝔽₂, OfNat.ofNat
Proof uses: Exists.intro, Submodule, ZMod, Fin, Exists, And, LE.le, Nat.card, Subtype, Membership.mem, Not, HAdd.hAdd, Bot.bot, And.intro, Nat.zero_le, of_eq_true, Eq.trans, False, True, congrArg and 2 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem hasCosetHole_empty (n : ℕ) :
    HasCosetHole (∅ : Finset (𝔽₂ n)) 0 := by
…
```
Mentions: Green32.HasCosetHole, 𝔽₂
theorem Green32.green_32.variants.finite_field Tom Sanders' finite field variant [Gr24] sorry line 161 source
Source documentation
Tom Sanders' finite field variant [Gr24]. If $N = 2^n$ and $A$ is a subset of size $\lfloor \sqrt{N} \rfloor$, then $A^c$ contains a coset of size at least $100\sqrt{N}$ for sufficiently large $n$.

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, Finset, 𝔽₂, Eq, Finset.card, Nat.floor, Real, Real.sqrt, HPow.hPow, OfNat.ofNat, Green32.HasCosetHole, HMul.hMul, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_32.variants.finite_field :
    ∀ᶠ n in atTop,
      ∀ A : Finset (𝔽₂ n), A.card = ⌊Real.sqrt (2^n : ℝ)⌋₊ →
      HasCosetHole A ⌊100 * Real.sqrt (2^n : ℝ)⌋₊ := by
…
```
Mentions: 𝔽₂, Green32.HasCosetHole