feat(combinatorics/additive/ruzsa_szemeredi): The Ruzsa-Szemerédi problem

[YaelDillies]

Prove the (implicit) lower bound on the Ruzsa-Szemerédi problem.

---

We can prove the explicit bound once #15327 is merged.

Bhavik told me to golf the proof using https://github.com/leanprover-community/mathlib/blob/1874b7ab2089c2c9922e89026527b9806f2d0953/src/combinatorics/szemeredi/triangle.lean#L349-L365 but I could not make it work.

[ericrbg]

should this prove the explicit bound now?

[YaelDillies]

Yes, but I'm not sure how to state it. The problem is that the explicit bound would need to quantify over all graphs over a certain size, hence over types. Further, the construction in this PR only gives graphs with a number of vertices divisible by 6, so we would get an explicit only on a sixth of the values (ven if that's mathematically irrelevant).

Thoughts?

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#19202~~
• ~~leanprover-community/mathlib#19203~~ By Dependent Issues (🤖). Happy coding!

[YaelDillies]

Ported to LeanCamCombi