The Proposition

Alice holds a quantum system $A$ and Bob a quantum system $B$, and they share a pure state $|\psi\rangle$ of the pair. They are restricted to local operations and classical communication (LOCC): each may measure their own system or apply a unitary to it, and announce a measurement outcome to the other, for as many rounds as they like and in either direction, every step chosen in view of the outcomes announced before it. Suppose some such protocol takes $|\psi\rangle$ to a state $\sigma$ of the pair whatever the outcomes. Then one round does the same: Alice makes a single measurement and announces its outcome $j$, Bob applies a unitary $V_j$ chosen by $j$, and the pair is left in $\sigma$.

Systems and Operations

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ The composite system $A \otimes B$ of two quantum systems $A$ and $B$ is the quantum system whose state space is the tensor product of the state spaces of $A$ and $B$; Alice holds the first factor, Bob the second.^✦

A state $\rho$ of a quantum system $S$ is a positive operator of unit trace on the state space of $S$.^✦ A pure state $|\psi\rangle$ of $S$ is a unit vector in the state space of $S$, $\langle\psi|\psi\rangle = 1$^✦, and the state it determines is the projector $|\psi\rangle\langle\psi|$ onto it.^✦

A unitary $U$ of $S$, an evolution of $S$ as a closed system, is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = I$.^✦ A measurement on $S$ with a finite set of outcomes is a family of measurement operators $M_j$ on the state space of $S$, one for each outcome $j$, that satisfy the completeness relation $$\sum_j M_j^\dagger M_j = I .$$(1)^✦

Alice acts on the first factor of a state $\rho$ of $A \otimes B$. A unitary $U$ of hers takes $\rho$ to $(U \otimes I)\rho(U \otimes I)^\dagger$, and a measurement $\{M_j\}$ on $A$ gives the outcome $j$ with probability $p_j$ and, when $p_j \neq 0$, leaves the state $\rho_j$: $$p_j = \operatorname{tr}\bigl[(M_j \otimes I)\,\rho\,(M_j \otimes I)^\dagger\bigr], \qquad \rho_j = \frac{(M_j \otimes I)\,\rho\,(M_j \otimes I)^\dagger}{p_j} .$$(2) Bob acts on the second factor in the same way: a unitary $V$ of his takes $\rho$ to $(I \otimes V)\rho(I \otimes V)^\dagger$, and a measurement $\{M_j\}$ on $B$ acts through $I \otimes M_j$.

LOCC Protocols

An LOCC protocol $P$ between Alice and Bob is either the stopped protocol, which does nothing further, or a first step followed by a protocol.^✦ The first step is one of four. Alice measures $A$ with a measurement $\{M_j\}$ of $n$ outcomes, announces the outcome $j$ to Bob, and continues with a protocol $P_j$ chosen by $j$.^✦ Bob measures $B$, announces his outcome to Alice, and continues in the same way. Alice applies a unitary $U$ to $A$ and continues with a protocol $P'$, or Bob applies a unitary $V$ to $B$ and continues with $P'$.^✦

A protocol $P$ transforms a state $\rho$ of $A \otimes B$ into a state $\sigma$ of $A \otimes B$, written $\rho \xrightarrow{P} \sigma$, when run on $\rho$ it ends in $\sigma$ whatever outcomes occur.^✦ By its first step, $$\begin{aligned} &\text{$P$ stops:} &&\rho \xrightarrow{P} \sigma \text{ when } \rho = \sigma,\\ &\text{Alice measures $\{M_j\}$, then $P_j$:} &&\rho \xrightarrow{P} \sigma \text{ when } \rho_j \xrightarrow{P_j} \sigma \text{ for every $j$ with } p_j \neq 0,\\ &\text{Alice applies $U$, then $P'$:} &&\rho \xrightarrow{P} \sigma \text{ when } (U \otimes I)\,\rho\,(U \otimes I)^\dagger \xrightarrow{P'} \sigma, \end{aligned}$$(3)^✦ and likewise for Bob’s two steps. A state $\rho$ can be transformed into $\sigma$ by LOCC, written $\rho \xrightarrow{\text{LOCC}} \sigma$, when some protocol transforms $\rho$ into $\sigma$.

The one way protocol given by a measurement $\{M_j\}_{j=1}^{n}$ on $A$ and unitaries $V_1, \dots, V_n$ of $B$ has Alice measure and announce $j$, then Bob apply $V_j$, and then stops.^✦ By (3) it transforms $\rho$ into $\sigma$ exactly when $$(I \otimes V_j)\,\rho_j\,(I \otimes V_j)^\dagger = \sigma \quad \text{for every $j$ with } p_j \neq 0 .$$(4) A state $\rho$ of $A \otimes B$ reaches $\sigma$ by one way LOCC, written $\rho \xrightarrow{\text{one way}} \sigma$, when some one way protocol transforms $\rho$ into $\sigma$.^✦

The Claim

What Is Checked

The claim is stated over a pure state $|\psi\rangle$ of the composite system $A \otimes B$, taken through its projector $|\psi\rangle\langle\psi|$, a state $\sigma$ of $A \otimes B$, the LOCC protocols, the transformation (3) of a state by a protocol, and reachability by one way LOCC.

Of these constructions the library proves that the projector onto a unit vector is a density operator, so that $|\psi\rangle\langle\psi|$ is a state of $A \otimes B$.