Output-first Choi covariance

Proved

QAlgorithms.Papers.Independent.Intake100.P12.choi_covariance

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $d\ge1$ and $U,A,B\in U(d)$ , in the fixed computational bases. Write $C(V)$ for the unnormalized, output-first Choi matrix of the channel $X\mapsto VXV^\dagger$ . Then

(A\otimes B)C(U)(A^\dagger\otimes B^\dagger)=C(AUB^{\mathsf T}).

The transpose on $B$ records the input leg convention of the Choi representation.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P12

Formal statement

noncomputable section

open QAlgorithms

open scoped Matrix ComplexConjugate ComplexOrder Kronecker

namespace QAlgorithms.Papers.Independent.Intake100.P12

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Information100.P21 (Op)

open QAlgorithms.Papers.Independent.Dependency50.P26 (ChannelChoi)

/-- PDF p.2, Eq. (3): unitary-channel Choi covariance, with B transposed. -/
theorem choi_covariance {d : ℕ} (hd : 0 < d)
    (U A B : Matrix.unitaryGroup (Fin d) ℂ) :
    ((A : Op (Fin d)) ⊗ₖ (B : Op (Fin d))) * gateChoi (U : Op (Fin d)) *
      (((A : Op (Fin d)) ⊗ₖ (B : Op (Fin d)))ᴴ) =
    gateChoi ((A : Op (Fin d)) * (U : Op (Fin d)) * (B : Op (Fin d)).transpose) := by sorry

end QAlgorithms.Papers.Independent.Intake100.P12

end

Source

Probabilistic exact universal quantum circuits for transforming unitary operations, arXiv:1909.01366v2, PDF p. 2, II A, Eq. (3)

Read-back

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

For every positive natural number $d$ and every three $d\times d$ unitary matrices $U,A,B$ , define $H(V)$ , for any $d\times d$ complex matrix $V$ , by

H(V)_{(a,i),(b,j)}=V_{ai}\overline{V_{bj}}.

Then

(A\otimes B)\,H(U)\,(A\otimes B)^\dagger = H( AUB^{\mathsf T}).

Here the tensor product is the Kronecker product, $\dagger$ denotes conjugate transpose, and $B^{\mathsf T}$ is the ordinary transpose. The matrices $H(V)$ in this statement have exactly the displayed entries, without a dimension-dependent normalization factor.

Human review

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

View graph