feat(Paper): three-sunflower-free set systems

[SproutSeeds]

Summary

• add a paper-backed Formal Conjectures entry for the published v2 preprint "Three-sunflower-free set systems with bounded pairwise intersections"
• define M3/I3-style bounded-intersection three-sunflower extremal quantities and the restricted-threshold interface
• record the v2 solved statements, the Mantel-tight structural reduction, and the open t >= 3 / t = 2 constant questions, with Lean v2 formal-proof links where available

Verification

• lake --wfail build FormalConjectures.Paper.ThreeSunflowerFreeSetSystems
• lake --wfail build

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

[mo271]

please mark as "Ready for review" when it is ready for review

[SproutSeeds]

-awaiting-author

[mo271]

Thanks! a few remarks:

• Most of the docstrings in this file use backticks instead of standard LaTeX $ ... $.let's use Latex!
• might it be possible to also link a few related references?

Generally this looks good mathematically, would potentially be good to relate it to other published questions/theorems

[mo271]

Suggested change

import FormalConjecturesForMathlib.Combinatorics.SetFamily.Sunflower

Instead of importing it here do it in FormalConjecturesForMathlib.lean

[mo271]

Let's not duplicte definitions that are in mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/IsPrimePow.html#IsPrimePow