Prove2Me

Sec. II.E: commuting Kraus matrices reduce Bob's term to tr(Eμ ⋅)\mathrm{tr}(E_\mu\,\cdot)

Proved
PeresTerno.commuting_kraus_sum_eq_trace_povm

by Lucas · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

quantum-information

Let {Am}m∈I\{A_m\}_{m\in I} and {Bn}n∈J\{B_n\}_{n\in J} be finite families of complex d×dd\times d matrices with AmBn=BnAmA_m B_n = B_n A_m for all m,nm,n, and let ρ\rho be any d×dd\times d matrix. Then

tr⁡(∑m∈I∑n∈JBnAm ρ Am†Bn†)=tr⁡(E∑n∈JBn ρ Bn†),E=∑m∈IAm†Am.\operatorname{tr}\Big(\sum_{m\in I}\sum_{n\in J} B_n A_m\,\rho\,A_m^\dagger B_n^\dagger\Big) = \operatorname{tr}\Big(E \sum_{n\in J} B_n\,\rho\,B_n^\dagger\Big),\qquad E = \sum_{m\in I}A_m^\dagger A_m .

This is the step in the source's derivation of Eq. (11): using Eq. (9) to exchange AμmA_{\mu m} and BνnB_{\nu n} (and their adjoints) and moving AμmA_{\mu m} cyclically, one obtains "expressions like Eq. (8)".

Preamble
import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

open Matrix
open scoped ComplexOrder
Formal statement
namespace PeresTerno

theorem commuting_kraus_sum_eq_trace_povm {d ι κ : Type*} [Fintype d] [Fintype ι] [Fintype κ]
    (A : ι → Matrix d d ℂ) (B : κ → Matrix d d ℂ)
    (hAB : ∀ m n, Commute (A m) (B n)) (ρ : Matrix d d ℂ) :
    trace (∑ m, ∑ n, B n * A m * ρ * (A m)ᴴ * (B n)ᴴ)
      = trace (povmElement A * ∑ n, B n * ρ * (B n)ᴴ) := by
  sorry

end PeresTerno
Source
A. Peres and D. R. Terno, Quantum information and relativity theory, Rev. Mod. Phys. 76, 93-123 (2004), https://doi.org/10.1103/RevModPhys.76.93, pp. 100-101, Sec. II.E, step from Eq. (10) to Eq. (11)
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - NON-BLIND: same agent that drafted the statements

Non-blind read-back - not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning, at the explicit request of the proposal owner. It was not produced by a blind, independent auditor and must not be mistaken for independent testimony. Reviewers should compare the Lean code against the source themselves.

For finite index types dd, II, JJ, every pair of families A:I→Cd×dA : I\to\mathbb C^{d\times d}, B:J→Cd×dB : J\to\mathbb C^{d\times d} such that AmBn=BnAmA_m B_n = B_n A_m for all m∈Im\in I, n∈Jn\in J, and every complex d×dd\times d matrix ρ\rho (no positivity or trace condition):

tr⁡(∑m∈I∑n∈JBnAmρAm†Bn†)=tr⁡((∑m∈IAm†Am)(∑n∈JBnρBn†)).\operatorname{tr}\Big(\sum_{m\in I}\sum_{n\in J} B_n A_m\rho A_m^\dagger B_n^\dagger\Big) = \operatorname{tr}\Big(\Big(\sum_{m\in I}A_m^\dagger A_m\Big)\Big(\sum_{n\in J} B_n\rho B_n^\dagger\Big)\Big).

Only commutation of each AmA_m with each BnB_n is assumed (not with the adjoints, and no completeness).

Human review

  • Endorsed by Shuze Chen · Oct 5, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 5, 2026

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

View graph