GHZ state preparation

The three-qubit GHZ state (|000⟩ + |111⟩)/√2, prepared from |000⟩ by a Hadamard on qubit 0 followed by a CNOT cascade:

(I ⊗ CNOT) · (CNOT ⊗ I) · (H ⊗ I ⊗ I) · |000⟩ = (|000⟩ + |111⟩)/√2.

States of this multipartite family are due to Greenberger, Horne and Zeilinger (1989), whose original argument uses a four-particle spin state (reprinted as arXiv:0712.0921). The three-qubit form and the name "GHZ state" are standard textbook material (e.g. Nielsen and Chuang 2000). In [dW19] the unnormalized states |000⟩ ± |111⟩ appear as the code blocks of Shor's 9-qubit code [dW19, qcnotes.tex:7456], and a locally-equivalent three-qubit state powers Mermin's game [dW19, qcnotes.tex:6667].

Conventions

• Big-endian basis labelling as in Core/State.lean: |000⟩ = ket 0 and |111⟩ = ket 7.
• Qubit 0 carries the Hadamard and controls the first CNOT (target qubit 1); qubit 1 controls the second CNOT (target qubit 2).
• The circuit factors use the qubit groupings 1+2, 2+1, 1+2; the index types all reduce to Fin (2^3) definitionally.

Main results

• LeanPool.LeanQuantumAlg.ghz — the three-qubit GHZ state, as a PureState 3.
• LeanPool.LeanQuantumAlg.ghzCircuit — the preparation circuit, as a Gate 3.
• LeanPool.LeanQuantumAlg.ghz_state_prep — the preparation-circuit equality.
• LeanPool.LeanQuantumAlg.norm_ghz — the GHZ state is normalized.

noncomputable def QuantumAlg.ghzVec : StateVector 3

The three-qubit GHZ state (|000⟩ + |111⟩)/√2 (Greenberger, Horne and Zeilinger 1989; three-qubit form standard, e.g. Nielsen and Chuang 2000). In the big-endian basis labelling, |000⟩ = ket 0 and |111⟩ = ket 7.

Equations

• QuantumAlg.ghzVec = QuantumAlg.PureState.invSqrt2 • ((QuantumAlg.PureState.ket 0).vec + (QuantumAlg.PureState.ket 7).vec)

theorem QuantumAlg.norm_ghzVec : ‖ghzVec‖ = 1

The raw GHZ vector has unit norm.

noncomputable def QuantumAlg.ghz : PureState 3

The normalized GHZ state.

Equations

• QuantumAlg.ghz = QuantumAlg.PureState.ofVec QuantumAlg.ghzVec QuantumAlg.norm_ghzVec

noncomputable def QuantumAlg.ghzCircuit : Gate 3

The GHZ preparation circuit: a Hadamard on qubit 0, a CNOT with control 0 and target 1, then a CNOT with control 1 and target 2 — (I ⊗ CNOT) · (CNOT ⊗ I) · (H ⊗ I ⊗ I).

Equations

• QuantumAlg.ghzCircuit = QuantumAlg.Gate.tensor 1 QuantumAlg.Gate.CNOT * (QuantumAlg.Gate.CNOT.tensor 1 * QuantumAlg.Gate.H.tensor 1)

theorem QuantumAlg.GHZStatePreparation.main : ghzCircuit.applyVec (PureState.ket0.vec.tensor (PureState.ket0.vec.tensor PureState.ket0.vec)) = ghz.vec

GHZ state preparation: the cascade circuit turns |000⟩ into the GHZ state, extending Bell-state preparation (bell_state_prep) by one CNOT.

@[simp]

theorem QuantumAlg.norm_ghz : ‖ghz‖ = 1

The GHZ state is normalized.