feat(OpenQuantumProblems): Formalization of open quantum problem 35

[MarioKrenn6240]

Summary

This PR adds a formalization of Open Quantum Problem 35 from the IQOQI Vienna Open Quantum Problems list: existence of absolutely maximally entangled pure states.

Mathematical content

For integers n ≥ 2 and d ≥ 2, the problem asks for which pairs (n,d) there exists a pure AME(n,d) state.

A pure state ψ on n parties of local dimension d is absolutely maximally entangled (AME) if, for every subset of at most half of the parties, the corresponding reduced density matrix is maximally mixed.

In the formalization, a multipartite pure state is represented by a computational-basis amplitude function
ψ : (Fin n → Fin d) → ℂ,
together with an explicit normalization condition.

The reduced density matrix on the first m parties is defined by summing over the remaining n - m parties, and the AME condition is encoded by requiring maximal mixing after arbitrary permutations of the parties, which is equivalent to checking all subsystems of size ⌊n / 2⌋.

What is introduced

The file defines:

• IsNormalized for normalized multipartite pure states,
• reducedDensityFirst for the reduced density matrix on the first subsystem block,
• HasMaximallyMixedFirstReduction for maximal mixing of a chosen reduction,
• IsAME for absolutely maximally entangled pure states,
• ExistsAME n d for existence of an AME(n,d) state.

It also introduces a reusable witness family:

• diagonalState for the uniform superposition over constant computational-basis strings,
• bellState and ghzState as special cases of this family.

The key reusable lemma is:

• reducedDensityFirst_of_completion, showing that a state given by a uniform superposition over the graph of an injective completion map has maximally mixed reduction.

Included results

The PR includes:

• the open theorem oqp_35, expressing the full classification problem for all n ≥ 2 and d ≥ 2,
• the open theorems ame_8_4_open and ame_7_6_open, expressing two especially important small unresolved cases,
• the formally witnessed existence results ame_2_exists and ame_3_exists, obtained from the Bell and GHZ families,
• benchmark solved/source-backed theorems for AME(2,2), AME(3,2), AME(5,2), AME(6,2), AME(4,2), AME(7,2), AME(4,3), and AME(4,6),
• the sanity-check negative result ghzState4_not_ame, showing that the 4-party GHZ family is not AME for d ≥ 2.

The Bell and 3-party GHZ witnesses are proved directly in Lean via the generic completion criterion.

Background

An AME(n,d) state is equivalently a pure state that is maximally entangled across every bipartition, or a ⌊n / 2⌋-uniform state.

The problem is closely related to quantum error-correcting codes: existence of an AME(n,d) state is equivalent to existence of a pure ((n,1,⌊n/2⌋+1))_d quantum code.

For qubits (d = 2), AME states exist only for n = 2, 3, 5, 6; in particular, there is no AME(4,2) and no AME(7,2).
A particularly notable solved case is AME(4,6), whose construction goes beyond the usual stabilizer/classical-code framework.
In higher local dimensions, the full classification remains open.

References

Primary source list entry:

• IQOQI Vienna Open Quantum Problems, problem 35:
  https://oqp.iqoqi.oeaw.ac.at/existence-of-absolutely-maximally-entangled-pure-states
• Master list of open quantum problems:
  https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems

Foundational and benchmark references included in the docstring:

• W. Helwig, W. Cui, A. Riera, J. I. Latorre, and H.-K. Lo, Absolute Maximal Entanglement and Quantum Secret Sharing, Phys. Rev. A 86, 052335 (2012).
• D. Goyeneche, D. Alsina, J. I. Latorre, A. Riera, and K. Życzkowski, Absolutely Maximally Entangled states, combinatorial designs and multi-unitary matrices, Phys. Rev. A 92, 032316 (2015).
• A. Higuchi and A. Sudbery, How entangled can two couples get?, Phys. Lett. A 273, 213–217 (2000).
• A. J. Scott, Multipartite entanglement, quantum-error-correcting codes, and entangling power of quantum evolutions, Phys. Rev. A 69, 052330 (2004).
• F. Huber, O. Gühne, and J. Siewert, Absolutely maximally entangled states of seven qubits do not exist, Phys. Rev. Lett. 118, 200502 (2017).
• F. Huber and M. Grassl, Quantum Codes of Maximal Distance and Highly Entangled Subspaces, Quantum 4, 284 (2020).
• S. A. Rather, A. Burchardt, W. Bruzda, G. Rajchel-Mieldzioć, A. Lakshminarayan, and K. Życzkowski, Thirty-six entangled officers of Euler: Quantum solution to a classically impossible problem, Phys. Rev. Lett. 128, 080507 (2022).

Closes #3452.

Assisted by GPT Pro 5.4.