feat(Papers): Add Monochromatic Quantum Graph conjectures

[MarioKrenn6240]

Summary

This PR adds a formalization of the monochromatic quantum graph / perfect-matching equation system problem (see #2205) in the formal-conjectures style. The problem is motivated by quantum-optics constructions of high-dimensional multipartite GHZ-type states via linear optics, where interference amplitudes can be expressed as weighted sums over perfect matchings.

The setup uses a complete graph K_N whose edges carry both (i) endpoint “color indices” in Fin D and (ii) a coefficient/weight. For each vertex assignment ι : V N → Fin D, we define a perfect-matching sum pmSumN N D W ι (sum over perfect matchings, each contributing the product of its induced edge weights). The equation system EqSystemN N D W enforces:

• pmSumN ... ι = 1 iff ι is constant (monochromatic inherited vertex coloring),
• pmSumN ... ι = 0 otherwise.

This yields exponentially many constraints in N on only O(N^2) edge variables, matching the combinatorial formulation in the MathOverflow reference above.

---

What this PR contains

• Core definitions:

  • edge/weight model (EdgeN, WeightsN)
  • perfect-matching sum (pmSumN)
  • the equation system (EqSystemN)

• Verified “sanity check” solutions (explicit witnesses):

  • N = 4, D = 2
  • N = 4, D = 3
  • N = 6, D = 2

• Open conjectures stating non-existence over several coefficient domains:

  • ℂ, ℝ, ℤ, and integer weights restricted to { -1, 0, 1 }

• Recorded non-existence results over ℝ≥0 attributed to Bogdanov’s lemma (as research solved, proof omitted)

All general statements are restricted to even N, since odd N admits no perfect matchings.

---

Selected references:

• PRL (2017): https://journals.aps.org/prl/abstract/10.1103/PhysRevLett.119.240403
• PNAS (2019): https://www.pnas.org/doi/10.1073/pnas.1816096116
• Graph-theoretic works: https://arxiv.org/abs/1902.06023, https://arxiv.org/abs/2202.05562, https://arxiv.org/abs/2407.00303
• MathOverflow background (inherited colorings): https://mathoverflow.net/questions/311325
• MathOverflow equation-system formulation: https://mathoverflow.net/questions/341983/combinatorial-equation-system-with-exponentially-many-equations-in-quadratic-man?noredirect=1&lq=1

---

Tags

Open problems are tagged @[category research open, AMS 05 14 81] and the recorded Bogdanov statements are tagged @[category research solved, AMS 05 14 81].

Closes #2205. Assisted by GPT 5.2 Pro.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[MarioKrenn6240]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

I believe this is fixed by now, let me know if i need to do something in addition here.

[Paul-Lez]

Thanks for the contribution, this looks pretty cool! A few initial comments:)

[MarioKrenn6240]

Thanks for the contribution, this looks pretty cool! A few initial comments:)

Thank you! Please note i only started with Lean a few days ago, and use GPT 5.2 Pro. I can read the code and verify that -- as far as i understand it -- it makes sense. The test solutions further strengthen my conviction that its right, but i certianly cannot verify it in full generality. Thus it would be helpful to check carefully whether the defitions (especially of the PMs and its sum) are really solid. Thank you!

[franzhusch]

@MarioKrenn6240 A PR is a normally limited to one problem at a time (to reduce reviewing scope), unless the problems are closely related and use the same definitions. You can open 2 new PRs for the 13 and 35 problem and also link the corresponding issue in the new PR then :)

[Paul-Lez]

@MarioKrenn6240 I think the initial content of this PR (minus the extra files you added) is good to go - happy to merge once you move the extra files to other PRs:)

[MarioKrenn6240]

@MarioKrenn6240 I think the initial content of this PR (minus the extra files you added) is good to go - happy to merge once you move the extra files to other PRs:)

Oh i am sorry, these files got accidentally added to this PR too while i made the other two PRs. Sorry, just fixed it. Great the file is now ready to merge. Thank you!

[Paul-Lez]

LGTM. Could you add the changes (a few style nits) I pushed to https://github.com/google-deepmind/formal-conjectures/tree/MarioKrenn6240/main ?

[MarioKrenn6240]

LGTM. Could you add the changes (a few style nits) I pushed to https://github.com/google-deepmind/formal-conjectures/tree/MarioKrenn6240/main ?

Perfect, i integrated them. Thanks for going through everything again!

[Paul-Lez]

Should merge automatically once CI has finished running:)