Formalize Open Quantum Problem #3: Polynomial entanglement invariants

### What is the conjecture
This is problem [#3](https://oqp.iqoqi.oeaw.ac.at/polynomial-entanglement-invariants/) in [Reinhard F. Werner's collection](https://arxiv.org/abs/quant-ph/0504166), later [collected by a community of quantum researchers](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

**Status:** this problem is listed as **solved** on the [Solved Quantum Problems](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems) page (solution idea: invariant theory for compact groups).

> **Problem (Open Quantum Problem #3: “Polynomial entanglement invariants”).**
> We say that two bipartite quantum states ρ and σ are “equally entangled” if they differ only by a choice of bases in Alice’s and Bob’s subspaces, i.e., if there exist unitaries `U_A`, `U_B` such that
> `ρ = (U_A ⊗ U_B) σ (U_A ⊗ U_B)^*`.
>
> An *entanglement invariant* is any real-valued function on bipartite density operators that is constant on these local-unitary orbits. A *polynomial invariant* is such an invariant given by a polynomial in the matrix entries of ρ (allowing conjugates doesn’t enlarge the class since ρ is Hermitian).
>
> **Main question:** are polynomial entanglement invariants **complete**?
> i.e. if *all* polynomial invariants take the same values on ρ and σ, must there exist local unitaries `U_A`, `U_B` with `ρ = (U_A ⊗ U_B) σ (U_A ⊗ U_B)^*`?

Informal rephrasing: do polynomial invariants separate local-unitary equivalence classes of (bi-/multi-partite) quantum states?

The OQP page also lists closely related sub-questions, e.g.:
- for fixed local dimensions `(d_A, d_B)`, exhibit an explicit **finite** complete set of polynomial invariants;
- extend this to **multipartite** systems;
- (more speculative) whether separability can be characterized by a single polynomial inequality `f(ρ) ≥ 0` equivalent to “ρ is separable” (or weaker variants).

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #3)](https://oqp.iqoqi.oeaw.ac.at/polynomial-entanglement-invariants/)
- [Solved Quantum Problems list (marks #3 as solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
- [Werner / Krüger–Werner arXiv list](https://arxiv.org/abs/quant-ph/0504166) (see “Problem 3”)

Key related references mentioned on the problem page:
- M. Grassl, M. Rötteler, and T. Beth, “Computing local invariants of qubit systems” (Phys. Rev. A 58, 1833 (1998); arXiv: quant-ph/9712040)
- E. M. Rains, “Polynomial invariants of quantum codes” (arXiv: quant-ph/9704042)
- Y. Makhlin, “Nonlocal properties of two-qubit gates and mixed states and optimization of quantum computations” (arXiv: quant-ph/0002045)
- A. Sudbery, “On local invariants of pure three-qubit states” (J. Phys. A 34, 643 (2001); arXiv: quant-ph/0001116)
- A. L. Onishchik and E. B. Vinberg, *Lie Groups and Algebraic Groups* (Springer, 1990), Chap. 3, §4, Thm. 3 (used in the OQP “Solution” section: polynomial invariants separate orbits of compact linear group actions)
- H. A. Carteret, A. Higuchi, and A. Sudbery, “Multipartite generalisation of the Schmidt decomposition” (J. Math. Phys. 41 (2000); arXiv: quant-ph/0006125)
- A. Acín, A. Andrianov, E. Jane, and R. Tarrach, “Three-qubit pure-state canonical forms” (J. Phys. A 34, 6725 (2001); arXiv: quant-ph/0009107)
- H. A. Carteret and A. Sudbery, “Local symmetry properties of pure states of three qubits” (J. Phys. A 33, 4981 (2000); arXiv: quant-ph/0001091)
- W. Dür, G. Vidal, and J. I. Cirac, “Three qubits can be entangled in two inequivalent ways” (Phys. Rev. A 62, 062314 (2000); arXiv: quant-ph/0005115)
- B. De Moor, F. Verstraete, J. Dehaene, and H. Verschelde, “Four qubits can be entangled in nine inequivalent ways” (arXiv: quant-ph/0109033)

### Prerequisites needed
- Finite-dimensional complex Hilbert spaces; tensor products; adjoints; traces
- Density operators (Hermitian/PSD, trace 1) and the **local unitary** group action `ρ ↦ (U_1 ⊗ … ⊗ U_n) ρ (U_1 ⊗ … ⊗ U_n)^*`
- Polynomial functions on finite-dimensional real vector spaces (e.g. on Hermitian matrices seen as a real vector space)
- Basic invariant theory / group actions: definition of “polynomial invariant”, and the notion of invariants **separating** orbits
- (If formalizing the “Solution”) a theorem of the form: *orbits of a compact linear group action are separated by polynomial invariants*, and instantiation to local unitary groups

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)
* ams-81 (Quantum theory)
* ams-20 (Group theory and generalizations)
* ams-13 (Commutative algebra / invariant theory)

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [X] This issue is up for grabs: I would like to see this conjecture added by somebody else

No repository files, tests, or Lean entry points are named. Start with the repository's existing formalized conjectures, then read the linked OQP solution and invariant-theory references to determine a suitable formalization scope. Done means the polynomial-invariant conjecture is added in Lean with the requested local-unitary setting and accepted repository checks.

Written by the indexing model from the issue text.