Quantum minimum description of density matrices
Patrick Hayden, Alexander Maloney, Jinzhao Wang, Yuxiang Yang
quant-ph
Oct 5, 2026 · v1
cs.IT math-ph
TL;DR
The authors provide a Lean certificate formally checking their proofs of the optimal quantum compression cost for density matrices with known spectrum.
Abstract
We study a variant of Schumacher compression. The task asks for the minimal memory cost for compressing many copies of a density matrix with known spectrum and unknown eigenbasis, without preserving its purification. For fixed dimension and distinct positive eigenvalues, we obtain the cost through its additive constant. Achievability uses a generalization of Werner's cloning map to $\mathrm{GL}(d,\mathbb C)$ irreducible representations, with finite trace-distance bounds controlled by highest-weight differences and row gaps. The matching converse follows from a quantitative form of Koashi–Imoto incompressibility for irreducible group orbits under a spectral-gap assumption. We also identify the relation between this quantum minimum description length and universal lossless coding overhead, and its connection to free entropy is explained in a companion letter. We provide a Lean certificate for our proofs.
Problem
The task is to find the minimal memory cost for compressing many identical copies of a density matrix with known spectrum and unknown eigenbasis, without preserving its purification. The cost is sought up to and including its additive constant, for fixed dimension and distinct positive eigenvalues.
Approach
Achievability generalizes Werner's cloning map to GL(d,C) irreducible representations. The encoder measures the Schur label and clones into one fixed padded target irrep; the decoder samples a label and clones back. Trace-distance bounds are controlled by highest-weight differences and row gaps. The converse is a quantitative Koashi–Imoto incompressibility bound for irreducible group orbits under a spectral-gap assumption, and the proofs are accompanied by a Lean certificate.
Results
The optimal memory cost is L_{d,r}(n,x)+o(1), attained with error O(log n/√n), with a matching converse for any code with vanishing error. The work also relates this cost to the overhead of universal lossless coding for an unknown eigenbasis.
