feat(GreensOpenProblems): 30

[jeangud]

Description

Given a set $A \subset \mathbb{Z}$ with $D(A) \leq K$, find a large structured subset $A' \subset A$ which 'obviously' has $D(A') \leq K + \varepsilon$, with $D(A) := |A - A|/|A|$.

• Partially addresses Green's Open Problems #30 #1565
• The conjecture is open-ended on multiple fronts:
  • Multiple interpretations of "large structured subset" and "obviously" are possible, as highlighted in feat(GreensOpenProblems): 30 #1612
  • The expected answer to the conjecture needs to be such example subsets, is finding one enough? Do we want construction rules or a full class of compatible subsets?
  • The full conjecture is left as a TODO
• As a starting point, I propose formalizing the helping example provided by Green in his comments:

If $|A - A| \leq (4 - \varepsilon)|A|$, then there is a progression $P$ of length $\gg_\varepsilon |A|$ on which $A$ has density $> 1/2$. Then $A' := A \cap P$ "obviously" has $D(A') \leq 4$

• First quick draft obtained with the help of Gemini 3.1 Pro, and then heavily rearranged for style and modularity

Testing

✅ Builds successfully.

$ lake build FormalConjectures/GreensOpenProblems/30.lean 
Build completed successfully (7975 jobs).