Formalize Open Quantum Problem #28: Local equivalence of graph states

### What is the conjecture

This is problem [#28](https://oqp.iqoqi.oeaw.ac.at/local-equivalence-of-graph-states) 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 (solved by Ji–Chen–Wei–Ying; see below).

> **Problem (Open Quantum Problem #28: “Local equivalence of graph states”).**
> Decide whether two graph states, which can be mapped into each other by a local unitary, can also be mapped into each other by a local unitary from the Clifford group.

Concretely, let `G = (V,E)` be a finite simple graph on `n = |V|` vertices. The associated `n`-qubit **graph state** `|G⟩` can be defined as the unique joint `+1` eigenstate of the commuting stabilizer generators
`K_v = X_v ∏_{u ∈ N(v)} Z_u`, for `v ∈ V`,
where `N(v)` is the neighborhood of `v`.

Given graph states `|G⟩` and `|H⟩`, one says that they are:
- **LU-equivalent** if there exist single-qubit unitaries `U_1, …, U_n` and a phase `e^{iφ}` such that
`|H⟩ = e^{iφ} (U_1 ⊗ … ⊗ U_n) |G⟩`;
- **LC-equivalent** if the same holds with each `U_i` belonging to the single-qubit **Clifford group**.

For graph states, LC-equivalence has a clean graph-theoretic description via **local complementation**: for a vertex `v`, the local complementation `τ_v(G)` replaces the induced subgraph on `N(v)` by its graph-theoretic complement. Two graph states are LC-equivalent iff their graphs are related by a finite sequence of such local complementations.

The original LU–LC question asks whether
`LU_equiv(|G⟩, |H⟩) ⇒ LC_equiv(|G⟩, |H⟩)`
for all graph states `|G⟩` and `|H⟩`.

**Solved statement to formalize (Ji–Chen–Wei–Ying, 2007/2010):**
The answer is **no**. Ji–Chen–Wei–Ying disprove the LU–LC conjecture by constructing an explicit **27-qubit** counterexample in the stabilizer formalism, found by systematic computer search. Since every stabilizer state is LC-equivalent to some graph state, this yields graph-state counterexamples as well. Equivalently, there exist graph states `|G⟩` and `|H⟩` on 27 qubits such that:
- `|H⟩ = e^{iφ} (U_1 ⊗ … ⊗ U_27) |G⟩` for some local unitaries `U_i`,
- but there do **not** exist single-qubit Clifford operators `C_i` and phase `e^{iφ'}` with
`|H⟩ = e^{iφ'} (C_1 ⊗ … ⊗ C_27) |G⟩`.

Equivalently: there exist 27-vertex graphs whose graph states are locally unitary equivalent but are **not** related by any sequence of local complementations.

A compact theorem-level target is therefore:
`∃ G,H` simple graphs on 27 vertices such that `LU_equiv(|G⟩, |H⟩) ∧ ¬ LC_equiv(|G⟩, |H⟩)`.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #28)](https://oqp.iqoqi.oeaw.ac.at/local-equivalence-of-graph-states)
- [Solved Quantum Problems list (shows #28 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 28”)

Key solution reference (as cited on the OQP page):
- Z. Ji, J. Chen, Z. Wei, and M. Ying, **“The LU-LC conjecture is false”**, *Quantum Inf. Comput.* 10, 97–108 (2010); arXiv: [0709.1266](https://arxiv.org/abs/0709.1266)

Related / partial results mentioned on the OQP page (useful background for a formalization roadmap):
- M. Van den Nest, J. Dehaene, and B. De Moor, **“On local unitary versus local Clifford equivalence of stabilizer states”**, *Phys. Rev. A* 71, 062323 (2005); arXiv: [quant-ph/0411115](https://arxiv.org/abs/quant-ph/0411115) — proves `LU ⇒ LC` for a significant class of stabilizer/graph states, including GL(4)-linear-code states and GHZ / star-graph states
- M. Hein, J. Eisert, and H. J. Briegel, **“Multi-party entanglement in graph states”**, *Phys. Rev. A* 69, 062311 (2004); arXiv: [quant-ph/0307130](https://arxiv.org/abs/quant-ph/0307130) — background on graph states and numerical evidence that LU and LC coincide for connected graphs up to 7 vertices
- M. Van den Nest, J. Dehaene, and B. De Moor, **“An efficient algorithm to recognize local Clifford equivalence of graph states”**, *Phys. Rev. A* 70, 034302 (2004); arXiv: [quant-ph/0405023](https://arxiv.org/abs/quant-ph/0405023) — LC-equivalence via sequences of local complementations, plus an efficient recognition algorithm
- D. Gross and M. Van den Nest, **“The LU-LC conjecture, diagonal local operations and quadratic forms over GF(2)”**, *Quantum Inf. Comput.* 8, 263–281 (2008); arXiv: [0707.4000](https://arxiv.org/abs/0707.4000) — reduces the conjecture to the diagonal-local-unitary / quadratic-form setting

### Prerequisites needed

- Finite-dimensional qubit Hilbert spaces; tensor products; Pauli matrices/operators
- Stabilizer formalism and graph states: commuting Pauli subgroups, stabilizer generators `K_v`, graph-state construction
- Local unitary equivalence vs local Clifford equivalence; single-qubit Clifford group; equivalence up to global phase
- Basic graph theory: neighborhoods, local complementation, and sequences of local complementations
- (If following the Gross–Van den Nest / Ji et al. route) binary linear algebra and quadratic forms over `GF(2)`, or alternatively a finite verification of a concrete 27-qubit counterexample

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

- ams-81 (Quantum theory)
- ams-05 (Combinatorics)
- ams-20 (Group theory and generalizations)

### 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
---

Read Ji–Chen–Wei–Ying, “The LU-LC conjecture is false” (arXiv:0709.1266), together with the graph-state and local-complementation references in the issue. Define the required graph, stabilizer, LU, and LC notions in the repository’s Lean style, then formalize the theorem asserting a 27-qubit counterexample. Done means the theorem-level existence statement is accepted by Lean.

Written by the indexing model from the issue text.