Prove2Me

Eq. (12), p. 6 — the reduced state Tr_K |ψ⟩⟨ψ| equals XX*/Tr(XX*) for the n × k coordinate matrix X(i, j) = ψ_ij

Proved
NechitaRDM.MP.eq_12

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1partial-tracequantum-informationwishart

Let ψ=∑i=1n∑j=1kψij ei⊗fj\psi = \sum_{i=1}^n\sum_{j=1}^k \psi_{ij}\, e_i \otimes f_j be a vector of Cn⊗Ck\mathbb C^n \otimes \mathbb C^k and arrange its coordinates in the n×kn\times k matrix XX with X(i,j)=ψijX(i,j) = \psi_{ij}. Then the partial trace over the environment Ck\mathbb C^k of the pure density matrix ∣ψ⟩⟨ψ∣|\psi\rangle\langle\psi| is

ρ=Tr⁡K(∣ψ⟩⟨ψ∣)=XX∗Tr⁡(XX∗).\rho = \operatorname{Tr}_{\mathcal K}\big(|\psi\rangle\langle\psi|\big) = \frac{X X^*}{\operatorname{Tr}(X X^*)} .

This deterministic identity, obtained in the paper through eqs. (9)–(11), turns a random pure state of the global system into a normalized Wishart-type matrix.

Formalization Note Cn⊗Ck\mathbb C^n\otimes\mathbb C^k is indexed by Fin n × Fin k and Tr⁡K\operatorname{Tr}_{\mathcal K} is the published WildeQIT.partialTraceRight. No hypothesis ψ≠0\psi \ne 0 is needed: at ψ=0\psi = 0 both sides are 00 in Lean.

Preamble
import Mathlib
import Definitions.Def_NechitaRDM_MP_Basic
Formal statement
namespace NechitaRDM.MP

/-- **Eq. (12)** (p. 6). Arranging the coordinates `ψ_{ij}` of `ψ ∈ ℂⁿ ⊗ ℂᵏ` in an `n × k`
matrix `X` with `X(i, j) = ψ_{ij}`, the reduced state is `Tr_K |ψ⟩⟨ψ| = XX* / Tr(XX*)`. -/
theorem eq_12 {n k : ℕ} (X : Matrix (Fin n) (Fin k) ℂ) :
    WildeQIT.partialTraceRight (pureState fun p : Fin n × Fin k => X p.1 p.2) =
      (wishart X).trace⁻¹ • wishart X := by sorry

end NechitaRDM.MP
Source
Nechita, Asymptotics of random density matrices, arXiv:quant-ph/0702154v3, p. 6, eq. (12) (derived through eqs. (9)–(11), pp. 5–6)
Human review

  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 21, 2026

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

View graph