Finite Memory History Capacity

Abstract

Perfectly distinguishable density matrices number at most the memory dimension.

Theorem 1.1 (Exact history capacity of finite quantum memory).

$$\begin{array}{r}\forall N,d:Nat,\\ \forall \rho ,E:\mathrm{Fin}(N)\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\\ (\forall i:\mathrm{Fin}(N),\mathrm{PosSemidef}({\rho }_i)\wedge \mathrm{Tr}({\rho }_i)=1)\Rightarrow \\ (\forall j:\mathrm{Fin}(N),\mathrm{PosSemidef}(E_j))\Rightarrow \\ (\sum _{j:\mathrm{Fin}(N)}{E}_j=I)\Rightarrow \\ (\forall i,j:\mathrm{Fin}(N),\mathrm{Tr}(E_j\cdot {\rho }_i)=\mathrm{if}(i=j,1,0))\Rightarrow \\ N\le d.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/FiniteMemoryHistoryCapacity.finite_memory_history_capacity (✓ std3). ∎

Citation. Stephen M. Barnett and Sarah Croke (2009). Quantum state discrimination. DOI: 10.1364/AOP.1.000238.

Commentary.

The memory has complex dimension d. Histories are represented by the indexed density matrices rho, and E is one designated POVM. PosSemidef means positive semidefinite, Tr is the complex matrix trace, I is the identity matrix, and if selects its second or third argument according to its first argument.

A zero trace pairing of two positive matrices forces their product to vanish, so the state range lies in the effect kernel. Applying this to the positive complement of an effect with unit probability puts its state range in the one-eigenspace.

The state ranges are therefore pairwise orthogonal. Trace one makes every state nonzero. Choosing a nonzero vector in each range gives a linearly independent family in dimension d.

This bound concerns perfectly distinguishable records, rather than the number of real parameters of a density matrix. Barnett and Croke provide the literature context for discrimination and orthogonal supports; the cited note identifies the scope.

References

• Truth anchor: D5/S3/Quantum/Measurements/FiniteMemoryHistoryCapacity.finite_memory_history_capacity