23.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

48 declarations, 16 contain sorry, 0 declared as axioms

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

Imports (1)

FormalConjecturesUtil

Imported by 2 files

abbrev OpenQuantumProblem23.StateVector A state vector in the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ line 116 source
Source documentation
A state vector in the $d$-dimensional complex Hilbert space $\mathbb{C}^d$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: EuclideanSpace, Complex, Fin
```
abbrev StateVector (d : ℕ) := EuclideanSpace ℂ (Fin d)
```
abbrev OpenQuantumProblem23.mkStateVector Build a state vector from its coordinates in the computational basis line 119 source
Source documentation
Build a state vector from its coordinates in the computational basis.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Complex, OpenQuantumProblem23.StateVector
Proof uses: WithLp.toLp, OfNat.ofNat, ENNReal
5 instances, coercions and auxiliary constants left out.
```
abbrev mkStateVector {d : ℕ} (ψ : Fin d → ℂ) : StateVector d := WithLp.toLp 2 ψ
```
Mentions: OpenQuantumProblem23.StateVector
instance OpenQuantumProblem23.(instance at line 122) line 122 source
Source documentation
Coercion from a state vector to its coordinate function.
```
instance {d : ℕ} : CoeFun (StateVector d) (fun _ => Fin d → ℂ) where
…
```
Mentions: OpenQuantumProblem23.StateVector
def OpenQuantumProblem23.IsNormalized A state vector is normalized if it has $L^2$ norm $1$ line 126 source
Source documentation
A state vector is normalized if it has $L^2$ norm $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem23.StateVector
Proof uses: Eq, Real, Norm.norm, OfNat.ofNat, ENNReal, Fin, Complex
10 instances, coercions and auxiliary constants left out.
```
def IsNormalized {d : ℕ} (ψ : StateVector d) : Prop := ‖ψ‖ = 1
```
Mentions: OpenQuantumProblem23.StateVector
def OpenQuantumProblem23.overlapSq The squared magnitude of the overlap between two state vectors line 129 source
Source documentation
The squared magnitude of the overlap between two state vectors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem23.StateVector, Real
Proof uses: MonoidWithZeroHom, Complex, Complex.normSq, Finset.sum, Fin, Finset.univ, HMul.hMul, Star.star, WithLp.ofLp, OfNat.ofNat, ENNReal
24 instances, coercions and auxiliary constants left out.
```
def overlapSq {d : ℕ} (φ ψ : StateVector d) : ℝ :=
…
```
Mentions: OpenQuantumProblem23.StateVector
def OpenQuantumProblem23.HasConstantOverlapSq A family has constant pairwise squared overlap $c$ if every two distinct members have squared overlap $c$ line 133 source
Source documentation
A family has constant pairwise squared overlap $c$ if every two distinct members have squared overlap $c$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Fin, OpenQuantumProblem23.StateVector
Proof uses: Pairwise, Eq, OpenQuantumProblem23.overlapSq
```
def HasConstantOverlapSq {d N : ℕ} (c : ℝ) (Φ : Fin N → StateVector d) : Prop :=
…
```
Mentions: c, OpenQuantumProblem23.StateVector
def OpenQuantumProblem23.sicOverlapSq The squared overlap value of a SIC family in dimension $d$ line 137 source
Source documentation
The squared overlap value of a SIC family in dimension $d$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Inv.inv, HAdd.hAdd, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def sicOverlapSq (d : ℕ) : ℝ := (d + 1 : ℝ)⁻¹
```
def OpenQuantumProblem23.IsSICFamily A SIC family in dimension $d$ consists of $d^2$ normalized vectors in $\mathbb{C}^d$ with pairwise squared overlap $(d + 1)^{-1}$ line 140 source
Source documentation
A SIC family in dimension $d$ consists of $d^2$ normalized vectors in $\mathbb{C}^d$ with pairwise squared overlap $(d + 1)^{-1}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HPow.hPow, OfNat.ofNat, OpenQuantumProblem23.StateVector
Proof uses: And, OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.HasConstantOverlapSq, OpenQuantumProblem23.sicOverlapSq
10 instances, coercions and auxiliary constants left out.
```
def IsSICFamily (d : ℕ) (Φ : Fin (d ^ 2) → StateVector d) : Prop :=
…
```
Mentions: OpenQuantumProblem23.StateVector
def OpenQuantumProblem23.HasSICPOVM There exists a SIC-POVM in dimension $d$ line 144 source
Source documentation
There exists a SIC-POVM in dimension $d$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Fin, HPow.hPow, OfNat.ofNat, OpenQuantumProblem23.StateVector, OpenQuantumProblem23.IsSICFamily
5 instances, coercions and auxiliary constants left out.
```
def HasSICPOVM (d : ℕ) : Prop :=
…
```
lemma OpenQuantumProblem23.hasConstantOverlapSq_singleton Any singleton family has constant pairwise squared overlap, vacuously line 151 source
Source documentation
Any singleton family has constant pairwise squared overlap, vacuously.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, OpenQuantumProblem23.StateVector, OpenQuantumProblem23.HasConstantOverlapSq, OfNat.ofNat, Fin
Proof uses: Ne, absurd, Eq, OpenQuantumProblem23.overlapSq, Subsingleton.elim
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma hasConstantOverlapSq_singleton {d : ℕ} (c : ℝ) (ψ : StateVector d) :
    HasConstantOverlapSq c (fun _ : Fin 1 => ψ) := by
…
```
Mentions: c, OpenQuantumProblem23.StateVector, OpenQuantumProblem23.HasConstantOverlapSq
lemma OpenQuantumProblem23.sicOverlapSq_one The SIC overlap value in dimension $1$ is $1/2$ line 158 source
Source documentation
The SIC overlap value in dimension $1$ is $1/2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, OpenQuantumProblem23.sicOverlapSq, OfNat.ofNat, Nat, HDiv.hDiv
Proof uses: Eq.mpr, HAdd.hAdd, id, Eq.trans, Inv.inv, congr, congrArg, congrFun', Nat.cast_one, one_div, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma sicOverlapSq_one : sicOverlapSq 1 = (1 / 2 : ℝ) := by
…
```
Mentions: OpenQuantumProblem23.sicOverlapSq
lemma OpenQuantumProblem23.sicOverlapSq_pos The SIC overlap value is positive in every dimension line 163 source
Source documentation
The SIC overlap value is positive in every dimension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, OfNat.ofNat, OpenQuantumProblem23.sicOverlapSq
Proof uses: Eq.mpr, HAdd.hAdd, id, Eq, Right.add_pos_of_nonneg_of_pos, LE.le, Nat.cast_nonneg', Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble
48 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma sicOverlapSq_pos (d : ℕ) : 0 < sicOverlapSq d := by
…
```
Mentions: OpenQuantumProblem23.sicOverlapSq
lemma OpenQuantumProblem23.isSICFamily_singleton_iff In dimension $1$, a singleton family is SIC exactly when its vector is normalized line 168 source
Source documentation
In dimension $1$, a singleton family is SIC exactly when its vector is normalized.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem23.StateVector, OfNat.ofNat, Nat, Iff, OpenQuantumProblem23.IsSICFamily, Fin, OpenQuantumProblem23.IsNormalized
Proof uses: Iff.intro, HPow.hPow, OpenQuantumProblem23.HasConstantOverlapSq, OpenQuantumProblem23.sicOverlapSq, And.intro, OpenQuantumProblem23.hasConstantOverlapSq_singleton
10 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma isSICFamily_singleton_iff {ψ : StateVector 1} :
    IsSICFamily 1 (fun _ : Fin 1 => ψ) ↔ IsNormalized ψ := by
…
```
Mentions: OpenQuantumProblem23.StateVector, OpenQuantumProblem23.IsSICFamily, OpenQuantumProblem23.IsNormalized
theorem OpenQuantumProblem23.hasSICPOVM_zero The empty family witnesses the degenerate dimension-$0$ case line 176 source
Source documentation
The empty family witnesses the degenerate dimension-$0$ case.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: Exists.intro, Fin, HPow.hPow, OpenQuantumProblem23.StateVector, OpenQuantumProblem23.IsSICFamily, Fin.elim0, And.intro, OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.HasConstantOverlapSq, OpenQuantumProblem23.sicOverlapSq, Ne, Eq, Real, OpenQuantumProblem23.overlapSq
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_zero : HasSICPOVM 0 := by
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
lemma OpenQuantumProblem23.isSICFamily_one_of_normalized Any normalized state in dimension $1$ yields a SIC family line 181 source
Source documentation
Any normalized state in dimension $1$ yields a SIC family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem23.StateVector, OfNat.ofNat, Nat, OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.IsSICFamily, Fin
Proof uses: Iff.mpr, OpenQuantumProblem23.isSICFamily_singleton_iff
2 instances, coercions and auxiliary constants left out.
```
lemma isSICFamily_one_of_normalized {ψ : StateVector 1} (hψ : IsNormalized ψ) :
    IsSICFamily 1 (fun _ : Fin 1 => ψ) :=
…
```
Mentions: OpenQuantumProblem23.StateVector, OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.IsSICFamily
theorem OpenQuantumProblem23.hasSICPOVM_one Dimension $1$ admits a SIC-POVM line 187 source
Source documentation
Dimension $1$ admits a SIC-POVM.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: Exists.intro, Fin, HPow.hPow, OpenQuantumProblem23.StateVector, OpenQuantumProblem23.IsSICFamily, EuclideanSpace.single, Complex, OpenQuantumProblem23.isSICFamily_one_of_normalized, of_eq_true, Eq, Real, Norm.norm, ENNReal, Eq.trans, True, congrFun', congrArg, PiLp, PiLp.single, PiLp.norm_single and 2 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_one : HasSICPOVM 1 := by
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
def OpenQuantumProblem23.ω The standard algebraic primitive cube root of unity line 194 source
Source documentation
The standard algebraic primitive cube root of unity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex
Proof uses: HAdd.hAdd, HDiv.hDiv, Real, Neg.neg, OfNat.ofNat, HMul.hMul, Real.sqrt, Complex.I
15 instances, coercions and auxiliary constants left out.
```
def ω : ℂ :=
…
```
def OpenQuantumProblem23.tetraA The first real amplitude used in the tetrahedral qubit SIC line 198 source
Source documentation
The first real amplitude used in the tetrahedral qubit SIC.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Real.sqrt, HDiv.hDiv, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
def tetraA : ℝ := Real.sqrt (1 / 3)
```
def OpenQuantumProblem23.tetraB The second real amplitude used in the tetrahedral qubit SIC line 201 source
Source documentation
The second real amplitude used in the tetrahedral qubit SIC.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Real.sqrt, HDiv.hDiv, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def tetraB : ℝ := Real.sqrt (2 / 3)
```
def OpenQuantumProblem23.hesseS The common scale used in the Hesse qutrit SIC line 204 source
Source documentation
The common scale used in the Hesse qutrit SIC.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Real.sqrt, HDiv.hDiv, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
def hesseS : ℝ := Real.sqrt (1 / 2)
```
def OpenQuantumProblem23.vec2 A convenient constructor for qubit state vectors line 207 source
Source documentation
A convenient constructor for qubit state vectors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, OpenQuantumProblem23.StateVector, OfNat.ofNat, Nat
Proof uses: OpenQuantumProblem23.mkStateVector, Matrix.vecCons, Matrix.vecEmpty
2 instances, coercions and auxiliary constants left out.
```
def vec2 (z₀ z₁ : ℂ) : StateVector 2 := mkStateVector ![z₀, z₁]
```
Mentions: OpenQuantumProblem23.StateVector, OpenQuantumProblem23.mkStateVector
def OpenQuantumProblem23.vec3 A convenient constructor for qutrit state vectors line 210 source
Source documentation
A convenient constructor for qutrit state vectors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, OpenQuantumProblem23.StateVector, OfNat.ofNat, Nat
Proof uses: OpenQuantumProblem23.mkStateVector, Matrix.vecCons, Matrix.vecEmpty
2 instances, coercions and auxiliary constants left out.
```
def vec3 (z₀ z₁ z₂ : ℂ) : StateVector 3 := mkStateVector ![z₀, z₁, z₂]
```
Mentions: OpenQuantumProblem23.StateVector, OpenQuantumProblem23.mkStateVector
def OpenQuantumProblem23.qubitSICFamily The tetrahedral qubit SIC family line 213 source
Source documentation
The tetrahedral qubit SIC family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, OpenQuantumProblem23.StateVector
Proof uses: OpenQuantumProblem23.qubitSICFamily.match_1, Unit, OpenQuantumProblem23.vec2, Complex, OpenQuantumProblem23.tetraA, OpenQuantumProblem23.tetraB, HMul.hMul, OpenQuantumProblem23.ω, HPow.hPow
14 instances, coercions and auxiliary constants left out.
```
def qubitSICFamily : Fin 4 → StateVector 2
  | 0 => vec2 1 0
  | 1 => vec2 (tetraA : ℂ) (tetraB : ℂ)
  | 2 => vec2 (tetraA : ℂ) ((tetraB : ℂ) * ω)
  | _ => vec2 (tetraA : ℂ) ((tetraB : ℂ) * (ω ^ 2))

/-- The Hesse qutrit SIC family. -/
```
Mentions: OpenQuantumProblem23.StateVector, OpenQuantumProblem23.vec2, OpenQuantumProblem23.tetraA, OpenQuantumProblem23.tetraB, OpenQuantumProblem23.ω
def OpenQuantumProblem23.hesseFamily The Hesse qutrit SIC family line 220 source
Source documentation
The Hesse qutrit SIC family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, OpenQuantumProblem23.StateVector
Proof uses: OpenQuantumProblem23.hesseFamily.match_1, Unit, OpenQuantumProblem23.vec3, Complex, OpenQuantumProblem23.hesseS, Neg.neg, HMul.hMul, OpenQuantumProblem23.ω, HPow.hPow
13 instances, coercions and auxiliary constants left out.
```
def hesseFamily : Fin 9 → StateVector 3
  | 0 => vec3 0 (hesseS : ℂ) (-(hesseS : ℂ))
  | 1 => vec3 0 (hesseS : ℂ) (-((hesseS : ℂ) * ω))
  | 2 => vec3 0 (hesseS : ℂ) (-((hesseS : ℂ) * (ω ^ 2)))
  | 3 => vec3 (-(hesseS : ℂ)) 0 (hesseS : ℂ)
  | 4 => vec3 (-((hesseS : ℂ) * ω)) 0 (hesseS : ℂ)
  | 5 => vec3 (-((hesseS : ℂ) * (ω ^ 2))) 0 (hesseS : ℂ)
  | 6 => vec3 (hesseS : ℂ) (-(hesseS : ℂ)) 0
  | 7 => vec3 (hesseS : ℂ) (-((hesseS : ℂ) * ω)) 0
  | _ => vec3 (hesseS : ℂ) (-((hesseS : ℂ) * (ω ^ 2))) 0

/-- The BB84 family of four qubit states. -/
```
Mentions: OpenQuantumProblem23.StateVector, OpenQuantumProblem23.vec3, OpenQuantumProblem23.hesseS, OpenQuantumProblem23.ω
def OpenQuantumProblem23.bb84Family The BB84 family of four qubit states line 232 source
Source documentation
The BB84 family of four qubit states.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, OpenQuantumProblem23.StateVector
Proof uses: OpenQuantumProblem23.qubitSICFamily.match_1, Unit, OpenQuantumProblem23.vec2, Complex, OpenQuantumProblem23.hesseS, Neg.neg
8 instances, coercions and auxiliary constants left out.
```
def bb84Family : Fin 4 → StateVector 2
  | 0 => vec2 1 0
  | 1 => vec2 0 1
  | 2 => vec2 (hesseS : ℂ) (hesseS : ℂ)
  | _ => vec2 (hesseS : ℂ) (-(hesseS : ℂ))

/-- The SIC overlap value in dimension $2$ is $1/3$. -/
@[category test, AMS 15 47 81]
```
Mentions: OpenQuantumProblem23.StateVector, OpenQuantumProblem23.vec2, OpenQuantumProblem23.hesseS, test, AMS
lemma OpenQuantumProblem23.sicOverlapSq_two The SIC overlap value in dimension $2$ is $1/3$ line 240 source
Source documentation
The SIC overlap value in dimension $2$ is $1/3$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, OpenQuantumProblem23.sicOverlapSq, OfNat.ofNat, Nat, HDiv.hDiv
Proof uses: Eq.mpr, HAdd.hAdd, id, Eq.trans, Inv.inv, congrArg, one_div, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_one
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma sicOverlapSq_two : sicOverlapSq 2 = (1 / 3 : ℝ) := by
…
```
Mentions: OpenQuantumProblem23.sicOverlapSq
lemma OpenQuantumProblem23.sicOverlapSq_three The SIC overlap value in dimension $3$ is $1/4$ line 245 source
Source documentation
The SIC overlap value in dimension $3$ is $1/4$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, OpenQuantumProblem23.sicOverlapSq, OfNat.ofNat, Nat, HDiv.hDiv
Proof uses: Eq.mpr, HAdd.hAdd, id, Eq.trans, Inv.inv, congrArg, one_div, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_one
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma sicOverlapSq_three : sicOverlapSq 3 = (1 / 4 : ℝ) := by
…
```
Mentions: OpenQuantumProblem23.sicOverlapSq
lemma OpenQuantumProblem23.omega_norm The unit complex number ω (primitive cube root) has norm 1 line 250 source
Source documentation
The unit complex number ω (primitive cube root) has norm 1.
```
private lemma omega_norm : ‖ω‖ = 1 := by
…
```
Mentions: OpenQuantumProblem23.ω
lemma OpenQuantumProblem23.qubitSICFamily_normalized Every vector in the tetrahedral qubit SIC family is normalized line 259 source
Source documentation
Every vector in the tetrahedral qubit SIC family is normalized.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.qubitSICFamily
Proof uses: Eq, Real, HPow.hPow, Real.sqrt, Real.sq_sqrt, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, LT.lt, Iff.mpr, Real.sqrt_pos, Mathlib.Meta.NormNum.isNat_lt_true, Bool.false, Norm.norm, Complex, OpenQuantumProblem23.ω and 186 more
175 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma qubitSICFamily_normalized (i : Fin 4) :
    IsNormalized (qubitSICFamily i) := by
…
```
Mentions: OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.qubitSICFamily
lemma OpenQuantumProblem23.qubitSICFamily_pairwise The tetrahedral qubit SIC family has the correct constant pairwise overlap sorry line 274 source
Source documentation
The tetrahedral qubit SIC family has the correct constant pairwise overlap.

depends on sorry what this means
Statement uses: OpenQuantumProblem23.HasConstantOverlapSq, OfNat.ofNat, Nat, OpenQuantumProblem23.sicOverlapSq, OpenQuantumProblem23.qubitSICFamily
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma qubitSICFamily_pairwise :
    HasConstantOverlapSq (sicOverlapSq 2) qubitSICFamily := by sorry
…
```
Mentions: OpenQuantumProblem23.HasConstantOverlapSq, OpenQuantumProblem23.sicOverlapSq, OpenQuantumProblem23.qubitSICFamily
theorem OpenQuantumProblem23.hasSICPOVM_two Dimension $2$ admits a SIC-POVM, witnessed by the tetrahedral qubit SIC sorry line 279 source
Source documentation
Dimension $2$ admits a SIC-POVM, witnessed by the tetrahedral qubit SIC.

depends on sorry what this means
Statement uses: OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_two : HasSICPOVM 2 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
lemma OpenQuantumProblem23.hesseFamily_normalized Every vector in the Hesse qutrit SIC family is normalized line 283 source
Source documentation
Every vector in the Hesse qutrit SIC family is normalized.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.hesseFamily
Proof uses: Eq, Real, HPow.hPow, Real.sqrt, Real.sq_sqrt, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, LT.lt, Iff.mpr, Real.sqrt_pos, Mathlib.Meta.NormNum.isNat_lt_true, Bool.false, Norm.norm, Complex, OpenQuantumProblem23.ω and 150 more
169 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma hesseFamily_normalized (i : Fin 9) :
    IsNormalized (hesseFamily i) := by
…
```
Mentions: OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.hesseFamily
lemma OpenQuantumProblem23.hesseFamily_pairwise The Hesse qutrit SIC family has the correct constant pairwise overlap sorry line 296 source
Source documentation
The Hesse qutrit SIC family has the correct constant pairwise overlap.

depends on sorry what this means
Statement uses: OpenQuantumProblem23.HasConstantOverlapSq, OfNat.ofNat, Nat, OpenQuantumProblem23.sicOverlapSq, OpenQuantumProblem23.hesseFamily
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma hesseFamily_pairwise :
    HasConstantOverlapSq (sicOverlapSq 3) hesseFamily := by sorry
…
```
Mentions: OpenQuantumProblem23.HasConstantOverlapSq, OpenQuantumProblem23.sicOverlapSq, OpenQuantumProblem23.hesseFamily
theorem OpenQuantumProblem23.hasSICPOVM_three Dimension $3$ admits a SIC-POVM, witnessed by the Hesse qutrit SIC sorry line 301 source
Source documentation
Dimension $3$ admits a SIC-POVM, witnessed by the Hesse qutrit SIC.

depends on sorry what this means
Statement uses: OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_three : HasSICPOVM 3 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
lemma OpenQuantumProblem23.bb84Family_normalized Every vector in the BB84 family is normalized line 305 source
Source documentation
Every vector in the BB84 family is normalized.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.bb84Family
Proof uses: List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true, Real, Norm.norm, OpenQuantumProblem23.StateVector, ENNReal and 65 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma bb84Family_normalized (i : Fin 4) :
    IsNormalized (bb84Family i) := by
…
```
Mentions: OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.bb84Family
theorem OpenQuantumProblem23.bb84Family_not_isSICFamily The BB84 family has the right cardinality for a qubit SIC but fails the constant-overlap condition line 311 source
Source documentation
The BB84 family has the right cardinality for a qubit SIC but fails the constant-overlap condition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, OpenQuantumProblem23.IsSICFamily, OfNat.ofNat, Nat, OpenQuantumProblem23.bb84Family
Proof uses: Fin, HPow.hPow, Eq, Real, OpenQuantumProblem23.overlapSq, OpenQuantumProblem23.sicOverlapSq, And.right, OpenQuantumProblem23.IsNormalized, OpenQuantumProblem23.HasConstantOverlapSq, Ne, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, False.elim, False, Eq.mp, Eq.trans and 39 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem bb84Family_not_isSICFamily : ¬ IsSICFamily 2 bb84Family := by
…
```
Mentions: OpenQuantumProblem23.IsSICFamily, OpenQuantumProblem23.bb84Family
theorem OpenQuantumProblem23.hasSICPOVM_56 Benchmark open subproblem: existence of a SIC-POVM in dimension $56$ sorry line 320 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $56$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_56 : answer(sorry) ↔ HasSICPOVM 56 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_58 Benchmark open subproblem: existence of a SIC-POVM in dimension $58$ sorry line 324 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $58$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_58 : answer(sorry) ↔ HasSICPOVM 58 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_59 Benchmark open subproblem: existence of a SIC-POVM in dimension $59$ sorry line 328 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $59$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_59 : answer(sorry) ↔ HasSICPOVM 59 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_60 Benchmark open subproblem: existence of a SIC-POVM in dimension $60$ sorry line 332 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $60$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_60 : answer(sorry) ↔ HasSICPOVM 60 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_64 Benchmark open subproblem: existence of a SIC-POVM in dimension $64$ sorry line 336 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $64$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_64 : answer(sorry) ↔ HasSICPOVM 64 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_68 Benchmark open subproblem: existence of a SIC-POVM in dimension $68$ sorry line 340 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $68$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_68 : answer(sorry) ↔ HasSICPOVM 68 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_69 Benchmark open subproblem: existence of a SIC-POVM in dimension $69$ sorry line 344 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $69$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_69 : answer(sorry) ↔ HasSICPOVM 69 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_70 Benchmark open subproblem: existence of a SIC-POVM in dimension $70$ sorry line 348 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $70$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_70 : answer(sorry) ↔ HasSICPOVM 70 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_71 Benchmark open subproblem: existence of a SIC-POVM in dimension $71$ sorry line 352 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $71$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_71 : answer(sorry) ↔ HasSICPOVM 71 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_72 Benchmark open subproblem: existence of a SIC-POVM in dimension $72$ sorry line 356 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $72$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_72 : answer(sorry) ↔ HasSICPOVM 72 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.hasSICPOVM_75 Benchmark open subproblem: existence of a SIC-POVM in dimension $75$ sorry line 360 source
Source documentation
Benchmark open subproblem: existence of a SIC-POVM in dimension $75$.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem23.HasSICPOVM, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasSICPOVM_75 : answer(sorry) ↔ HasSICPOVM 75 := by sorry
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM
theorem OpenQuantumProblem23.sicPOVMs Do SIC-POVMs exist in every finite dimension? sorry line 366 source
Source documentation
Do SIC-POVMs exist in every finite dimension?

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, OpenQuantumProblem23.HasSICPOVM
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem sicPOVMs :
    answer(sorry) ↔ ∀ d : ℕ, 1 ≤ d → HasSICPOVM d := by
…
```
Mentions: OpenQuantumProblem23.HasSICPOVM