feat(ErdosProblems/36): prove M_three (M 3 = 2)

[Sanexxxx777]

Summary

Proves M_three : M 3 = 2 for the Erdős minimum-overlap problem (Erdős 36) at n = 3. This is the first test value with M(n) > 1 — M_one (#4151) and M_two (#4153) are both 1, where the lower bound is trivial; at n = 3 the lower bound requires actually ruling out MaxOverlap ≤ 1.

Proof

• Upper bound (M 3 ≤ 2): the balanced partition A = {1, 4, 5}, B = {2, 3, 6} of {1, …, 6} has MaxOverlap = 2 (maxOverlap_145_236). The ≤ 2 direction bounds Overlap at every k by splitting on whether k lies in the finite range of realizable differences [-5, 3] (fin_cases … <;> decide) or outside it (Overlap = 0).
• Lower bound (M 3 ≥ 2): every balanced partition has MaxOverlap ≥ 2. Since A ∪ B = Icc 1 6, Disjoint A B, |A| = |B| force A ∈ (Icc 1 6).powersetCard 3 and B = Icc 1 6 \ A, I enumerate all C(6,3) partitions with fin_cases and discharge each by exhibiting a difference achieved twice (two_le_maxOverlap_of_exists (by decide)).

Adds three small API lemmas: overlap_le_card_mul, two_le_maxOverlap_of_overlap, two_le_maxOverlap_of_exists. (overlap_le_card_mul mirrors the one used behind the M_two formal_proof link, which is not present on main.)

The same machinery generalizes to M_four = 2 and M_five = 3 (with powersetCard 4 / powersetCard 5 enumerations); I kept this PR to M_three alone to match the incremental cadence of #4151 / #4153 and avoid a heavy decide over the larger partition sets. Happy to follow up with M_four/M_five if you'd like them.

Verification

• lake --wfail build FormalConjectures.ErdosProblems.«36» succeeds (no linter warnings).
• #print axioms Erdos36.M_three → [propext, Classical.choice, Quot.sound].

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