Prove2Me

Eq. (7): ∑mtr(AmρAm†)=tr(ρE)\sum_m \mathrm{tr}(A_m\rho A_m^\dagger) = \mathrm{tr}(\rho E)

Proved
PeresTerno.outcome_probability_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} be a finite family of complex e×de\times d matrices (the Kraus matrices of one outcome μ\mu), let E=∑mAm†AmE = \sum_m A_m^\dagger A_m be the corresponding POVM element, and let ρ\rho be any complex d×dd\times d matrix. Then

∑m∈Itr⁡(Am ρ Am†)=tr⁡(ρ E).\sum_{m\in I} \operatorname{tr}\big(A_m\,\rho\,A_m^\dagger\big) = \operatorname{tr}(\rho\,E).

This is Eq. (7) of the source: the probability of outcome μ\mu depends on the Kraus matrices only through the POVM element EμE_\mu.

Formalization Note The identity is stated for every square matrix ρ\rho, which contains the source's case of a density matrix.

Preamble
import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

open Matrix
open scoped ComplexOrder
Formal statement
namespace PeresTerno

theorem outcome_probability_eq_trace_povm {d e ι : Type*} [Fintype d] [Fintype e] [Fintype ι]
    (A : ι → Matrix e d ℂ) (ρ : Matrix d d ℂ) :
    ∑ m, trace (A m * ρ * (A m)ᴴ) = trace (ρ * povmElement A) := 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, p. 100, Sec. II.D, Eq. (7) (with Eq. (8))
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 arbitrary index types dd and ee and a finite index type II (with dd, ee finite), every family A:I→Ce×dA : I\to\mathbb C^{e\times d} and every complex d×dd\times d matrix ρ\rho (no positivity, Hermiticity or trace condition):

∑m∈Itr⁡(Am ρ Am†)=tr⁡(ρ∑m∈IAm†Am),\sum_{m\in I} \operatorname{tr}\big(A_m\,\rho\,A_m^{\dagger}\big) = \operatorname{tr}\Big(\rho \sum_{m\in I} A_m^{\dagger}A_m\Big),

where †{}^\dagger is conjugate transpose and both sides are complex numbers. If II is empty both sides are 00.

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