The Theorem

A quantum code stores information in a subspace of the state space of a system, the code space. Suppose a noise process $\mathcal{E}$ acts on the system through operators $E_i$ , its operation elements, and a recovery operation $\mathcal{R}$ undoes it on the code: noise followed by recovery returns every state of the code space up to normalization. Theorem 10.2 of Nielsen and Chuang says that the same $\mathcal{R}$ undoes every noise process $\mathcal{F}$ whose operation elements are linear combinations of the $E_i$ , $F_j = \sum_i m_{ji} E_i ,$ (1)^✦ for any complex numbers $m_{ji}$ .

A Quantum System

A quantum system $S$ is a physical object whose mathematical realisation is its state space, a finite dimensional complex Hilbert space.^✦ A state $\rho$ of $S$ is a positive operator of unit trace on the state space of $S$ , pure or mixed.^✦

Code, Noise and Recovery

A code of $S$ is a Hermitian operator $P$ on the state space of $S$ , such as the projector onto a code subspace. A state $\rho$ of $S$ lies in the code when $P \rho P = \rho$ .

Noise and recovery are each given by finitely many operators on the state space of $S$ , their operation elements: the errors $E_i$ and the recovery elements $R_k$ . The recovery acts on an operator $\sigma$ as $\mathcal{R}(\sigma) = \sum_k R_k \sigma R_k^\dagger ,$ (2) and the noise $\mathcal{F}$ acts as in (2) through the $F_j$ .

A recovery with operation elements $R_k$ corrects the errors $E_i$ on the code $P$ when there are complex numbers $c_{ki}$ with $R_k E_i P = c_{ki} P \qquad \text{for every } k \text{ and } i .$ (3)^✦

The Claim

Theorem 1. Let $S$ be a quantum system and $P$ a Hermitian operator on its state space. Let $R_k$ and $E_i$ be finitely many operators on the state space such that the recovery with elements $R_k$ corrects the errors $E_i$ on the code $P$ , as in (3), and let $\mathcal{F}$ be the noise with operation elements (1), for any complex numbers $m_{ji}$ . Then there is a real number $\lambda \ge 0$ such that every state $\rho$ of $S$ with $P \rho P = \rho$ satisfies $\mathcal{R}\bigl(\mathcal{F}(\rho)\bigr) = \lambda \rho .$ (4)^✦

What Is Checked

The claim is stated over a quantum system $S$ and its states, a Hermitian operator $P$ for the code, finitely many errors $E_i$ and recovery elements $R_k$ related by (3), and an arbitrary complex matrix $m_{ji}$ forming the noise $\mathcal{F}$ . What the library proves about them is the proportionality (4).