feat(GreensOpenProblems): 18

[jeangud]

Description

Suppose that $G$ is a finite group, and let $A \subset G \times G$ be a subset of density $\alpha$. Is it true that there are $\gg_\alpha |G|^3$ triples $x, y, g$ such that $(x, y), (gx, y), (x, gy)$ all lie in $A$?

• Closes Green's Open Problems #18 #1553
• Couple clarifications from Green's statement:
  • Added $\exists m_0 \in \mathbb{N}, ..., |G| \ge m_0$ to focus on asymptotic behavior and avoid edge cases on tiny groups.
  • Added $g \neq e$ from Austin's paper, to avoid trivial triples. Not strictly required.
  • Still following Austin's referenced paper, density is taken as "A is $\alpha$-dense, i.e. $|A| \ge \alpha |G|^2$"
• Also added the solved case for "BMZ" corners

Testing

✅ Builds successfully.

$ lake build FormalConjectures/GreensOpenProblems/18.lean 
Build completed successfully.