Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Problem 16 definitions — Existence of complete sets of mutually unbiased bases

Definition
rybin2026_p16_mutually_unbiased_bases

by wenxinzhang · Sep 1, 2026 · Mathlib c5ea003 (Lean v4.30.0)

finite-fieldshilbert-spacesmutually-unbiased-basesquantum-foundationsquantum-information-theory

For any 6×66\times66×6 complex matrix U=(Uki)U=(U_{ki})U=(Uki​), with k,i∈{0,…,5}k,i\in\{0,\ldots,5\}k,i∈{0,…,5}, IsOrthonormalBasis6⁡(U)\operatorname{IsOrthonormalBasis6}(U)IsOrthonormalBasis6(U) is the proposition U∗U=I6U^{*}U=I_6U∗U=I6​, where U∗U^{*}U∗ is the conjugate transpose and I6I_6I6​ is the 6×66\times66×6 identity matrix. Entrywise, this requires, for every i,j∈{0,…,5}i,j\in\{0,\ldots,5\}i,j∈{0,…,5}, ∑k=05Uki‾ Ukj=1\sum_{k=0}^{5}\overline{U_{ki}}\,U_{kj}=1∑k=05​Uki​​Ukj​=1 when i=ji=ji=j, and ∑k=05Uki‾ Ukj=0\sum_{k=0}^{5}\overline{U_{ki}}\,U_{kj}=0∑k=05​Uki​​Ukj​=0 when i≠ji\ne ji=j. Thus all thirty-six entrywise equalities are required, and every sum has exactly six terms; there is no empty-index or zero-dimensional case. The definition contains no separately stated condition UU∗=I6UU^{*}=I_6UU∗=I6​, invertibility condition, or spanning condition, and it defines a property of UUU without asserting that any such matrix exists.

For any two 6×66\times66×6 complex matrices U=(Uki)U=(U_{ki})U=(Uki​) and V=(Vkj)V=(V_{kj})V=(Vkj​), MutuallyUnbiased6⁡(U,V)\operatorname{MutuallyUnbiased6}(U,V)MutuallyUnbiased6(U,V) is the proposition that, for every i,j∈{0,…,5}i,j\in\{0,\ldots,5\}i,j∈{0,…,5}, the squared complex modulus of the (i,j)(i,j)(i,j)-entry of U∗VU^{*}VU∗V is exactly 1/61/61/6; explicitly, ∣∑k=05Uki‾ Vkj∣2=1/6\left|\sum_{k=0}^{5}\overline{U_{ki}}\,V_{kj}\right|^{2}=1/6​∑k=05​Uki​​Vkj​​2=1/6. Here the squared modulus of a complex number zzz means (Re⁡z)2+(Im⁡z)2(\operatorname{Re}z)^2+(\operatorname{Im}z)^2(Rez)2+(Imz)2, with no square root. All thirty-six choices of i,ji,ji,j are included, each sum has six terms, and the denominator is the fixed nonzero real number 666. No hypothesis in this definition requires either UUU or VVV to satisfy IsOrthonormalBasis6⁡\operatorname{IsOrthonormalBasis6}IsOrthonormalBasis6, so this predicate is defined for arbitrary pairs of 6×66\times66×6 complex matrices; it defines a property and makes no existence assertion.

For any function BBB assigning a 6×66\times66×6 complex matrix BrB_rBr​ to each label r∈{0,…,6}r\in\{0,\ldots,6\}r∈{0,…,6}, IsCompleteMUB6⁡(B)\operatorname{IsCompleteMUB6}(B)IsCompleteMUB6(B) is the conjunction of the following two requirements. First, for every r∈{0,…,6}r\in\{0,\ldots,6\}r∈{0,…,6}, (Br)∗Br=I6(B_r)^{*}B_r=I_6(Br​)∗Br​=I6​, meaning that for every i,j∈{0,…,5}i,j\in\{0,\ldots,5\}i,j∈{0,…,5}, ∑k=05(Br)ki‾ (Br)kj\sum_{k=0}^{5}\overline{(B_r)_{ki}}\,(B_r)_{kj}∑k=05​(Br​)ki​​(Br​)kj​ equals 111 if i=ji=ji=j and 000 if i≠ji\ne ji=j. Second, for every ordered pair r,s∈{0,…,6}r,s\in\{0,\ldots,6\}r,s∈{0,…,6}, if r≠sr\ne sr=s, then for every i,j∈{0,…,5}i,j\in\{0,\ldots,5\}i,j∈{0,…,5}, ∣∑k=05(Br)ki‾ (Bs)kj∣2=1/6\left|\sum_{k=0}^{5}\overline{(B_r)_{ki}}\,(B_s)_{kj}\right|^{2}=1/6​∑k=05​(Br​)ki​​(Bs​)kj​​2=1/6. The second requirement therefore covers all forty-two ordered pairs of unequal labels, equivalently each of the twenty-one unordered pairs in both orders. When r=sr=sr=s, its implication has a false antecedent and imposes no transition-amplitude condition, although the first requirement still applies to BrB_rBr​. The function BBB is not explicitly required to be injective or its matrices explicitly required to be distinct beyond what the displayed conditions entail. The declaration merely defines this property of a seven-indexed family: it does not assert that such a family exists, quantify over an eighth matrix, exclude extension by additional matrices, or state any maximality property.

Definition code
import Mathlib

open Matrix
open scoped ComplexConjugate Matrix

namespace RybinAI2026.P16

/-- A matrix whose columns form an orthonormal basis of `ℂ⁶`. -/
def IsOrthonormalBasis6 (U : Matrix (Fin 6) (Fin 6) ℂ) : Prop :=
  Uᴴ * U = 1

/-- Two column-orthonormal matrices are mutually unbiased when every transition amplitude has
squared modulus `1/6`. -/
def MutuallyUnbiased6
    (U V : Matrix (Fin 6) (Fin 6) ℂ) : Prop :=
  ∀ i j, Complex.normSq ((Uᴴ * V) i j) = (1 : ℝ) / 6

/-- Seven pairwise mutually unbiased orthonormal bases, the complete number in dimension six. -/
def IsCompleteMUB6 (B : Fin 7 → Matrix (Fin 6) (Fin 6) ℂ) : Prop :=
  (∀ r, IsOrthonormalBasis6 (B r)) ∧
    ∀ r s, r ≠ s → MutuallyUnbiased6 (B r) (B s)

end RybinAI2026.P16
Source
https://rybindmitry.github.io/problems/16.html
Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

For any 6×66\times66×6 complex matrix U=(Uki)U=(U_{ki})U=(Uki​), with k,i∈{0,…,5}k,i\in\{0,\ldots,5\}k,i∈{0,…,5}, IsOrthonormalBasis6⁡(U)\operatorname{IsOrthonormalBasis6}(U)IsOrthonormalBasis6(U) is the proposition U∗U=I6U^{*}U=I_6U∗U=I6​, where U∗U^{*}U∗ is the conjugate transpose and I6I_6I6​ is the 6×66\times66×6 identity matrix. Entrywise, this requires, for every i,j∈{0,…,5}i,j\in\{0,\ldots,5\}i,j∈{0,…,5}, ∑k=05Uki‾ Ukj=1\sum_{k=0}^{5}\overline{U_{ki}}\,U_{kj}=1∑k=05​Uki​​Ukj​=1 when i=ji=ji=j, and ∑k=05Uki‾ Ukj=0\sum_{k=0}^{5}\overline{U_{ki}}\,U_{kj}=0∑k=05​Uki​​Ukj​=0 when i≠ji\ne ji=j. Thus all thirty-six entrywise equalities are required, and every sum has exactly six terms; there is no empty-index or zero-dimensional case. The definition contains no separately stated condition UU∗=I6UU^{*}=I_6UU∗=I6​, invertibility condition, or spanning condition, and it defines a property of UUU without asserting that any such matrix exists.

For any two 6×66\times66×6 complex matrices U=(Uki)U=(U_{ki})U=(Uki​) and V=(Vkj)V=(V_{kj})V=(Vkj​), MutuallyUnbiased6⁡(U,V)\operatorname{MutuallyUnbiased6}(U,V)MutuallyUnbiased6(U,V) is the proposition that, for every i,j∈{0,…,5}i,j\in\{0,\ldots,5\}i,j∈{0,…,5}, the squared complex modulus of the (i,j)(i,j)(i,j)-entry of U∗VU^{*}VU∗V is exactly 1/61/61/6; explicitly, ∣∑k=05Uki‾ Vkj∣2=1/6\left|\sum_{k=0}^{5}\overline{U_{ki}}\,V_{kj}\right|^{2}=1/6​∑k=05​Uki​​Vkj​​2=1/6. Here the squared modulus of a complex number zzz means (Re⁡z)2+(Im⁡z)2(\operatorname{Re}z)^2+(\operatorname{Im}z)^2(Rez)2+(Imz)2, with no square root. All thirty-six choices of i,ji,ji,j are included, each sum has six terms, and the denominator is the fixed nonzero real number 666. No hypothesis in this definition requires either UUU or VVV to satisfy IsOrthonormalBasis6⁡\operatorname{IsOrthonormalBasis6}IsOrthonormalBasis6, so this predicate is defined for arbitrary pairs of 6×66\times66×6 complex matrices; it defines a property and makes no existence assertion.

For any function BBB assigning a 6×66\times66×6 complex matrix BrB_rBr​ to each label r∈{0,…,6}r\in\{0,\ldots,6\}r∈{0,…,6}, IsCompleteMUB6⁡(B)\operatorname{IsCompleteMUB6}(B)IsCompleteMUB6(B) is the conjunction of the following two requirements. First, for every r∈{0,…,6}r\in\{0,\ldots,6\}r∈{0,…,6}, (Br)∗Br=I6(B_r)^{*}B_r=I_6(Br​)∗Br​=I6​, meaning that for every i,j∈{0,…,5}i,j\in\{0,\ldots,5\}i,j∈{0,…,5}, ∑k=05(Br)ki‾ (Br)kj\sum_{k=0}^{5}\overline{(B_r)_{ki}}\,(B_r)_{kj}∑k=05​(Br​)ki​​(Br​)kj​ equals 111 if i=ji=ji=j and 000 if i≠ji\ne ji=j. Second, for every ordered pair r,s∈{0,…,6}r,s\in\{0,\ldots,6\}r,s∈{0,…,6}, if r≠sr\ne sr=s, then for every i,j∈{0,…,5}i,j\in\{0,\ldots,5\}i,j∈{0,…,5}, ∣∑k=05(Br)ki‾ (Bs)kj∣2=1/6\left|\sum_{k=0}^{5}\overline{(B_r)_{ki}}\,(B_s)_{kj}\right|^{2}=1/6​∑k=05​(Br​)ki​​(Bs​)kj​​2=1/6. The second requirement therefore covers all forty-two ordered pairs of unequal labels, equivalently each of the twenty-one unordered pairs in both orders. When r=sr=sr=s, its implication has a false antecedent and imposes no transition-amplitude condition, although the first requirement still applies to BrB_rBr​. The function BBB is not explicitly required to be injective or its matrices explicitly required to be distinct beyond what the displayed conditions entail. The declaration merely defines this property of a seven-indexed family: it does not assert that such a family exists, quantify over an eighth matrix, exclude extension by additional matrices, or state any maximality property.

Human review
  • Endorsed by Shuze Chen · Sep 1, 2026

  • Endorsed by wenxinzhang · Sep 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me