Prove2Me

The symmetric support is not locally unitarily equivalent to antisymmetric support

Open
QAlgorithms.Papers.Independent.Intakethird100.P83.supportsNotLocallyUnitary

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For the qutrit state ρ(1/2)\rho^{(1/2)} defined in Proposition 5, let

S+=span⁡{∣01⟩+∣10⟩,∣02⟩+∣20⟩,∣12⟩+∣21⟩},S−=span⁡{∣01⟩−∣10⟩,∣02⟩−∣20⟩,∣12⟩−∣21⟩}.S_+=\operatorname{span}\{|01\rangle+|10\rangle,|02\rangle+|20\rangle,|12\rangle+|21\rangle\},\quad S_-=\operatorname{span}\{|01\rangle-|10\rangle,|02\rangle-|20\rangle,|12\rangle-|21\rangle\}.

Then supp⁡(ρ(1/2))=S+\operatorname{supp}(\rho^{(1/2)})=S_+, and there are no unitaries U,VU,V on the respective qutrit spaces for which (U⊗V)S+=S−(U\otimes V)S_+=S_-. Here S+S_+ is the displayed three-dimensional span. The assertion concerns local unitary equivalence of subspaces.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P83
Formal statement
noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P83

open QAlgorithms.Papers.Independent.Support50.P11 (Loewner)

open QAlgorithms.Papers.Independent.Dependency50.P32 (partialTranspose)

open QAlgorithms.Papers.Independent.Information100.P34 (supportProjector)

variable {A B C D : Type*}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

/-- Remark, PDF p.4: rho(1/2) has exactly the displayed three-dimensional
support, and no tensor product of local unitaries maps it onto S_minus. -/
theorem supportsNotLocallyUnitary :
    supportSpace (rhoAlpha (1/2)) = symmetricSupport ∧
    ¬ ∃ U V : Matrix.unitaryGroup (Fin 3) ℂ,
      Submodule.map (Matrix.toLin' (Matrix.kronecker (U : Matrix (Fin 3) (Fin 3) ℂ)
        (V : Matrix (Fin 3) (Fin 3) ℂ))) symmetricSupport = antisymmetricSupport := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end
Source
Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 4, Unnumbered Remark: symmetric-support example is not locally unitarily equivalent to antisymmetric support
Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let ∣ij⟩|ij\rangle, i,j∈{0,1,2}i,j\in\{0,1,2\}, denote the standard basis of C3⊗C3\mathbb C^3\otimes\mathbb C^3, and define

ρ1/2=16∑i<j(∣ij⟩+∣ji⟩)(⟨ij∣+⟨ji∣),S+=span⁡C{∣01⟩+∣10⟩, ∣02⟩+∣20⟩, ∣12⟩+∣21⟩},\rho_{1/2}=\frac16\sum_{i<j}(|ij\rangle+|ji\rangle)(\langle ij|+\langle ji|),\qquad S_+=\operatorname{span}_{\mathbb C}\{|01\rangle+|10\rangle,\ |02\rangle+|20\rangle,\ |12\rangle+|21\rangle\},

and S−=span⁡C{∣01⟩−∣10⟩, ∣02⟩−∣20⟩, ∣12⟩−∣21⟩}S_-=\operatorname{span}_{\mathbb C}\{|01\rangle-|10\rangle,\ |02\rangle-|20\rangle,\ |12\rangle-|21\rangle\}. The range of multiplication by ρ1/2\rho_{1/2} on the space of complex coordinate functions is exactly S+S_+, and there do not exist two 3×33\times3 unitary matrices U,VU,V for which the image (U⊗V)S+(U\otimes V)S_+ equals S−S_-.

Human review

  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph