Open Quantum Problem 23: SIC-POVMs

Mathematical problem

The OQP page presents three increasingly strong formulations of this problem. In this file we formalize the first one, closest to the physics terminology: existence of a symmetric informationally complete POVM in every finite dimension.

A SIC-POVM in dimension $d$ can be represented by a family of $d^2$ normalized vectors in $\mathbb{C}^d$ whose pairwise squared overlaps are all equal to $(d + 1)^{-1}$. We encode such a family as a map Fin (d ^ 2) → StateVector d.

Background

SIC-POVMs are a basic structure in finite-dimensional quantum information. They are closely related to equiangular lines, tight frames, quantum state reconstruction, and finite-dimensional measurement theory. The open problem asks whether such families exist in every dimension.

What this file formalizes

This file formalizes the existence problem for symmetric informationally complete POVMs through the predicate HasSICPOVM d.

More precisely, it contains the following layers.

Core API

The main definitions formalized in this file are:

• StateVector d: a state vector in ℂ^d;
• mkStateVector: constructor from coordinates in the computational basis;
• IsNormalized ψ: normalization predicate for a state vector;
• overlapSq φ ψ: squared magnitude of the inner-product overlap;
• HasConstantOverlapSq c Φ: constant pairwise squared-overlap condition;
• sicOverlapSq d: the SIC overlap value (d + 1)⁻¹;
• IsSICFamily d Φ: the predicate that a family of d^2 vectors in ℂ^d is a SIC family;
• HasSICPOVM d: existence of a SIC family in dimension d.

In addition, the file includes explicit witness families and convenient constructors used in the low-dimensional benchmark cases:

• vec2, vec3;
• qubitSICFamily;
• hesseFamily;
• bb84Family.

Complete open conjecture

The main open theorem is:

• sicPOVMs, expressing the conjecture that for every d ≥ 1, there exists a SIC-POVM in dimension d.

Special cases

The file also isolates several special cases:

• solved low-dimensional benchmark cases: hasSICPOVM_zero, hasSICPOVM_one, hasSICPOVM_two, hasSICPOVM_three;
• a negative benchmark result: bb84Family_not_isSICFamily, showing that the BB84 family in dimension 2 does not form a SIC family;
• selected open benchmark dimensions: hasSICPOVM_56, hasSICPOVM_58, hasSICPOVM_59, hasSICPOVM_60, hasSICPOVM_64, hasSICPOVM_68, hasSICPOVM_69, hasSICPOVM_70, hasSICPOVM_71, hasSICPOVM_72, hasSICPOVM_75.

Test lemmas

The file includes the following test lemmas and benchmark-support statements:

• hasConstantOverlapSq_singleton;
• sicOverlapSq_one, sicOverlapSq_two, sicOverlapSq_three, sicOverlapSq_pos;
• isSICFamily_singleton_iff, isSICFamily_one_of_normalized;
• qubitSICFamily_normalized, qubitSICFamily_pairwise;
• hesseFamily_normalized, hesseFamily_pairwise;
• bb84Family_normalized.

At present, these @[category test, AMS 15 47 81] results are included with placeholder proofs by sorry; they are intended to be proved in the next PR.

References

Primary source list entry:

• IQOQI Vienna Open Quantum Problems, problem 23: https://oqp.iqoqi.oeaw.ac.at/sic-povms-and-zauners-conjecture
• Formal Conjectures issue #1823: https://github.com/google-deepmind/formal-conjectures/issues/1823

Foundational references

• J. M. Renes, R. Blume-Kohout, A. J. Scott, and M. C. Caves, Symmetric informationally complete quantum measurements, J. Math. Phys. 45, 2171-2180 (2004), arXiv:quant-ph/0310075.
• G. Zauner, Quantum Designs: Foundations of a Noncommutative Design Theory, PhD thesis, University of Vienna (1999).

@[reducible, inline]

abbrev OpenQuantumProblem23.StateVector (d : ℕ) : Type

A state vector in the $d$-dimensional complex Hilbert space $\mathbb{C}^d$.

Equations

• OpenQuantumProblem23.StateVector d = EuclideanSpace ℂ (Fin d)

@[reducible, inline]

abbrev OpenQuantumProblem23.mkStateVector {d : ℕ} (ψ : Fin d → ℂ) : StateVector d

Build a state vector from its coordinates in the computational basis.

Equations

• OpenQuantumProblem23.mkStateVector ψ = WithLp.toLp 2 ψ

instance OpenQuantumProblem23.instCoeFunStateVectorForallFinComplex {d : ℕ} : CoeFun (StateVector d) fun (x : StateVector d) => Fin d → ℂ

Coercion from a state vector to its coordinate function.

Equations

• OpenQuantumProblem23.instCoeFunStateVectorForallFinComplex = { coe := fun (ψ : OpenQuantumProblem23.StateVector d) => ψ.ofLp }

def OpenQuantumProblem23.IsNormalized {d : ℕ} (ψ : StateVector d) : Prop

A state vector is normalized if it has $L^2$ norm $1$.

Equations

• OpenQuantumProblem23.IsNormalized ψ = (‖ψ‖ = 1)

def OpenQuantumProblem23.overlapSq {d : ℕ} (φ ψ : StateVector d) : ℝ

The squared magnitude of the overlap between two state vectors.

Equations

• OpenQuantumProblem23.overlapSq φ ψ = Complex.normSq (∑ i : Fin d, star (φ.ofLp i) * ψ.ofLp i)

def OpenQuantumProblem23.HasConstantOverlapSq {d N : ℕ} (c : ℝ) (Φ : Fin N → StateVector d) : Prop

A family has constant pairwise squared overlap $c$ if every two distinct members have squared overlap $c$.

Equations

• OpenQuantumProblem23.HasConstantOverlapSq c Φ = Pairwise fun (i j : Fin N) => OpenQuantumProblem23.overlapSq (Φ i) (Φ j) = c

def OpenQuantumProblem23.sicOverlapSq (d : ℕ) : ℝ

The squared overlap value of a SIC family in dimension $d$.

Equations

• OpenQuantumProblem23.sicOverlapSq d = (↑d + 1)⁻¹

def OpenQuantumProblem23.IsSICFamily (d : ℕ) (Φ : Fin (d ^ 2) → StateVector d) : Prop

A SIC family in dimension $d$ consists of $d^2$ normalized vectors in $\mathbb{C}^d$ with pairwise squared overlap $(d + 1)^{-1}$.

Equations

• OpenQuantumProblem23.IsSICFamily d Φ = ((∀ (i : Fin (d ^ 2)), OpenQuantumProblem23.IsNormalized (Φ i)) ∧ OpenQuantumProblem23.HasConstantOverlapSq (OpenQuantumProblem23.sicOverlapSq d) Φ)

def OpenQuantumProblem23.HasSICPOVM (d : ℕ) : Prop

There exists a SIC-POVM in dimension $d$.

Equations

• OpenQuantumProblem23.HasSICPOVM d = ∃ (Φ : Fin (d ^ 2) → OpenQuantumProblem23.StateVector d), OpenQuantumProblem23.IsSICFamily d Φ

theorem OpenQuantumProblem23.hasConstantOverlapSq_singleton {d : ℕ} (c : ℝ) (ψ : StateVector d) : HasConstantOverlapSq c fun (x : Fin 1) => ψ

Any singleton family has constant pairwise squared overlap, vacuously.

theorem OpenQuantumProblem23.sicOverlapSq_one : sicOverlapSq 1 = 1 / 2

The SIC overlap value in dimension $1$ is $1/2$.

theorem OpenQuantumProblem23.sicOverlapSq_pos (d : ℕ) : 0 < sicOverlapSq d

The SIC overlap value is positive in every dimension.

theorem OpenQuantumProblem23.isSICFamily_singleton_iff {ψ : StateVector 1} : (IsSICFamily 1 fun (x : Fin 1) => ψ) ↔ IsNormalized ψ

In dimension $1$, a singleton family is SIC exactly when its vector is normalized.

theorem OpenQuantumProblem23.hasSICPOVM_zero : HasSICPOVM 0

The empty family witnesses the degenerate dimension-$0$ case.

theorem OpenQuantumProblem23.isSICFamily_one_of_normalized {ψ : StateVector 1} (hψ : IsNormalized ψ) : IsSICFamily 1 fun (x : Fin 1) => ψ

Any normalized state in dimension $1$ yields a SIC family.

theorem OpenQuantumProblem23.hasSICPOVM_one : HasSICPOVM 1

Dimension $1$ admits a SIC-POVM.

def OpenQuantumProblem23.ω : ℂ

The standard algebraic primitive cube root of unity.

Equations

• OpenQuantumProblem23.ω = ↑(-1 / 2) + ↑(√3 / 2) * Complex.I

def OpenQuantumProblem23.tetraA : ℝ

The first real amplitude used in the tetrahedral qubit SIC.

Equations

• OpenQuantumProblem23.tetraA = √(1 / 3)

def OpenQuantumProblem23.tetraB : ℝ

The second real amplitude used in the tetrahedral qubit SIC.

Equations

• OpenQuantumProblem23.tetraB = √(2 / 3)

def OpenQuantumProblem23.hesseS : ℝ

The common scale used in the Hesse qutrit SIC.

Equations

• OpenQuantumProblem23.hesseS = √(1 / 2)

def OpenQuantumProblem23.vec2 (z₀ z₁ : ℂ) : StateVector 2

A convenient constructor for qubit state vectors.

Equations

• OpenQuantumProblem23.vec2 z₀ z₁ = OpenQuantumProblem23.mkStateVector ![z₀, z₁]

def OpenQuantumProblem23.vec3 (z₀ z₁ z₂ : ℂ) : StateVector 3

A convenient constructor for qutrit state vectors.

Equations

• OpenQuantumProblem23.vec3 z₀ z₁ z₂ = OpenQuantumProblem23.mkStateVector ![z₀, z₁, z₂]

def OpenQuantumProblem23.qubitSICFamily : Fin 4 → StateVector 2

The tetrahedral qubit SIC family.

Equations

• OpenQuantumProblem23.qubitSICFamily 0 = OpenQuantumProblem23.vec2 1 0
• OpenQuantumProblem23.qubitSICFamily 1 = OpenQuantumProblem23.vec2 ↑OpenQuantumProblem23.tetraA ↑OpenQuantumProblem23.tetraB
• OpenQuantumProblem23.qubitSICFamily 2 = OpenQuantumProblem23.vec2 (↑OpenQuantumProblem23.tetraA) (↑OpenQuantumProblem23.tetraB * OpenQuantumProblem23.ω)
• OpenQuantumProblem23.qubitSICFamily x✝ = OpenQuantumProblem23.vec2 (↑OpenQuantumProblem23.tetraA) (↑OpenQuantumProblem23.tetraB * OpenQuantumProblem23.ω ^ 2)

def OpenQuantumProblem23.hesseFamily : Fin 9 → StateVector 3

The Hesse qutrit SIC family.

Equations

• OpenQuantumProblem23.hesseFamily 0 = OpenQuantumProblem23.vec3 0 (↑OpenQuantumProblem23.hesseS) (-↑OpenQuantumProblem23.hesseS)
• OpenQuantumProblem23.hesseFamily 1 = OpenQuantumProblem23.vec3 0 (↑OpenQuantumProblem23.hesseS) (-(↑OpenQuantumProblem23.hesseS * OpenQuantumProblem23.ω))
• OpenQuantumProblem23.hesseFamily 2 = OpenQuantumProblem23.vec3 0 (↑OpenQuantumProblem23.hesseS) (-(↑OpenQuantumProblem23.hesseS * OpenQuantumProblem23.ω ^ 2))
• OpenQuantumProblem23.hesseFamily 3 = OpenQuantumProblem23.vec3 (-↑OpenQuantumProblem23.hesseS) 0 ↑OpenQuantumProblem23.hesseS
• OpenQuantumProblem23.hesseFamily 4 = OpenQuantumProblem23.vec3 (-(↑OpenQuantumProblem23.hesseS * OpenQuantumProblem23.ω)) 0 ↑OpenQuantumProblem23.hesseS
• OpenQuantumProblem23.hesseFamily 5 = OpenQuantumProblem23.vec3 (-(↑OpenQuantumProblem23.hesseS * OpenQuantumProblem23.ω ^ 2)) 0 ↑OpenQuantumProblem23.hesseS
• OpenQuantumProblem23.hesseFamily 6 = OpenQuantumProblem23.vec3 (↑OpenQuantumProblem23.hesseS) (-↑OpenQuantumProblem23.hesseS) 0
• OpenQuantumProblem23.hesseFamily 7 = OpenQuantumProblem23.vec3 (↑OpenQuantumProblem23.hesseS) (-(↑OpenQuantumProblem23.hesseS * OpenQuantumProblem23.ω)) 0
• OpenQuantumProblem23.hesseFamily x✝ = OpenQuantumProblem23.vec3 (↑OpenQuantumProblem23.hesseS) (-(↑OpenQuantumProblem23.hesseS * OpenQuantumProblem23.ω ^ 2)) 0

def OpenQuantumProblem23.bb84Family : Fin 4 → StateVector 2

The BB84 family of four qubit states.

Equations

• OpenQuantumProblem23.bb84Family 0 = OpenQuantumProblem23.vec2 1 0
• OpenQuantumProblem23.bb84Family 1 = OpenQuantumProblem23.vec2 0 1
• OpenQuantumProblem23.bb84Family 2 = OpenQuantumProblem23.vec2 ↑OpenQuantumProblem23.hesseS ↑OpenQuantumProblem23.hesseS
• OpenQuantumProblem23.bb84Family x✝ = OpenQuantumProblem23.vec2 (↑OpenQuantumProblem23.hesseS) (-↑OpenQuantumProblem23.hesseS)

theorem OpenQuantumProblem23.sicOverlapSq_two : sicOverlapSq 2 = 1 / 3

The SIC overlap value in dimension $2$ is $1/3$.

theorem OpenQuantumProblem23.sicOverlapSq_three : sicOverlapSq 3 = 1 / 4

The SIC overlap value in dimension $3$ is $1/4$.

theorem OpenQuantumProblem23.qubitSICFamily_normalized (i : Fin 4) : IsNormalized (qubitSICFamily i)

Every vector in the tetrahedral qubit SIC family is normalized.

theorem OpenQuantumProblem23.qubitSICFamily_pairwise : HasConstantOverlapSq (sicOverlapSq 2) qubitSICFamily

The tetrahedral qubit SIC family has the correct constant pairwise overlap.

theorem OpenQuantumProblem23.hasSICPOVM_two : HasSICPOVM 2

Dimension $2$ admits a SIC-POVM, witnessed by the tetrahedral qubit SIC.

theorem OpenQuantumProblem23.hesseFamily_normalized (i : Fin 9) : IsNormalized (hesseFamily i)

Every vector in the Hesse qutrit SIC family is normalized.

theorem OpenQuantumProblem23.hesseFamily_pairwise : HasConstantOverlapSq (sicOverlapSq 3) hesseFamily

The Hesse qutrit SIC family has the correct constant pairwise overlap.

theorem OpenQuantumProblem23.hasSICPOVM_three : HasSICPOVM 3

Dimension $3$ admits a SIC-POVM, witnessed by the Hesse qutrit SIC.

theorem OpenQuantumProblem23.bb84Family_normalized (i : Fin 4) : IsNormalized (bb84Family i)

Every vector in the BB84 family is normalized.

theorem OpenQuantumProblem23.bb84Family_not_isSICFamily : ¬IsSICFamily 2 bb84Family

The BB84 family has the right cardinality for a qubit SIC but fails the constant-overlap condition.

theorem OpenQuantumProblem23.hasSICPOVM_56 : True ↔ HasSICPOVM 56

Benchmark open subproblem: existence of a SIC-POVM in dimension $56$.

theorem OpenQuantumProblem23.hasSICPOVM_58 : True ↔ HasSICPOVM 58

Benchmark open subproblem: existence of a SIC-POVM in dimension $58$.

theorem OpenQuantumProblem23.hasSICPOVM_59 : True ↔ HasSICPOVM 59

Benchmark open subproblem: existence of a SIC-POVM in dimension $59$.

theorem OpenQuantumProblem23.hasSICPOVM_60 : True ↔ HasSICPOVM 60

Benchmark open subproblem: existence of a SIC-POVM in dimension $60$.

theorem OpenQuantumProblem23.hasSICPOVM_64 : True ↔ HasSICPOVM 64

Benchmark open subproblem: existence of a SIC-POVM in dimension $64$.

theorem OpenQuantumProblem23.hasSICPOVM_68 : True ↔ HasSICPOVM 68

Benchmark open subproblem: existence of a SIC-POVM in dimension $68$.

theorem OpenQuantumProblem23.hasSICPOVM_69 : True ↔ HasSICPOVM 69

Benchmark open subproblem: existence of a SIC-POVM in dimension $69$.

theorem OpenQuantumProblem23.hasSICPOVM_70 : True ↔ HasSICPOVM 70

Benchmark open subproblem: existence of a SIC-POVM in dimension $70$.

theorem OpenQuantumProblem23.hasSICPOVM_71 : True ↔ HasSICPOVM 71

Benchmark open subproblem: existence of a SIC-POVM in dimension $71$.

theorem OpenQuantumProblem23.hasSICPOVM_72 : True ↔ HasSICPOVM 72

Benchmark open subproblem: existence of a SIC-POVM in dimension $72$.

theorem OpenQuantumProblem23.hasSICPOVM_75 : True ↔ HasSICPOVM 75

Benchmark open subproblem: existence of a SIC-POVM in dimension $75$.

theorem OpenQuantumProblem23.sicPOVMs : True ↔ ∀ (d : ℕ), 1 ≤ d → HasSICPOVM d

Do SIC-POVMs exist in every finite dimension?