Lean, informalized

Nielsen & Chuang · Chapter 2, Introduction to quantum mechanics · p. 96

Exercise 2.68 - No two single qubit states have the Bell state as their tensor product

The Bell state is not a product of qubit states.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

Two qubits are in the Bell state |Φ+⟩=|00⟩+|11⟩2.|\Phi^+\rangle = \frac{|00\rangle + |11\rangle}{\sqrt{2}} .(1)✦ The exercise is to show that there are no single qubit states |a⟩|a\rangle of the first qubit and |b⟩|b\rangle of the second with |Φ+⟩=|a⟩|b⟩|\Phi^+\rangle = |a\rangle|b\rangle.✦ A pure state of a pair of qubits that is not the product of a pure state of the first and a pure state of the second is called entangled.

Two Qubits

A quantum system SS is a physical system whose state space is a finite dimensional complex Hilbert space.✦ The composite system S⊗TS \otimes T of two quantum systems SS and TT is the quantum system whose state space is the tensor product of the state spaces of SS and TT.✦ The qubit is the two level system whose state space is ℂ2\mathbb{C}^2 itself.✦

A pure state |ψ⟩|\psi\rangle of a system SS is a unit vector in the state space of SS.✦ For a bit ii, the basis state |i⟩|i\rangle of the qubit is the pure state whose vector is the standard basis vector eie_i of ℂ2\mathbb{C}^2, and |0⟩|0\rangle and |1⟩|1\rangle are the computational basis states.✦

For pure states |ψ⟩|\psi\rangle of SS and |φ⟩|\varphi\rangle of TT, the product |ψ⟩⊗|φ⟩|\psi\rangle \otimes |\varphi\rangle, written |ψ⟩|φ⟩|\psi\rangle|\varphi\rangle in the exercise, is the pure state of S⊗TS \otimes T whose vector is the tensor product of the two vectors.✦

The unnormalised Bell vector is the vector |00⟩+|11⟩=|0⟩⊗|0⟩+|1⟩⊗|1⟩|00\rangle + |11\rangle = |0\rangle \otimes |0\rangle + |1\rangle \otimes |1\rangle in the state space ℂ2⊗ℂ2\mathbb{C}^2 \otimes \mathbb{C}^2 of two qubits.✦ The Bell state |Φ+⟩|\Phi^+\rangle is the pure state of the composite system of two qubits whose vector is the unnormalised Bell vector divided by 2\sqrt{2}, as in (1).✦

The Claim

Theorem 1. Let |a⟩|a\rangle and |b⟩|b\rangle be pure states of a qubit. Then the Bell state of two qubits is not their product: |Φ+⟩≠|a⟩⊗|b⟩.|\Phi^+\rangle \neq |a\rangle \otimes |b\rangle .(2)✦

What Is Checked

The claim (2) is stated over the Bell state |Φ+⟩|\Phi^+\rangle and the product |a⟩⊗|b⟩|a\rangle \otimes |b\rangle of two pure states of a qubit, both pure states of the composite system of two qubits.

The library proves that each of these constructions gives a pure state. For the product this is (3), the norm of a tensor product of vectors being the product of their norms: ∥|a⟩⊗|b⟩∥=∥|a⟩∥∥|b⟩∥=1.\bigl\lVert |a\rangle \otimes |b\rangle \bigr\rVert = \bigl\lVert |a\rangle \bigr\rVert \, \bigl\lVert |b\rangle \bigr\rVert = 1 .(3) The unnormalised Bell vector has norm 2\sqrt{2}, so the division in (1) leaves a unit vector.