Extend quantum graph N=6 obstruction to all integer colors

[DomTheDeveloper]

Stacked on the exact head of google-deepmind#4511.

This adds a standalone Lean proof that EqSystemN solution existence is downward-closed in the number of colors. Therefore the N = 6, D = 3 integer obstruction from google-deepmind#4511 immediately implies:

• no integer solution for D = 5;
• no integer solution for every D ≥ 3;
• the corresponding {-1,0,1}-restricted statements.

Canonical DTD proof package:

• Add complete quantum graph N=6 proof and color restriction #96 — clean one-commit PR directly against DTD main, containing the complete 47-certificate proof, color-restriction theorem, four terminal consequences, and focused audit workflow.

Upstream delivery:

• cross-fork stack into the Solve the N=6, D=3 integer quantum graph cases google-deepmind/formal-conjectures#4511 author's branch: Extend N=6 integer quantum obstruction to all D ≥ 3 infinityscroll/formal-conjectures#1
• target GDM PR: Solve the N=6, D=3 integer quantum graph cases google-deepmind/formal-conjectures#4511

This remains draft until DTD #96's focused Lean audit is green.

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