feat: add quantum low individual degree soundness problem

[LionSR]

Summary

• add the self-contained statement closure for MIPStarRE.LDT.Test.mainFormal as a quantum-information benchmark problem
• mark the main soundness theorem with @[eval_problem]
• add the corresponding manifest with the paper source and formal proof/comparator references

The statement comes from Ji–Natarajan–Vidick–Wright–Yuen, Quantum soundness of the classical low individual degree test (arXiv:2009.12982). It includes the corrected k ≥ 400md and k > 0 boundary hypotheses documented by the complete MIPStarRE formalization. The trusted prelude was generated from and audited against https://github.com/LionSR/MIPStarRE using https://github.com/leanprover/comparator.

Validation

• lake exe lean-eval validate-manifest
• lake exe lean-eval check-problem-build

Both pass; the only warnings are the expected benchmark sorry warnings.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.