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

53 declarations, 7 contain sorry, 0 declared as axioms

Open Quantum Problem 13: Mutually unbiased bases

Mathematical problem

For each integer $d \ge 2$, determine the maximum number $k$ for which there exist orthonormal bases $\mathcal{B}_1, \dots, \mathcal{B}_k$ of the complex Hilbert space $\mathbb{C}^d$ such that any two distinct bases are mutually unbiased.

Concretely, if $\mathcal{B}_r = \{ e_0^{(r)}, \dots, e_{d-1}^{(r)} \}$ and $\mathcal{B}_s = \{ e_0^{(s)}, \dots, e_{d-1}^{(s)} \}$, then $\mathcal{B}_r$ and $\mathcal{B}_s$ are mutually unbiased if for all $i, j$ and all $r \ne s$, $|\langle e_i^{(r)}, e_j^{(s)} \rangle| = d^{-1/2}$.

The problem is therefore to determine the maximal value $\mu(d) := \max \{ k : \text{there exist } k \text{ pairwise mutually unbiased orthonormal bases in } \mathbb{C}^d \}$.

In this file, an orthonormal basis is represented by a unitary matrix whose columns are the basis vectors. For two such bases U and V, the matrix relativeUnitary U V, which is $U^\dagger V$, contains all cross-basis overlaps as its entries. Since Lean works more smoothly with squared norms, we formalize mutual unbiasedness by requiring $\| (relativeUnitary\ U\ V)_{ij} \|^2 = 1 / d$ for all $i, j$, which is equivalent to $|\langle e_i^{(r)}, e_j^{(s)} \rangle| = d^{-1/2}$.

Background

Mutually unbiased bases are a basic structure in finite-dimensional quantum theory. They arise in quantum state determination, quantum tomography, quantum cryptography, finite geometry, and combinatorics.

A general upper bound is $\mu(d) \le d + 1$. Equality is known when $d$ is a prime power, via constructions over finite fields. For composite dimensions that are not prime powers, the exact value of $\mu(d)$ is in general open.

The smallest and most famous unresolved case is $d = 6$. The IQOQI OQP page emphasizes this dimension in particular: although many equivalent reformulations are known, no construction yielding more than three mutually unbiased bases in dimension six is known.

What this file formalizes

This file is organized around the quantity IsMaxMUBCount d k, which expresses that $k$ is the maximum number of mutually unbiased orthonormal bases in dimension $d$.

the open theorem mutuallyUnbiasedBases expresses the full problem for all $d \ge 2$;
the open theorem mutuallyUnbiasedBases_dim6 expresses the especially important case $d = 6$;
the solved theorem mutuallyUnbiasedBases_dim2 proves the qubit case $\mu(2) = 3$.

References

Primary source list entry:

IQOQI Vienna Open Quantum Problems, problem 13: https://oqp.iqoqi.oeaw.ac.at/mutually-unbiased-bases
Master list of open quantum problems: https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems

Foundational papers

I. D. Ivanović, Geometrical description of quantal state determination, J. Phys. A 14, 3241-3245 (1981).
W. K. Wootters and B. D. Fields, Optimal state-determination by mutually unbiased measurements, Ann. Phys. 191, 363-381 (1989).

General constructions and surveys

A. Klappenecker and M. Rötteler, Constructions of mutually unbiased bases, in Finite Fields and Applications, LNCS 2948 (2004).

Dimension six and the maximal-number problem

M. Grassl, On SIC-POVMs and MUBs in Dimension 6, arXiv:quant-ph/0406175 (2004).
P. Butterley and W. Hall, Numerical evidence for the maximum number of mutually unbiased bases in dimension six, Phys. Lett. A 369, 5-8 (2007), arXiv:quant-ph/0701122.
S. Brierley and S. Weigert, Maximal Sets of Mutually Unbiased Quantum States in Dimension Six, Phys. Rev. A 78, 042312 (2008), arXiv:0808.1614.
P. Raynal, X. Lü, and B.-G. Englert, Mutually unbiased bases in dimension six: The four most distant bases, Phys. Rev. A 83, 062303 (2011), arXiv:1103.1025.

Remark on the status of $d = 6$

The dimension-six case is not known to be solved. At present, the best-known general picture is:

$3 \le \mu(6) \le 7$,
complete sets of $7$ MUBs are not known,
and several analytic and numerical works give strong evidence that one cannot go beyond $3$.

This is why the theorem mutuallyUnbiasedBases_dim6 is marked as an open research statement.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

abbrev OpenQuantumProblem13.UMat A unitary matrix representing an orthonormal basis of $\mathbb{C}^d$ via its columns line 130 source
Source documentation
A unitary matrix representing an orthonormal basis of $\mathbb{C}^d$ via its columns.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Subtype, Matrix, Fin, Complex, Membership.mem, Submonoid, Matrix.unitaryGroup
11 instances, coercions and auxiliary constants left out.
```
abbrev UMat (d : ℕ) := ↥(Matrix.unitaryGroup (Fin d) ℂ)
```
def OpenQuantumProblem13.relativeUnitary The relative unitary between two bases line 133 source
Source documentation
The relative unitary between two bases.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem13.UMat, Matrix, Fin, Complex
Proof uses: HMul.hMul, Star.star, Membership.mem, Submonoid, Matrix.unitaryGroup
25 instances, coercions and auxiliary constants left out.
```
def relativeUnitary {d : ℕ} (U V : UMat d) : Matrix (Fin d) (Fin d) ℂ :=
…
```
Mentions: OpenQuantumProblem13.UMat
def OpenQuantumProblem13.IsUnbiased Two unitary matrices represent mutually unbiased bases if every entry of the relative unitary has squared norm $1 / d$ line 138 source
Source documentation
Two unitary matrices represent mutually unbiased bases if every entry of the relative unitary has squared norm $1 / d$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem13.UMat
Proof uses: Fin, Eq, Real, HPow.hPow, Norm.norm, Complex, OpenQuantumProblem13.relativeUnitary, OfNat.ofNat, Inv.inv
9 instances, coercions and auxiliary constants left out.
```
def IsUnbiased {d : ℕ} (U V : UMat d) : Prop :=
…
```
Mentions: OpenQuantumProblem13.UMat
lemma OpenQuantumProblem13.IsUnbiased.symm Mutual unbiasedness is symmetric line 143 source
Source documentation
Mutual unbiasedness is symmetric.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem13.UMat, OpenQuantumProblem13.IsUnbiased
Proof uses: Fin, Eq, Matrix, Complex, OpenQuantumProblem13.relativeUnitary, Star.star, of_eq_true, HMul.hMul, Membership.mem, Submonoid, Matrix.unitaryGroup, Eq.trans, True, congrArg, StarMul.star_mul, star_star, eq_self, Trans.trans, Real, HPow.hPow and 8 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma IsUnbiased.symm {d : ℕ} {U V : UMat d} (hUV : IsUnbiased U V) :
    IsUnbiased V U := by
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.IsUnbiased
def OpenQuantumProblem13.IsMUBFamily A family of unitary matrices is a family of mutually unbiased bases if every two distinct members are unbiased line 155 source
Source documentation
A family of unitary matrices is a family of mutually unbiased bases if every two distinct members are unbiased.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OpenQuantumProblem13.UMat
Proof uses: Pairwise, OpenQuantumProblem13.IsUnbiased
```
def IsMUBFamily {d k : ℕ} (B : Fin k → UMat d) : Prop :=
…
```
Mentions: OpenQuantumProblem13.UMat
def OpenQuantumProblem13.HasMUBs There exist $k$ mutually unbiased bases in $\mathbb{C}^d$ line 159 source
Source documentation
There exist $k$ mutually unbiased bases in $\mathbb{C}^d$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Fin, OpenQuantumProblem13.UMat, OpenQuantumProblem13.IsMUBFamily
```
def HasMUBs (d k : ℕ) : Prop :=
…
```
def OpenQuantumProblem13.HasCompleteMUBs There exists a complete set of $d + 1$ mutually unbiased bases in $\mathbb{C}^d$ line 163 source
Source documentation
There exists a complete set of $d + 1$ mutually unbiased bases in $\mathbb{C}^d$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: OpenQuantumProblem13.HasMUBs, HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def HasCompleteMUBs (d : ℕ) : Prop :=
…
```
def OpenQuantumProblem13.IsMaxMUBCount $k$ is the maximal size of a family of mutually unbiased bases in dimension $d$ line 167 source
Source documentation
$k$ is the maximal size of a family of mutually unbiased bases in dimension $d$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, OpenQuantumProblem13.HasMUBs, LE.le
1 instances, coercions and auxiliary constants left out.
```
def IsMaxMUBCount (d k : ℕ) : Prop :=
…
```
theorem OpenQuantumProblem13.hasMUBs_zero Every dimension admits the empty family of mutually unbiased bases line 172 source
Source documentation
Every dimension admits the empty family of mutually unbiased bases.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem13.HasMUBs, OfNat.ofNat
Proof uses: Exists.intro, Fin, OpenQuantumProblem13.UMat, OpenQuantumProblem13.IsMUBFamily, Fin.elim0, Ne, OpenQuantumProblem13.IsUnbiased
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasMUBs_zero (d : ℕ) : HasMUBs d 0 := by
…
```
Mentions: OpenQuantumProblem13.HasMUBs
theorem OpenQuantumProblem13.hasMUBs_one Every dimension admits a family of one mutually unbiased basis line 177 source
Source documentation
Every dimension admits a family of one mutually unbiased basis.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem13.HasMUBs, OfNat.ofNat
Proof uses: Exists.intro, Fin, OpenQuantumProblem13.UMat, OpenQuantumProblem13.IsMUBFamily, Matrix, Complex, Matrix.unitaryGroup, Ne, absurd, Eq, OpenQuantumProblem13.IsUnbiased, Subsingleton.elim
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasMUBs_one (d : ℕ) : HasMUBs d 1 := by
…
```
Mentions: OpenQuantumProblem13.HasMUBs
def OpenQuantumProblem13.Qubit.ω A convenient phase with squared norm $1/2$ line 183 source
Source documentation
A convenient phase with squared norm $1/2$. Using $\omega = (1+i)/2$ avoids square roots.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex
Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Complex.I
10 instances, coercions and auxiliary constants left out.
```
def ω : ℂ := (1 + Complex.I) / 2
```
def OpenQuantumProblem13.Qubit.phaseMatrix The raw phase-parametrized Hadamard matrix line 187 source
Source documentation
The raw phase-parametrized Hadamard matrix. The cases $\zeta = 1$ and $\zeta = i$ give the $X$ and $Y$ bases.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Matrix, Fin, OfNat.ofNat, Nat
Proof uses: Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Neg.neg
8 instances, coercions and auxiliary constants left out.
```
def phaseMatrix (ζ : ℂ) : Matrix (Fin 2) (Fin 2) ℂ :=
…
```
lemma OpenQuantumProblem13.Qubit.omega_norm_sq The squared norm of ω is $1/2$ line 193 source
Source documentation
The squared norm of ω is $1/2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, HPow.hPow, Nat, Norm.norm, Complex, OpenQuantumProblem13.Qubit.ω, OfNat.ofNat, Inv.inv
Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, AddMonoidHom, AddZero.mk, AddMonoid.toZero, RCLike.re, RCLike.im, id, congrArg, RCLike.norm_sq_eq_def, congrFun', congr, Eq.trans, Complex.re, HDiv.hDiv, Complex.I, Complex.div_ofNat_re, add_zero, one_div and 12 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma omega_norm_sq : ‖ω‖ ^ (2 : ℕ) = (2 : ℝ)⁻¹ := by
…
```
Mentions: OpenQuantumProblem13.Qubit.ω
lemma OpenQuantumProblem13.Qubit.conj_omega_mul_omega The product $\overline{\omega}\,\omega$ is $1/2$ line 200 source
Source documentation
The product $\overline{\omega}\,\omega$ is $1/2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Complex, HMul.hMul, Star.star, OpenQuantumProblem13.Qubit.ω, Inv.inv, OfNat.ofNat, Real, Nat
Proof uses: Trans.trans, HPow.hPow, Norm.norm, id, Complex.conj_mul', cast, Eq.symm, Eq.trans, congr, congrArg, OpenQuantumProblem13.Qubit.omega_norm_sq
51 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma conj_omega_mul_omega : star ω * ω = ((2 : ℝ)⁻¹ : ℂ) := by
…
```
Mentions: OpenQuantumProblem13.Qubit.ω
lemma OpenQuantumProblem13.Qubit.star_smul_mul_smul Taking the star of a scalar multiple on the left and multiplying by another scalar multiple collects the scalar factor as $\overline{a} a$ line 210 source
Source documentation
Taking the star of a scalar multiple on the left and multiplying by another scalar multiple collects the scalar factor as $\overline{a} a$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Matrix, Fin, OfNat.ofNat, Nat, Eq, HMul.hMul, Star.star, HSMul.hSMul
Proof uses: Matrix.ext, List, List.Mem, 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, Eq.mpr, HAdd.hAdd, RingHom, starRingEnd, id and 41 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma star_smul_mul_smul (a : ℂ) (A B : Matrix (Fin 2) (Fin 2) ℂ) :
    star (a • A) * (a • B) = (star a * a) • (star A * B) := by
…
```
lemma OpenQuantumProblem13.Qubit.star_phaseMatrix_mul_phaseMatrix The relative product of two phase matrices has the expected $2 \times 2$ form line 218 source
Source documentation
The relative product of two phase matrices has the expected $2 \times 2$ form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Matrix, Fin, OfNat.ofNat, Nat, HMul.hMul, Star.star, OpenQuantumProblem13.Qubit.phaseMatrix, Equiv, Matrix.of, Matrix.vecCons, HAdd.hAdd, HSub.hSub, Matrix.vecEmpty
Proof uses: Matrix.ext, List, List.Mem, 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, Eq.trans, RingHom, starRingEnd, True and 29 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma star_phaseMatrix_mul_phaseMatrix (ζ η : ℂ) :
    star (phaseMatrix ζ) * phaseMatrix η =
      !![1 + star ζ * η, 1 - star ζ * η;
         1 - star ζ * η, 1 + star ζ * η] := by
…
```
Mentions: OpenQuantumProblem13.Qubit.phaseMatrix
lemma OpenQuantumProblem13.Qubit.star_phaseMatrix_mul_self_of_unit_phase If $\zeta$ has unit modulus, then the phase matrix is orthogonal up to the scalar factor $2$ line 228 source
Source documentation
If $\zeta$ has unit modulus, then the phase matrix is orthogonal up to the scalar factor $2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HMul.hMul, Star.star, OfNat.ofNat, Matrix, Fin, Nat, OpenQuantumProblem13.Qubit.phaseMatrix, HSMul.hSMul
Proof uses: Eq.mpr, Equiv, Matrix.of, Matrix.vecCons, HAdd.hAdd, HSub.hSub, Matrix.vecEmpty, id, congrArg, OpenQuantumProblem13.Qubit.star_phaseMatrix_mul_phaseMatrix, Matrix.ext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons and 44 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma star_phaseMatrix_mul_self_of_unit_phase {ζ : ℂ} (hζ : star ζ * ζ = 1) :
    star (phaseMatrix ζ) * phaseMatrix ζ = (2 : ℂ) • (1 : Matrix (Fin 2) (Fin 2) ℂ) := by
…
```
Mentions: OpenQuantumProblem13.Qubit.phaseMatrix
lemma OpenQuantumProblem13.Qubit.scaled_phaseMatrix_mem_unitary Scaling a phase matrix by $\omega$ produces a unitary matrix whenever the phase has unit modulus line 236 source
Source documentation
Scaling a phase matrix by $\omega$ produces a unitary matrix whenever the phase has unit modulus.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HMul.hMul, Star.star, OfNat.ofNat, Membership.mem, Matrix, Fin, Nat, Submonoid, Matrix.unitaryGroup, HSMul.hSMul, OpenQuantumProblem13.Qubit.ω, OpenQuantumProblem13.Qubit.phaseMatrix
Proof uses: Eq.mpr, id, congrArg, propext, Matrix.mem_unitaryGroup_iff', Trans.trans, RingHom, starRingEnd, congrFun', Eq.trans, StarModule.star_smul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, Eq.mp, OpenQuantumProblem13.Qubit.star_smul_mul_smul, OpenQuantumProblem13.Qubit.star_phaseMatrix_mul_self_of_unit_phase, smul_smul, Eq.refl, Inv.inv, Real and 22 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma scaled_phaseMatrix_mem_unitary {ζ : ℂ} (hζ : star ζ * ζ = 1) :
    (ω • phaseMatrix ζ) ∈ Matrix.unitaryGroup (Fin 2) ℂ := by
…
```
Mentions: OpenQuantumProblem13.Qubit.ω, OpenQuantumProblem13.Qubit.phaseMatrix
lemma OpenQuantumProblem13.Qubit.star_phaseBasis_mul_phaseBasis The relative product of two scaled phase matrices is obtained by scaling the corresponding relative product of phase matrices line 252 source
Source documentation
The relative product of two scaled phase matrices is obtained by scaling the corresponding relative product of phase matrices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Matrix, Fin, OfNat.ofNat, Nat, HMul.hMul, Star.star, HSMul.hSMul, OpenQuantumProblem13.Qubit.ω, OpenQuantumProblem13.Qubit.phaseMatrix, Equiv, Matrix.of, Matrix.vecCons, HAdd.hAdd, HSub.hSub, Matrix.vecEmpty
Proof uses: Eq.mpr, id, congrArg, OpenQuantumProblem13.Qubit.star_smul_mul_smul, OpenQuantumProblem13.Qubit.star_phaseMatrix_mul_phaseMatrix, Eq.refl
58 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma star_phaseBasis_mul_phaseBasis (ζ η : ℂ) :
    star (ω • phaseMatrix ζ) * (ω • phaseMatrix η) =
      (star ω * ω) • !![1 + star ζ * η, 1 - star ζ * η;
                        1 - star ζ * η, 1 + star ζ * η] := by
…
```
Mentions: OpenQuantumProblem13.Qubit.ω, OpenQuantumProblem13.Qubit.phaseMatrix
def OpenQuantumProblem13.Qubit.phaseU The bundled qubit basis associated to a unit-modulus phase $\zeta$ line 259 source
Source documentation
The bundled qubit basis associated to a unit-modulus phase $\zeta$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HMul.hMul, Star.star, OfNat.ofNat, OpenQuantumProblem13.UMat, Nat
Proof uses: Subtype.mk, Matrix, Fin, Membership.mem, Submonoid, Matrix.unitaryGroup, HSMul.hSMul, OpenQuantumProblem13.Qubit.ω, OpenQuantumProblem13.Qubit.phaseMatrix, OpenQuantumProblem13.Qubit.scaled_phaseMatrix_mem_unitary
43 instances, coercions and auxiliary constants left out.
```
def phaseU (ζ : ℂ) (hζ : star ζ * ζ = 1) : UMat 2 :=
…
```
Mentions: OpenQuantumProblem13.UMat
lemma OpenQuantumProblem13.Qubit.phase_norm_sq_eq_one A complex number with $\overline{\zeta}\,\zeta = 1$ has squared norm $1$ line 264 source
Source documentation
A complex number with $\overline{\zeta}\,\zeta = 1$ has squared norm $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HMul.hMul, Star.star, OfNat.ofNat, Real, HPow.hPow, Nat, Norm.norm
Proof uses: Trans.trans, id, Eq.symm, RingHom, starRingEnd, Complex.conj_mul', cast, Eq.trans, congrArg, Nat.cast_one, congrFun'
62 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma phase_norm_sq_eq_one {ζ : ℂ} (hζ : star ζ * ζ = 1) :
    ‖ζ‖ ^ (2 : ℕ) = 1 := by
…
```
lemma OpenQuantumProblem13.Qubit.omega_mul_phase_norm_sq Multiplying $\omega$ by a unit-modulus phase preserves the squared norm $1/2$ line 275 source
Source documentation
Multiplying $\omega$ by a unit-modulus phase preserves the squared norm $1/2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HMul.hMul, Star.star, OfNat.ofNat, Real, HPow.hPow, Nat, Norm.norm, OpenQuantumProblem13.Qubit.ω, Inv.inv
Proof uses: Eq.mpr, id, congrArg, norm_mul, mul_pow, OpenQuantumProblem13.Qubit.omega_norm_sq, OpenQuantumProblem13.Qubit.phase_norm_sq_eq_one, Mathlib.Meta.NormNum.isNNRat_eq_true, Mathlib.Meta.NormNum.isNNRat_mul, Eq.refl, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_one, Nat.mul
76 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma omega_mul_phase_norm_sq {ζ : ℂ} (hζ : star ζ * ζ = 1) :
    ‖ω * ζ‖ ^ (2 : ℕ) = (2 : ℝ)⁻¹ := by
…
```
Mentions: OpenQuantumProblem13.Qubit.ω
def OpenQuantumProblem13.Qubit.ZU The standard qubit basis line 280 source
Source documentation
The standard qubit basis.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat
Proof uses: Matrix, Fin, Complex, Matrix.unitaryGroup
13 instances, coercions and auxiliary constants left out.
```
def ZU : UMat 2 := 1
```
Mentions: OpenQuantumProblem13.UMat
def OpenQuantumProblem13.Qubit.XU The qubit $X$ basis as a bundled unitary matrix line 283 source
Source documentation
The qubit $X$ basis as a bundled unitary matrix.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat
Proof uses: OpenQuantumProblem13.Qubit.phaseU, Complex
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def XU : UMat 2 := phaseU 1 (by simp)
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.Qubit.phaseU
def OpenQuantumProblem13.Qubit.YU The qubit $Y$ basis as a bundled unitary matrix line 286 source
Source documentation
The qubit $Y$ basis as a bundled unitary matrix.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat
Proof uses: OpenQuantumProblem13.Qubit.phaseU, Complex.I
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def YU : UMat 2 := phaseU Complex.I (by simp)
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.Qubit.phaseU
lemma OpenQuantumProblem13.Qubit.isUnbiased_Z_phaseU The standard basis is mutually unbiased with any phase basis of unit-modulus phase line 290 source
Source documentation
The standard basis is mutually unbiased with any phase basis of unit-modulus phase.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HMul.hMul, Star.star, OfNat.ofNat, OpenQuantumProblem13.IsUnbiased, Nat, OpenQuantumProblem13.Qubit.ZU, OpenQuantumProblem13.Qubit.phaseU
Proof uses: Fin, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, Real, HPow.hPow, Norm.norm, OpenQuantumProblem13.relativeUnitary, Inv.inv, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil and 47 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma isUnbiased_Z_phaseU (ζ : ℂ) (hζ : star ζ * ζ = 1) :
    IsUnbiased ZU (phaseU ζ hζ) := by
…
```
Mentions: OpenQuantumProblem13.IsUnbiased, OpenQuantumProblem13.Qubit.ZU, OpenQuantumProblem13.Qubit.phaseU
lemma OpenQuantumProblem13.Qubit.relative_phaseU_phaseU_of_mul_eq_I If $\overline{\zeta}\,\eta = i$, then the relative unitary between the corresponding phase bases is the qubit mutually unbiased overlap matrix line 302 source
Source documentation
If $\overline{\zeta}\,\eta = i$, then the relative unitary between the corresponding phase bases is the qubit mutually unbiased overlap matrix.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HMul.hMul, Star.star, OfNat.ofNat, Complex.I, Matrix, Fin, Nat, OpenQuantumProblem13.relativeUnitary, OpenQuantumProblem13.Qubit.phaseU, Equiv, Matrix.of, Matrix.vecCons, OpenQuantumProblem13.Qubit.ω, Matrix.vecEmpty
Proof uses: Trans.trans, HSMul.hSMul, Inv.inv, Real, HAdd.hAdd, HSub.hSub, Eq.mpr, RingHom, starRingEnd, OpenQuantumProblem13.Qubit.phaseMatrix, Neg.neg, id, congr, congrArg, Eq.trans, Membership.mem, Submonoid, Matrix.unitaryGroup, congrFun', StarModule.star_smul and 102 more
162 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma relative_phaseU_phaseU_of_mul_eq_I {ζ η : ℂ}
    (hζ : star ζ * ζ = 1) (hη : star η * η = 1) (hζη : star ζ * η = Complex.I) :
    relativeUnitary (phaseU ζ hζ) (phaseU η hη) = !![ω, star ω;
                                                      star ω, ω] := by
…
```
Mentions: OpenQuantumProblem13.relativeUnitary, OpenQuantumProblem13.Qubit.phaseU, OpenQuantumProblem13.Qubit.ω
lemma OpenQuantumProblem13.Qubit.isUnbiased_phaseU_phaseU_of_mul_eq_I If $\overline{\zeta}\,\eta = i$, then the corresponding phase bases are mutually unbiased line 326 source
Source documentation
If $\overline{\zeta}\,\eta = i$, then the corresponding phase bases are mutually unbiased.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, HMul.hMul, Star.star, OfNat.ofNat, Complex.I, OpenQuantumProblem13.IsUnbiased, Nat, OpenQuantumProblem13.Qubit.phaseU
Proof uses: Fin, Eq.mpr, Real, HPow.hPow, Norm.norm, OpenQuantumProblem13.relativeUnitary, Inv.inv, Equiv, Matrix, Matrix.of, Matrix.vecCons, OpenQuantumProblem13.Qubit.ω, Matrix.vecEmpty, id, congrArg, OpenQuantumProblem13.Qubit.relative_phaseU_phaseU_of_mul_eq_I, List, List.Mem, List.finRange, HEq and 32 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma isUnbiased_phaseU_phaseU_of_mul_eq_I {ζ η : ℂ}
    (hζ : star ζ * ζ = 1) (hη : star η * η = 1) (hζη : star ζ * η = Complex.I) :
    IsUnbiased (phaseU ζ hζ) (phaseU η hη) := by
…
```
Mentions: OpenQuantumProblem13.IsUnbiased, OpenQuantumProblem13.Qubit.phaseU
def OpenQuantumProblem13.Qubit.qubitFamily The three standard qubit mutually unbiased bases: $Z$, $X$, and $Y$ line 334 source
Source documentation
The three standard qubit mutually unbiased bases: $Z$, $X$, and $Y$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, OpenQuantumProblem13.UMat
Proof uses: Matrix.vecCons, OpenQuantumProblem13.Qubit.ZU, OpenQuantumProblem13.Qubit.XU, OpenQuantumProblem13.Qubit.YU, Matrix.vecEmpty
2 instances, coercions and auxiliary constants left out.
```
def qubitFamily : Fin 3 → UMat 2 :=
…
```
Mentions: OpenQuantumProblem13.UMat
lemma OpenQuantumProblem13.Qubit.qubitFamily_isMUB The standard qubit family is a family of mutually unbiased bases line 339 source
Source documentation
The standard qubit family is a family of mutually unbiased bases.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.IsMUBFamily, OfNat.ofNat, Nat, OpenQuantumProblem13.Qubit.qubitFamily
Proof uses: Fin, Ne, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, OpenQuantumProblem13.IsUnbiased, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, absurd, Eq.refl and 30 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma qubitFamily_isMUB : IsMUBFamily qubitFamily := by
…
```
Mentions: OpenQuantumProblem13.IsMUBFamily, OpenQuantumProblem13.Qubit.qubitFamily
lemma OpenQuantumProblem13.Qubit.qubit_hasThreeMUBs There exist three mutually unbiased bases in dimension $2$ line 358 source
Source documentation
There exist three mutually unbiased bases in dimension $2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.HasMUBs, OfNat.ofNat, Nat
Proof uses: Exists.intro, Fin, OpenQuantumProblem13.UMat, OpenQuantumProblem13.IsMUBFamily, OpenQuantumProblem13.Qubit.qubitFamily, OpenQuantumProblem13.Qubit.qubitFamily_isMUB
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma qubit_hasThreeMUBs : HasMUBs 2 3 := by
…
```
Mentions: OpenQuantumProblem13.HasMUBs
def OpenQuantumProblem13.Qubit.u0 The first entry of the first column of a qubit unitary basis matrix line 365 source
Source documentation
The first entry of the first column of a qubit unitary basis matrix.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, Complex
Proof uses: Matrix, Fin, Membership.mem, Submonoid, Matrix.unitaryGroup
16 instances, coercions and auxiliary constants left out.
```
def u0 (U : UMat 2) : ℂ :=
…
```
Mentions: OpenQuantumProblem13.UMat
def OpenQuantumProblem13.Qubit.u1 The second entry of the first column of a qubit unitary basis matrix line 370 source
Source documentation
The second entry of the first column of a qubit unitary basis matrix.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, Complex
Proof uses: Matrix, Fin, Membership.mem, Submonoid, Matrix.unitaryGroup
16 instances, coercions and auxiliary constants left out.
```
def u1 (U : UMat 2) : ℂ :=
…
```
Mentions: OpenQuantumProblem13.UMat
abbrev OpenQuantumProblem13.Qubit.BlochVec The real Bloch-vector space for qubits line 374 source
Source documentation
The real Bloch-vector space for qubits.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
```
abbrev BlochVec := EuclideanSpace ℝ (Fin 3)
…
```
def OpenQuantumProblem13.Qubit.bloch The Bloch vector associated to the first column of a qubit basis matrix line 378 source
Source documentation
The Bloch vector associated to the first column of a qubit basis matrix.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, OpenQuantumProblem13.Qubit.BlochVec
Proof uses: WithLp.toLp, ENNReal, Fin, Real, Matrix.vecCons, HMul.hMul, Complex.re, Complex, Star.star, OpenQuantumProblem13.Qubit.u0, OpenQuantumProblem13.Qubit.u1, Complex.im, HSub.hSub, MonoidWithZeroHom, Complex.normSq, Matrix.vecEmpty
28 instances, coercions and auxiliary constants left out.
```
def bloch (U : UMat 2) : BlochVec :=
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.Qubit.BlochVec
lemma OpenQuantumProblem13.Qubit.relativeUnitary_apply_zero_zero The $(0,0)$ entry of the relative unitary is the overlap of the first columns line 385 source
Source documentation
The $(0,0)$ entry of the relative unitary is the overlap of the first columns.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, Eq, Complex, OpenQuantumProblem13.relativeUnitary, Fin, HAdd.hAdd, HMul.hMul, Star.star, OpenQuantumProblem13.Qubit.u0, OpenQuantumProblem13.Qubit.u1
Proof uses: of_eq_true, RingHom, starRingEnd, Matrix, Membership.mem, Submonoid, Matrix.unitaryGroup, Eq.trans, True, congrFun', congrArg, Fin.sum_univ_two, eq_self
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma relativeUnitary_apply_zero_zero (U V : UMat 2) :
    relativeUnitary U V 0 0 = star (u0 U) * u0 V + star (u1 U) * u1 V := by
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.relativeUnitary, OpenQuantumProblem13.Qubit.u0, OpenQuantumProblem13.Qubit.u1
lemma OpenQuantumProblem13.Qubit.firstCol_normSq The first column of a unitary matrix has squared norm $1$ line 391 source
Source documentation
The first column of a unitary matrix has squared norm $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, Eq, Real, HAdd.hAdd, MonoidWithZeroHom, Complex, Complex.normSq, OpenQuantumProblem13.Qubit.u0, OpenQuantumProblem13.Qubit.u1
Proof uses: Matrix, Fin, HMul.hMul, Star.star, Membership.mem, Submonoid, Matrix.unitaryGroup, Iff.mp, Matrix.mem_unitaryGroup_iff', Subtype.property, congrArg, Eq.mpr, RingHom, starRingEnd, id, congrFun', congr, Complex.normSq_eq_conj_mul_self, Eq.mp, Fin.sum_univ_two and 5 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma firstCol_normSq (U : UMat 2) :
    Complex.normSq (u0 U) + Complex.normSq (u1 U) = 1 := by
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.Qubit.u0, OpenQuantumProblem13.Qubit.u1
lemma OpenQuantumProblem13.Qubit.re_mul_conj The real part of $z \overline{w}$ is the Euclidean dot product of the coordinate pairs of z and w line 403 source
Source documentation
The real part of $z \overline{w}$ is the Euclidean dot product of the coordinate pairs of z and w.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, Complex.re, HMul.hMul, Star.star, HAdd.hAdd, Complex.im
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, RingHom, starRingEnd, HSub.hSub, Complex.mul_re, Neg.neg, mul_neg, sub_neg_eq_add, eq_self
58 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma re_mul_conj (z w : ℂ) :
    Complex.re (z * star w) = Complex.re z * Complex.re w + Complex.im z * Complex.im w := by
…
```
lemma OpenQuantumProblem13.Qubit.bloch_inner_eq_two_normSq_sub_one The Bloch inner product is determined by the $(0,0)$ entry of the relative unitary line 410 source
Source documentation
The Bloch inner product is determined by the $(0,0)$ entry of the relative unitary.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, Eq, Real, Inner.inner, OpenQuantumProblem13.Qubit.BlochVec, ENNReal, Fin, OpenQuantumProblem13.Qubit.bloch, HSub.hSub, HMul.hMul, MonoidWithZeroHom, Complex, Complex.normSq, OpenQuantumProblem13.relativeUnitary
Proof uses: OpenQuantumProblem13.Qubit.u0, OpenQuantumProblem13.Qubit.u1, HAdd.hAdd, id, OpenQuantumProblem13.Qubit.firstCol_normSq, Complex.re, Star.star, Eq.mpr, RingHom, starRingEnd, Complex.im, Neg.neg, congr, congrArg, OpenQuantumProblem13.Qubit.relativeUnitary_apply_zero_zero, Eq.trans, mul_assoc, Complex.mul_re, mul_neg, sub_neg_eq_add and 109 more
189 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma bloch_inner_eq_two_normSq_sub_one (U V : UMat 2) :
    inner ℝ (bloch U) (bloch V) = 2 * Complex.normSq (relativeUnitary U V 0 0) - 1 := by
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.Qubit.bloch, OpenQuantumProblem13.relativeUnitary
lemma OpenQuantumProblem13.Qubit.relativeUnitary_self The relative unitary of a basis with itself is the identity matrix line 453 source
Source documentation
The relative unitary of a basis with itself is the identity matrix.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, Eq, Matrix, Fin, Complex, OpenQuantumProblem13.relativeUnitary
Proof uses: Eq.mpr, HMul.hMul, Star.star, Membership.mem, Submonoid, Matrix.unitaryGroup, id, congrArg, OpenQuantumProblem13.relativeUnitary.eq_1, Matrix.UnitaryGroup.star_mul_self
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma relativeUnitary_self (U : UMat 2) : relativeUnitary U U = 1 := by
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.relativeUnitary
lemma OpenQuantumProblem13.Qubit.bloch_inner_self Every qubit Bloch vector has squared Euclidean norm $1$ line 459 source
Source documentation
Every qubit Bloch vector has squared Euclidean norm $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, Eq, Real, Inner.inner, OpenQuantumProblem13.Qubit.BlochVec, ENNReal, Fin, OpenQuantumProblem13.Qubit.bloch
Proof uses: Eq.mpr, HSub.hSub, HMul.hMul, MonoidWithZeroHom, Complex, Complex.normSq, OpenQuantumProblem13.relativeUnitary, id, congrArg, OpenQuantumProblem13.Qubit.bloch_inner_eq_two_normSq_sub_one, Matrix, OpenQuantumProblem13.Qubit.relativeUnitary_self, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAddMonoidWithOne, congrFun', Matrix.one_apply_eq, map_one, mul_one and 13 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma bloch_inner_self (U : UMat 2) : inner ℝ (bloch U) (bloch U) = 1 := by
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.Qubit.bloch
lemma OpenQuantumProblem13.Qubit.bloch_ne_zero A qubit Bloch vector is never the zero vector line 465 source
Source documentation
A qubit Bloch vector is never the zero vector.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, Ne, OpenQuantumProblem13.Qubit.BlochVec, OpenQuantumProblem13.Qubit.bloch, ENNReal, Fin, Real
Proof uses: Eq, Eq.mpr, False, id, False.elim, Eq.mp, Inner.inner, Eq.trans, congrArg, HPow.hPow, Norm.norm, congr, inner_self_eq_norm_sq_to_K, congrFun', norm_zero, Real.ringHom_apply, RingHom, Algebra.algebraMap, zero_pow, of_eq_true and 13 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma bloch_ne_zero (U : UMat 2) : bloch U ≠ 0 := by
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.Qubit.bloch
lemma OpenQuantumProblem13.Qubit.bloch_inner_eq_zero_of_isUnbiased Mutually unbiased qubit bases have orthogonal Bloch vectors line 473 source
Source documentation
Mutually unbiased qubit bases have orthogonal Bloch vectors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.UMat, OfNat.ofNat, Nat, OpenQuantumProblem13.IsUnbiased, Eq, Real, Inner.inner, OpenQuantumProblem13.Qubit.BlochVec, ENNReal, Fin, OpenQuantumProblem13.Qubit.bloch
Proof uses: Eq.mpr, HSub.hSub, HMul.hMul, MonoidWithZeroHom, Complex, Complex.normSq, OpenQuantumProblem13.relativeUnitary, id, congrArg, OpenQuantumProblem13.Qubit.bloch_inner_eq_two_normSq_sub_one, Inv.inv, Trans.trans, HPow.hPow, Norm.norm, RCLike.normSq_eq_def', Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_sub, Int.ofNat and 12 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma bloch_inner_eq_zero_of_isUnbiased {U V : UMat 2} (hUV : IsUnbiased U V) :
    inner ℝ (bloch U) (bloch V) = 0 := by
…
```
Mentions: OpenQuantumProblem13.UMat, OpenQuantumProblem13.IsUnbiased, OpenQuantumProblem13.Qubit.bloch
lemma OpenQuantumProblem13.Qubit.qubit_upper_bound No family of mutually unbiased bases in dimension $2$ has size greater than $3$ line 487 source
Source documentation
No family of mutually unbiased bases in dimension $2$ has size greater than $3$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem13.HasMUBs, OfNat.ofNat, LE.le
Proof uses: Fin, OpenQuantumProblem13.UMat, OpenQuantumProblem13.IsMUBFamily, OpenQuantumProblem13.Qubit.BlochVec, OpenQuantumProblem13.Qubit.bloch, Ne, ENNReal, Real, id, OpenQuantumProblem13.Qubit.bloch_ne_zero, Pairwise, Eq, Inner.inner, OpenQuantumProblem13.Qubit.bloch_inner_eq_zero_of_isUnbiased, LinearIndependent, linearIndependent_of_ne_zero_of_inner_eq_zero, Fintype.card, Module.finrank, LinearIndependent.fintype_card_le_finrank, Eq.mpr and 7 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma qubit_upper_bound (m : ℕ) : HasMUBs 2 m → m ≤ 3 := by
…
```
Mentions: OpenQuantumProblem13.HasMUBs
theorem OpenQuantumProblem13.Qubit.qubit_maximal The maximum number of mutually unbiased bases in dimension $2$ is $3$ line 504 source
Source documentation
The maximum number of mutually unbiased bases in dimension $2$ is $3$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.IsMaxMUBCount, OfNat.ofNat, Nat
Proof uses: And.intro, OpenQuantumProblem13.HasMUBs, LE.le, OpenQuantumProblem13.Qubit.qubit_hasThreeMUBs, OpenQuantumProblem13.Qubit.qubit_upper_bound
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem qubit_maximal : IsMaxMUBCount 2 3 := by
…
```
Mentions: OpenQuantumProblem13.IsMaxMUBCount
theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim2 In dimension $2$, the maximum number of mutually unbiased orthonormal bases is $3$ line 513 source
Source documentation
In dimension $2$, the maximum number of mutually unbiased orthonormal bases is $3$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem13.IsMaxMUBCount, OfNat.ofNat, Nat
Proof uses: OpenQuantumProblem13.Qubit.qubit_maximal
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem mutuallyUnbiasedBases_dim2 : IsMaxMUBCount 2 3 := by
…
```
Mentions: OpenQuantumProblem13.IsMaxMUBCount
theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim6_bounds sorry line 520 source
depends on sorry what this means
Statement uses: And, OpenQuantumProblem13.HasMUBs, OfNat.ofNat, Nat, LE.le
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 OpenQuantumProblem13.mutuallyUnbiasedBases_dim6 Special case in dimension $6$: determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^6$ sorry line 529 source
Source documentation
Special case in dimension $6$: determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^6$.

depends on sorry what this means
Statement uses: OpenQuantumProblem13.IsMaxMUBCount, OfNat.ofNat, Nat, sorryAx, Bool.false
Proof uses: Lean.Name, 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 mutuallyUnbiasedBases_dim6 :
    IsMaxMUBCount 6 (answer(sorry)) := by
…
```
Mentions: OpenQuantumProblem13.IsMaxMUBCount
theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim10 Special case in dimension $10$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^{10}$ sorry line 536 source
Source documentation
Special case in dimension $10$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^{10}$.

depends on sorry what this means
Statement uses: OpenQuantumProblem13.IsMaxMUBCount, OfNat.ofNat, Nat, sorryAx, Bool.false
Proof uses: Lean.Name, 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 mutuallyUnbiasedBases_dim10 :
    IsMaxMUBCount 10 (answer(sorry)) := by
…
```
Mentions: OpenQuantumProblem13.IsMaxMUBCount
theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim12 Special case in dimension $12$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^{12}$ sorry line 543 source
Source documentation
Special case in dimension $12$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^{12}$.

depends on sorry what this means
Statement uses: OpenQuantumProblem13.IsMaxMUBCount, OfNat.ofNat, Nat, sorryAx, Bool.false
Proof uses: Lean.Name, 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 mutuallyUnbiasedBases_dim12 :
    IsMaxMUBCount 12 (answer(sorry)) := by
…
```
Mentions: OpenQuantumProblem13.IsMaxMUBCount
theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim14 Special case in dimension $14$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^{14}$ sorry line 550 source
Source documentation
Special case in dimension $14$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^{14}$.

depends on sorry what this means
Statement uses: OpenQuantumProblem13.IsMaxMUBCount, OfNat.ofNat, Nat, sorryAx, Bool.false
Proof uses: Lean.Name, 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 mutuallyUnbiasedBases_dim14 :
    IsMaxMUBCount 14 (answer(sorry)) := by
…
```
Mentions: OpenQuantumProblem13.IsMaxMUBCount
theorem OpenQuantumProblem13.mutuallyUnbiasedBases_dim15 Special case in dimension $15$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^{15}$ sorry line 557 source
Source documentation
Special case in dimension $15$ (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^{15}$.

depends on sorry what this means
Statement uses: OpenQuantumProblem13.IsMaxMUBCount, OfNat.ofNat, Nat, sorryAx, Bool.false
Proof uses: Lean.Name, 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 mutuallyUnbiasedBases_dim15 :
    IsMaxMUBCount 15 (answer(sorry)) := by
…
```
Mentions: OpenQuantumProblem13.IsMaxMUBCount
theorem OpenQuantumProblem13.mutuallyUnbiasedBases Open Quantum Problem 13: determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^d$ for $d \ge 2$ sorry line 564 source
Source documentation
Open Quantum Problem 13: determine the maximal number of mutually unbiased orthonormal bases in $\mathbb{C}^d$ for $d \ge 2$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem13.IsMaxMUBCount, sorryAx, Bool.false
Proof uses: Lean.Name, 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 mutuallyUnbiasedBases (d : ℕ) (hd : 2 ≤ d) :
    IsMaxMUBCount d ((answer(sorry) : ℕ → ℕ) d) := by
…
```
Mentions: OpenQuantumProblem13.IsMaxMUBCount