Prove2Me

Observables commute in the maximally mixed state

Proved
HighEntropyLimit.maximally_mixed_expectation_comm

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

mathematical-physicsquantum-mechanics

Let n∈Nn\in\mathbb N, let A,BA,B be complex n×nn\times n matrices, and let ρ=I/n\rho = I/n be the maximally mixed state. Then

⟨AB⟩ρ=tr⁡(ABρ)=tr⁡(BAρ)=⟨BA⟩ρ.\langle AB\rangle_\rho = \operatorname{tr}(AB\rho) = \operatorname{tr}(BA\rho) = \langle BA\rangle_\rho.
Preamble
import Mathlib
Formal statement
namespace HighEntropyLimit
theorem maximally_mixed_expectation_comm (n : ℕ) (A B : Matrix (Fin n) (Fin n) ℂ) :
    Matrix.trace (A * B * ((n : ℂ)⁻¹ • (1 : Matrix (Fin n) (Fin n) ℂ))) =
      Matrix.trace (B * A * ((n : ℂ)⁻¹ • (1 : Matrix (Fin n) (Fin n) ℂ))) := by sorry
end HighEntropyLimit
Source
Carcassi, Landini, Aidala, Classical mechanics as the high-entropy limit of quantum mechanics, arXiv:2411.00972v3 (1 Feb 2026), https://arxiv.org/abs/2411.00972, p. 5, Eq. (4)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

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

View graph