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

12 declarations, 5 contain sorry, 0 declared as axioms

Ben Green's Open Problem 21

References:

[Gr24] Green, Ben. "100 open problems." (2024).
[Ra33] Rado, Richard, Studien zur Kombinatorik. Math. Zeit. 36 (1933), 424-480.
[FoKl06] Fox, Jacob and Kleitman, Daniel, On Rado's boundedness conjecture. J. Combin. Theory Ser. A 113 (2006), no. 1, 84-100.
[ElJo23] Ellis, David and Johnson, Robert (editors), A collection of open problems in celebration of Imre Leader's 60th birthday. arXiv preprint arXiv:2310.18163 (2023).

Imports (1)

FormalConjecturesUtil

def Green21.RadoCondition The coefficients $a_1, \dots, a_k$ satisfy Rado's condition if $\sum_{i \in I} a_i = 0$ for some non-empty $I \subseteq [k]$ line 47 source
Source documentation
The coefficients $a_1, \dots, a_k$ satisfy Rado's condition if $\sum_{i \in I} a_i = 0$ for some non-empty $I \subseteq [k]$.
For a single homogeneous equation with $k > 0$ nonzero coefficients this is exactly the criterion of Rado's theorem [Ra33]: $a_1x_1 + \cdots + a_kx_k = 0$ is partition regular if and only if the coefficients satisfy it. (With a zero coefficient the condition holds trivially, but e.g. $0 \cdot x_1 + x_2 = 0$ has no solution in positive integers.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int
Proof uses: Exists, Finset, And, Finset.Nonempty, Eq, Finset.sum, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def RadoCondition {k : ℕ} (a : Fin k → ℤ) : Prop :=
…
```
def Green21.minColours $c(a_1, \dots, a_k)$, the least number of colours required in order to colour $\mathbb{N}$ so that there is no monochromatic solution to $a_1x_1 + \cdots + a_kx_k = 0$ line 62 source
Source documentation
$c(a_1, \dots, a_k)$, the least number of colours required in order to colour $\mathbb{N}$ so that there is no monochromatic solution to $a_1x_1 + \cdots + a_kx_k = 0$.
The solutions $x_i$ are required to be positive, as in [FoKl06]: were $0$ admitted then $x_1 = \cdots = x_k = 0$ would be a monochromatic solution for every colouring, and no number of colours would ever suffice. The $x_i$ are not required to be distinct.
When the coefficients do not satisfy RadoCondition, Rado's theorem [Ra33] guarantees that some finite colouring has no monochromatic solution, so the set below is non-empty and this sInf is a genuine minimum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int
Proof uses: InfSet.sInf, Set.ofPred, Exists, LT.lt, OfNat.ofNat, Eq, Ne, Finset.sum, Finset.univ, HMul.hMul
10 instances, coercions and auxiliary constants left out.
```
noncomputable def minColours {k : ℕ} (a : Fin k → ℤ) : ℕ :=
…
```
theorem Green21.green_21 Suppose that $a_1, \dots, a_k$ are integers which do not satisfy Rado's condition: thus if $\sum_{i \in I} a_i = 0$ then $I = \emptyset$ sorry line 78 source
Source documentation
Suppose that $a_1, \dots, a_k$ are integers which do not satisfy Rado's condition: thus if $\sum_{i \in I} a_i = 0$ then $I = \emptyset$. It then follows from Rado's theorem that the equation $a_1x_1 + \cdots + a_kx_k = 0$ is not partition regular. Write $c(a_1, \dots, a_k)$ for the least number of colours required in order to colour $\mathbb{N}$ so that there is no monochromatic solution to $a_1x_1 + \cdots + a_kx_k = 0$. Is $c(a_1, \dots, a_k)$ bounded in terms of $k$ only?
This problem, which is known as Rado's boundedness conjecture, dates back to 1933 [Ra33]. It is open for all $k \geq 4$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Fin, Int, Not, Green21.RadoCondition, LE.le, Green21.minColours
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_21 : answer(sorry) ↔ ∃ B : ℕ → ℕ, ∀ (k : ℕ) (a : Fin k → ℤ),
    ¬ RadoCondition a → minColours a ≤ B k := by
…
```
Mentions: Green21.RadoCondition, Green21.minColours
theorem Green21.green_21.variants.fox_kleitman The answer was shown to be affirmative for $k = 3$ by Fox and Kleitman [FoKl06], who showed that $c(a_1, a_2, a_3) \leq 24$ sorry line 87 source
Source documentation
The answer was shown to be affirmative for $k = 3$ by Fox and Kleitman [FoKl06], who showed that $c(a_1, a_2, a_3) \leq 24$.

depends on sorry what this means
Statement uses: Fin, OfNat.ofNat, Nat, Int, Not, Green21.RadoCondition, LE.le, Green21.minColours
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_21.variants.fox_kleitman (a : Fin 3 → ℤ) (ha : ¬ RadoCondition a) :
    minColours a ≤ 24 := by
…
```
Mentions: Green21.RadoCondition, Green21.minColours
theorem Green21.green_21.variants.fox_kleitman_sharp Green [Gr24] is not sure that the constant $24$ of [FoKl06] is sharp, and remarks that it might be interesting to determine the sharp constant sorry line 99 source
Source documentation
Green [Gr24] is not sure that the constant $24$ of [FoKl06] is sharp, and remarks that it might be interesting to determine the sharp constant.
The largest value of $c(a_1, a_2, a_3)$ is attained, since by green_21.variants.fox_kleitman the values form a non-empty set of naturals bounded above by $24$.

depends on sorry what this means
Statement uses: IsGreatest, Nat, Set.ofPred, Exists, Fin, OfNat.ofNat, Int, And, Not, Green21.RadoCondition, Eq, Green21.minColours, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_21.variants.fox_kleitman_sharp :
    IsGreatest {c | ∃ a : Fin 3 → ℤ, ¬ RadoCondition a ∧ minColours a = c} answer(sorry) := by
…
```
Mentions: c, Green21.RadoCondition, Green21.minColours
theorem Green21.green_21.variants.fox_kleitman_modular A question [FoKl06, Conjecture 5] of Fox and Kleitman, which they call a 'modular analogue' of Rado's Boundedness Conjecture sorry line 118 source
Source documentation
A question [FoKl06, Conjecture 5] of Fox and Kleitman, which they call a 'modular analogue' of Rado's Boundedness Conjecture. Let $k > 0$, let $p$ be a prime, and suppose that $a_1, \dots, a_k$ are integers with $\sum_{i \in I} a_i \equiv 0 \pmod p$ only when $I = \emptyset$. Does there exist an $f(k)$-colouring of $(\mathbb{Z}/p\mathbb{Z})^*$ with no monochromatic solution to $a_1x_1 + \cdots + a_kx_k = 0$? This seems to be open even when $k = 3$; Green [Gr24] suspects the answer may be negative.
The point of the question is that the number of colours $f(k)$ must not depend on $p$.
The arity $k$ is required to be positive, as in [FoKl06]: for $k = 0$ the empty tuple is a monochromatic solution with sum $0$ for every colouring, so no $f(0)$ could work.

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, LT.lt, OfNat.ofNat, Nat.Prime, Fin, Int, Finset, Dvd.dvd, Finset.sum, Eq, EmptyCollection.emptyCollection, Units, ZMod, Ne, Finset.univ, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_21.variants.fox_kleitman_modular : answer(sorry) ↔ ∃ f : ℕ → ℕ,
    ∀ (k p : ℕ), 0 < k → p.Prime → ∀ a : Fin k → ℤ,
      (∀ I : Finset (Fin k), (p : ℤ) ∣ ∑ i ∈ I, a i → I = ∅) →
      ∃ col : (ZMod p)ˣ → Fin (f k), ∀ x : Fin k → (ZMod p)ˣ,
        (∀ i j, col (x i) = col (x j)) → ∑ i, (a i : ZMod p) * (x i : ZMod p) ≠ 0 := by
…
```
def Green21.maxDepth The largest $d \leq r$ such that $\sum_{i \in I} a_i \equiv 0 \pmod{2^d}$ for some non-empty subset $I \subseteq [k]$, where $a_1, \dots, a_k \in \mathbb{Z}/2^r\mathbb{Z}$ line 132 source
Source documentation
The largest $d \leq r$ such that $\sum_{i \in I} a_i \equiv 0 \pmod{2^d}$ for some non-empty subset $I \subseteq [k]$, where $a_1, \dots, a_k \in \mathbb{Z}/2^r\mathbb{Z}$.
Congruence mod $2^d$ of an element of $\mathbb{Z}/2^r\mathbb{Z}$ is expressed through its canonical representative ZMod.val; this is unambiguous because $d$ is capped at $r$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, ZMod, HPow.hPow, OfNat.ofNat
Proof uses: SupSet.sSup, Set.ofPred, And, LE.le, Exists, Finset, Finset.Nonempty, Dvd.dvd, ZMod.val, Finset.sum
17 instances, coercions and auxiliary constants left out.
```
noncomputable def maxDepth {k r : ℕ} (a : Fin k → ZMod (2 ^ r)) : ℕ :=
…
```
theorem Green21.green_21.variants.milicevic Milićević [ElJo23, Conjecture 11.1] conjectures the following 2-adic variant sorry line 148 source
Source documentation
Milićević [ElJo23, Conjecture 11.1] conjectures the following 2-adic variant. For any $k \in \mathbb{N}$, there exists $K = K(k)$ such that the following is true. Let $r$ be a positive integer, and let $a_1, \dots, a_k \in \mathbb{Z}/2^r\mathbb{Z}$. Let $d$ be the largest integer such that $\sum_{i \in I} a_i \equiv 0 \pmod{2^d}$ for some non-empty subset $I \subset [k]$. Then there is a $K$-colouring of $\mathbb{Z}/2^r\mathbb{Z}$ such that all monochromatic solutions $x = (x_1, \dots, x_k)$ to the equation $a_1x_1 + \cdots + a_kx_k = 0$ satisfy $x_i \equiv 0 \pmod{2^{r-d}}$ for all $i = 1, \dots, k$.
Milićević remarks that, if true, this would imply the Rado boundedness conjecture by a compactness argument.

depends on sorry what this means
Statement uses: Nat, Exists, LT.lt, OfNat.ofNat, Fin, ZMod, HPow.hPow, Eq, Finset.sum, Finset.univ, HMul.hMul, Dvd.dvd, HSub.hSub, Green21.maxDepth, ZMod.val
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_21.variants.milicevic : ∀ k : ℕ, ∃ K : ℕ, ∀ r : ℕ, 0 < r →
    ∀ a : Fin k → ZMod (2 ^ r), ∃ col : ZMod (2 ^ r) → Fin K,
      ∀ x : Fin k → ZMod (2 ^ r), (∀ i j, col (x i) = col (x j)) →
        ∑ i, a i * x i = 0 → ∀ i, 2 ^ (r - maxDepth a) ∣ (x i).val := by
…
```
Mentions: Green21.maxDepth
theorem Green21.not_radoCondition_iff Not satisfying RadoCondition is Green's phrasing "if $\sum_{i \in I} a_i = 0$ then $I = \emptyset$" line 159 source
Source documentation
Not satisfying RadoCondition is Green's phrasing "if $\sum_{i \in I} a_i = 0$ then $I = \emptyset$".

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Iff, Not, Green21.RadoCondition, Finset, Eq, Finset.sum, OfNat.ofNat, EmptyCollection.emptyCollection
Proof uses: Eq.mpr, Ne, id, congrFun', congrArg, Eq.trans, And, Exists, Finset.Nonempty, funext, forall_congr, Iff.intro, by_contra
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem not_radoCondition_iff {k : ℕ} (a : Fin k → ℤ) :
    ¬ RadoCondition a ↔ ∀ I : Finset (Fin k), ∑ i ∈ I, a i = 0 → I = ∅ := by
…
```
Mentions: Green21.RadoCondition
theorem Green21.ne_zero_of_not_radoCondition A tuple failing RadoCondition has no zero coefficient, since a singleton is a non-empty subset line 168 source
Source documentation
A tuple failing RadoCondition has no zero coefficient, since a singleton is a non-empty subset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Not, Green21.RadoCondition, Ne, OfNat.ofNat
Proof uses: Eq, Exists.intro, Finset, And, Finset.Nonempty, Finset.sum, Singleton.singleton, And.intro, Finset.singleton_nonempty, Eq.mpr, id, congrFun', congrArg, Finset.sum_singleton
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ne_zero_of_not_radoCondition {k : ℕ} {a : Fin k → ℤ} (ha : ¬ RadoCondition a) (i : Fin k) :
    a i ≠ 0 := fun h => ha ⟨{i}, Finset.singleton_nonempty i, by simpa using h⟩
…
```
Mentions: Green21.RadoCondition
theorem Green21.minColours_eq_zero In the degenerate case $k = 0$ the equation reads $0 = 0$, so the empty tuple is a monochromatic solution for every colouring and minColours takes its junk value 0 line 178 source
Source documentation
In the degenerate case $k = 0$ the equation reads $0 = 0$, so the empty tuple is a monochromatic solution for every colouring and minColours takes its junk value 0. The bound asserted by green_21 is therefore vacuously satisfied at $k = 0$, and the content of the problem is unaffected.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Int, Eq, Green21.minColours
Proof uses: Set, Set.ofPred, Exists, LT.lt, Ne, Finset.sum, Finset.univ, HMul.hMul, EmptyCollection.emptyCollection, Set.ext, Eq.mpr, Iff, Membership.mem, Not, id, Eq.trans, False, congrArg, iff_false, Fin.elim0 and 11 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem minColours_eq_zero (a : Fin 0 → ℤ) : minColours a = 0 := by
…
```
Mentions: Green21.minColours
theorem Green21.minColours_ones A case where the infimum defining minColours is a genuine minimum rather than the junk value of sInf ∅ line 193 source
Source documentation
A case where the infimum defining minColours is a genuine minimum rather than the junk value of sInf ∅. The coefficients $(1, 1, 1)$ fail RadoCondition, and since the $x_i$ are positive the equation $x_1 + x_2 + x_3 = 0$ has no solutions at all, so a single colour suffices; no colouring of $\mathbb{N}$ into Fin 0 exists, so $0$ is not attainable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Green21.minColours, Nat.succ, OfNat.ofNat, Matrix.vecCons, Int, Matrix.vecEmpty
Proof uses: Membership.mem, Set, Set.ofPred, Exists, Fin, LT.lt, Ne, Finset.sum, Finset.univ, HMul.hMul, Exists.intro, Eq.mpr, HAdd.hAdd, id, congrFun', congrArg, Eq.trans, Fin.sum_univ_three, congr, one_mul and 20 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem minColours_ones : minColours ![(1 : ℤ), 1, 1] = 1 := by
…
```
Mentions: Green21.minColours