Kernel-prove the exact value M(2)=1

[DomTheDeveloper]

Result

Proves the first nontrivial minimum-overlap value M 2 = 1.

• Upper bound: the balanced partition {1,4} and {2,3} has four distinct cross-differences, so every overlap is at most one.
• Lower bound: every balanced partition of {1,2,3,4} has two nonempty parts, and any cross-pair contributes an overlap of at least one.

Green verification

Focused audit run 30212008331 passed every gate:

• source scan rejecting proof holes and trust escapes;
• exact registered Lake-module build;
• exact theorem axiom audit.

The theorem depends only on:

[propext, Classical.choice, Quot.sound]

No sorryAx or compiler-trust dependency appears.

Status

The proof theorem is green. A one-file canonical wrapper replacement is still required before promotion to _PRs/ready/.

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