A summed commutator forces diagonal relative unitaries

Open

QAlgorithms.Papers.Independent.Intakethird100.P96.diagonal_relative_unitaries

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $d\ge2$ and let $U_1,\ldots,U_d$ and $V_1,\ldots,V_d$ be unitary matrices on $\mathbb C^d$ . In its fixed standard orthonormal basis write $P_\mu=|\mu\rangle\langle\mu|$ . Suppose that for every pair $A,B\in M_d(\mathbb C)$ ,

\sum_{\mu,\nu}[U_\mu^*AU_\mu\otimes P_\mu,\;P_\nu\otimes V_\nu^*BV_\nu]=0.

There are unitary matrices $U,V$ , chosen independently of the family index, such that

U^*U_\mu\text{ and }V^*V_\mu\text{ are diagonal for every }\mu.

The condition is on the entire sum of commutators. The conclusion provides a common reference unitary for each family.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P96

Formal statement

noncomputable section

open scoped TensorProduct Kronecker BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P96

open QAlgorithms.Papers.Independent.Information100.P26 (Mat)

/-- Lemma 9, PDF p.11. The hypothesis is the sum of commutators in (30). -/
theorem diagonal_relative_unitaries (d : ℕ) (hd : 2 ≤ d)
    (U V : Fin d → Matrix.unitaryGroup (Fin d) ℂ)
    (hcomm : ∀ A B : Mat d,
      (∑ i : Fin d, ∑ j : Fin d,
        (((star (U i : Mat d) * A * (U i : Mat d)) ⊗ₖ coordinateProjection i) *
            (coordinateProjection j ⊗ₖ (star (V j : Mat d) * B * (V j : Mat d))) -
          (coordinateProjection j ⊗ₖ (star (V j : Mat d) * B * (V j : Mat d))) *
            ((star (U i : Mat d) * A * (U i : Mat d)) ⊗ₖ coordinateProjection i))) = 0) :
    ∃ Ubase Vbase : Matrix.unitaryGroup (Fin d) ℂ,
      ∀ k : Fin d, ∀ i j : Fin d, i ≠ j →
        (star (Ubase : Mat d) * (U k : Mat d)) i j = 0 ∧
        (star (Vbase : Mat d) * (V k : Mat d)) i j = 0 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P96

end

Source

Reversible quantum cellular automata, arXiv:quant-ph/0405174v1, PDF p. 11, Lemma 9: diagonal relative unitaries

Read-back

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

For every natural number $d\ge2$ , let $(U_i)_{i=0}^{d-1}$ and $(V_i)_{i=0}^{d-1}$ be families of unitary complex $d\times d$ matrices. Write $E_i$ for the matrix with a single $1$ in diagonal position $(i,i)$ and zeros elsewhere, $^{*}$ for conjugate transpose, and $\otimes$ for the matrix Kronecker product. Suppose that for every pair of complex $d\times d$ matrices $A,B$ ,

\sum_{i=0}^{d-1}\sum_{j=0}^{d-1} \left[ (U_i^{*}AU_i\otimes E_i)(E_j\otimes V_j^{*}BV_j) -(E_j\otimes V_j^{*}BV_j)(U_i^{*}AU_i\otimes E_i) \right]=0.

Then there exist unitary complex $d\times d$ matrices $U_{\mathrm{base}},V_{\mathrm{base}}$ such that for every $k\in\{0,\ldots,d-1\}$ and every distinct pair $i,j$ of indices, both $(U_{\mathrm{base}}^{*}U_k)_{ij}=0$ and $(V_{\mathrm{base}}^{*}V_k)_{ij}=0$ ; thus all these relative matrices are diagonal.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph