Bell pair (EPR pair) and its preparation

The Bell state (EPR-pair) (|00⟩ + |11⟩)/√2 [dW19, qcnotes.tex:622] is prepared from |00⟩ by a Hadamard on qubit 0 followed by a CNOT with control qubit 0:

CNOT · (H ⊗ I) · |00⟩ = (|00⟩ + |11⟩)/√2.

This is a Primitives module: the Bell pair is a reusable resource state, so it lives below Algorithms/ and is shared by the protocols that consume it (superdense coding, teleportation) without those algorithms importing one another. The registered bell-state-prep target is bell_state_prep here.

Main results

• LeanPool.LeanQuantumAlg.bell — the Bell state, as a PureState 2.
• LeanPool.LeanQuantumAlg.BellStatePreparation.main — the preparation-circuit equality.
• LeanPool.LeanQuantumAlg.bell_eq_tensor — the Bell state in per-qubit tensor form.
• LeanPool.LeanQuantumAlg.norm_bell — the Bell state is normalized.

noncomputable def QuantumAlg.bellVec : StateVector 2

Raw Bell-state vector ( |00⟩ + |11⟩ ) / √2 [dW19, qcnotes.tex:622]. In the big-endian basis labelling, |00⟩ = ket 0 and |11⟩ = ket 3.

Equations

• QuantumAlg.bellVec = QuantumAlg.PureState.invSqrt2 • ((QuantumAlg.PureState.ket 0).vec + (QuantumAlg.PureState.ket 3).vec)

theorem QuantumAlg.norm_bellVec : ‖bellVec‖ = 1

The raw Bell-state vector has unit norm.

noncomputable def QuantumAlg.bell : PureState 2

The Bell state (EPR-pair) as a normalized pure state.

Equations

• QuantumAlg.bell = QuantumAlg.PureState.ofVec QuantumAlg.bellVec QuantumAlg.norm_bellVec

theorem QuantumAlg.bell_eq_tensor : bell.vec = PureState.invSqrt2 • ((PureState.ket0.tensor PureState.ket0).vec + (PureState.ket1.tensor PureState.ket1).vec)

The Bell state in per-qubit tensor form: (|0⟩⊗|0⟩ + |1⟩⊗|1⟩)/√2.

theorem QuantumAlg.BellStatePreparation.main : Gate.CNOT.apply ((Gate.H.tensor 1).apply (PureState.ket0.tensor PureState.ket0)) = bell

Bell-state preparation: a Hadamard on qubit 0 followed by a CNOT (control = qubit 0) turns |00⟩ into the Bell state.

@[simp]

theorem QuantumAlg.norm_bell : ‖bell‖ = 1

The Bell state is normalized by construction.