Open Quantum Problem 23: SIC-POVMs

The question

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

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

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

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

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

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

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

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

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

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

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

sicPOVMs. Do SIC-POVMs exist in every finite dimension?

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 $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).

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OpenQuantumProblems.«23» (12 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem hasSICPOVM_56 : answer(sorry) ↔ HasSICPOVM 56

theorem hasSICPOVM_58 : answer(sorry) ↔ HasSICPOVM 58

theorem hasSICPOVM_59 : answer(sorry) ↔ HasSICPOVM 59

theorem hasSICPOVM_60 : answer(sorry) ↔ HasSICPOVM 60

theorem hasSICPOVM_64 : answer(sorry) ↔ HasSICPOVM 64

theorem hasSICPOVM_68 : answer(sorry) ↔ HasSICPOVM 68

theorem hasSICPOVM_69 : answer(sorry) ↔ HasSICPOVM 69

theorem hasSICPOVM_70 : answer(sorry) ↔ HasSICPOVM 70

theorem hasSICPOVM_71 : answer(sorry) ↔ HasSICPOVM 71

theorem hasSICPOVM_72 : answer(sorry) ↔ HasSICPOVM 72

theorem hasSICPOVM_75 : answer(sorry) ↔ HasSICPOVM 75

theorem sicPOVMs :
    answer(sorry) ↔ ∀ d : ℕ, 1 ≤ d → HasSICPOVM d

What counts as progress

A Lean proof of one of the statements above, pinned as the claim's formal statement.
Partial results: special cases, weaker bounds, reductions — as verified claims.
Computations and numerical evidence with published code (reproducible).
Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Source and licence

Imported from Formal Conjectures (Open quantum problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.