feat(OpenQuantumProblems): Formalization of open quantum problem 13

[MarioKrenn6240]

Summary

This PR adds a formalization of Open Quantum Problem 13 from the IQOQI Vienna Open Quantum Problems list: mutually unbiased bases.

Mathematical content

For each integer d ≥ 2, the problem asks for the maximal number μ(d) of orthonormal bases of ℂ^d that are pairwise mutually unbiased.

In the formalization, 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 = U† V contains the cross-basis overlaps, and mutual unbiasedness is expressed via the equivalent squared-norm condition

‖(relativeUnitary U V) i j‖^2 = 1 / d.

What is introduced

The file defines:

• IsUnbiased for two orthonormal bases,
• IsMUBFamily for pairwise mutually unbiased families,
• HasMUBs d k for existence of k mutually unbiased bases in dimension d,
• IsMaxMUBCount d k for the statement that k is the maximal number of MUBs in dimension d.

Included results

The PR includes:

• the open theorem mutuallyUnbiasedBases, expressing the full problem for arbitrary d ≥ 2,
• the open theorem mutuallyUnbiasedBases_dim6, expressing the especially important and famous unresolved case d = 6,
• the solved theorem mutuallyUnbiasedBases_dim2, proving the qubit case μ(2) = 3.

The dimension-2 result is proved using the standard Z, X, and Y qubit bases together with a Bloch-vector argument giving the upper bound.

Background

A general upper bound is μ(d) ≤ d + 1, with equality known for prime-power dimensions.
For non-prime-power composite dimensions, the exact value is in general open. The smallest and most famous unresolved case is d = 6.

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 references included in the docstring:

• I. D. Ivanović, Geometrical description of quantal state determination, Journal of Physics A: Mathematical and General 14 (1981), 3241–3245.
• W. K. Wootters and B. D. Fields, Optimal state-determination by mutually unbiased measurements, Annals of Physics 191 (1989), 363–381.

Closes #3419.

Assisted by GPT Pro 5.4.

[mo271]

Thanks!
This formalisation looks great to me. I didn't find any bugs in the math apart from a little misunderstanding of how our answer(sorry) works!
Just a few other nits

[mo271]

Suggested change

	import Mathlib.Analysis.Complex.Basic
	import Mathlib.Analysis.InnerProductSpace.PiL2
	import Mathlib.LinearAlgebra.Matrix.Notation
	import Mathlib.LinearAlgebra.UnitaryGroup

Those are imported by ProblemImports anyhow

[mo271]

Suggested change

	@[category API, AMS 05 15 81 94]
	@[category API, AMS 5 15 81 94]

throughout

[mo271]

Suggested change

	/-- Any dimension admits a vacuous MUB family of size 0. -/
	@[category test, AMS 5 15 81 94]
	theorem hasMUBs_zero (d : ℕ) : HasMUBs d 0 := by
	exact ⟨Fin.elim0, fun i => i.elim0⟩
	/-- Any dimension admits a trivial MUB family of size 1 (a single basis). -/
	@[category test, AMS 5 15 81 94]
	theorem hasMUBs_one (d : ℕ) : HasMUBs d 1 := by
	exact ⟨fun _ => 1, fun {i j} hij => absurd (Subsingleton.elim i j) hij⟩

Perhaps those are useful test statements?

[mo271]

This statement is trivially false as formalized, because answer(sorry) is a single
fixed ℕ that does not depend on d. Since μ(2) = 3 and μ(3) ≥ 4, no single k works
for all d:

theorem mutuallyUnbiasedBases_disprovable (k : ℕ) :
    ¬ (∀ d, 2 ≤ d → IsMaxMUBCount d k) := by
  intro hk
  -- From d=2: k must equal 3 (fully proved qubit case)
  have h2 := hk 2 (by omega)
  have hk_ge : 3 ≤ k := h2.2 3 Qubit.qubit_hasThreeMUBs
  have hk_le : k ≤ 3 := Qubit.qubit_upper_bound k h2.1
  -- From d=3 with k=3: 4 ≤ 3, contradiction
  have hk3 : k = 3 := by omega
  subst hk3
  exact absurd ((hk 3 (by omega)).2 4 hasMUBs_dim3_four) (by omega)

One way get a around is is to define an answer(sorry) that is actually a function:

@[category research open, AMS 5 15 81 94]
theorem mutuallyUnbiasedBases' (d : ℕ) (hd : 2 ≤ d) :
    let count : ℕ → ℕ := answer(sorry)
    IsMaxMUBCount d (count d) := by
  sorry

one can of course also inline this with letI or directly writing

    IsMaxMUBCount d ((answer(sorry) : ℕ → ℕ) d) := by

[mo271]

Suggested change

	/-- The standard basis. -/
	def ZU : UMat 2 := 1
	/-- The `X` basis as a bundled unitary matrix. -/
	def XU : UMat 2 := phaseU 1 (by simp)
	/-- The `Y` basis as a bundled unitary matrix. -/
	def YU : UMat 2 := phaseU Complex.I (by simp)
	/-- The standard basis. -/
	def zU : UMat 2 := 1
	/-- The `X` basis as a bundled unitary matrix. -/
	def zU : UMat 2 := phaseU 1 (by simp)
	/-- The `Y` basis as a bundled unitary matrix. -/
	def yU : UMat 2 := phaseU Complex.I (by simp)

that would be the naming convention, I think, but if it is really unusual, I'd say it is ok to stick closer with what is in the literature...

[mo271]

I'd be nicer to look at in the rendered documentation (website) if all the docstrings were using latex markdown instead of backtics

[mo271]

FormalConjectures/OpenQuantumProblems/13.lean‎ should be the filename here, let's not mention oqp twice..