feat(GreensOpenProblems): 52

[jeangud]

Description

Suppose that $A \subset \mathbb{F}_2^n$ is a set with an additive complement of size $K$ (that is, for which there is another set $S \subset \mathbb{F}_2^n$, $|S| = K$, with $A + S = \mathbb{F}_2^n$). Does $2A$ contain a coset of codimension $O_K(1)$? Could it even contain a coset of codimension $O(\log K)$? [Gr24]

• Closes Green's Open Problems #52 #1657
• Update: I had initially implemented this with the maxCosetDim helper from Green 51 but it complicated everything
  • This present implementation is simpler, and focuses on existential statements, without unnecessary maximality considerations.
  • The byproducts of the first attempt might still be useful and were filed under refactor(GreensOpenProblems): add tests for Green 51 #4309 if needed
• 🤖 Initial draft obtained with Gemini 3.1 Pro and refined manually for style and correctness.
• Variants left as a later exercise to keep this PR short

Testing

✅ Files build successfully

$ lake build FormalConjectures/GreensOpenProblems/52.lean
Build completed successfully (8035 jobs).

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[jeangud]

Actually converting back to draft, I want to see if we can make do without the maxCosetDim from Green 51.

[jeangud]

Simplified the implementation, now ready for review. Sorry about the double-post 😬

[mo271]

Thanks, LGTM modulo one minor comment, that could also be addressed in a follow up