Empirical/QM: Bell-state preparation circuit #
Category: 3-Local (promotion-ready to 2-Framework on demand).
The canonical two-gate Bell-state preparation circuit:
(CNOT) ∘ (H ⊗ I) applied to |00⟩ yields |Φ⁺⟩ = (|00⟩ + |11⟩)/√2.
This is the building block for entanglement generation in essentially
every quantum-circuit construction. Pairs with Empirical/CSD/Gates/BellPrep.lean.
Contents #
qmH_tensor_I: the 4×4 matrixH ⊗ I(Hadamard on qubit 0, identity on qubit 1).qmBellPrepCircuit: the compositionqmCNOT * qmH_tensor_I.qmKet00,qmKetPhiPlus: the|00⟩and|Φ⁺⟩state vectors asEuclideanSpace ℂ (Fin 4).qmBellPrep_yields_phiplus: the headline identityqmBellPrepCircuit · |00⟩ = |Φ⁺⟩(matrix-vector form, up to theMatrix.toEuclideanLincoercion).
Notation #
|Φ⁺⟩ is one of the four Bell states. The LF3 singlet is |Ψ⁻⟩,
a different Bell state related to |Φ⁺⟩ by (I ⊗ σ_y) up to
phase. No direct algebraic identity between this file's circuit
output and the LF3 singlet — the circuit produces a different Bell
state, mentioned in the docstring for context.
The 4×4 matrix H ⊗ I. Hadamard on qubit 0 (the high bit),
identity on qubit 1.
Explicit entries with basis order |00⟩, |01⟩, |10⟩, |11⟩:
(1/√2) · ((H[0,0]·I, H[0,1]·I), (H[1,0]·I, H[1,1]·I)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Bell-state preparation circuit: CNOT ∘ (H ⊗ I).
Equations
Instances For
The Bell state |Φ⁺⟩ = (|00⟩ + |11⟩) / √2.
Equations
Instances For
Definitional unfold of the Bell-prep circuit's factorisation.
A rfl-closed labelled handle on qmBellPrepCircuit = qmCNOT * qmH_tensor_I;
exists for downstream consumers that prefer the factorised form. The
genuine empirical identity is qmBellPrep_yields_phiplus below.
Column-0 entries of the composite circuit #
The 4×4 matrix qmBellPrepCircuit = qmCNOT * qmH_tensor_I has, in
column 0 (the only column probed by |00⟩ = e_0):
- entry 0:
(1/√2)(fromCNOT[0,0] · (H⊗I)[0,0] = 1 · (1/√2)), - entry 1:
0, - entry 2:
0(CNOT[2,3] · (H⊗I)[3,0] = 1 · 0), - entry 3:
(1/√2)(CNOT[3,2] · (H⊗I)[2,0] = 1 · (1/√2)).
These four entries are the matrix-element computations underlying
qmBellPrep_yields_phiplus.
Component-form expressions for qmKet00 and qmKetPhiPlus #
Both vectors live in EuclideanSpace ℂ (Fin 4) and have explicit
component expressions; we expose those for the headline proof.
qmKet00.ofLp is 1 at index 0 and 0 elsewhere. qmKetPhiPlus.ofLp
is (1/√2) at indices 0 and 3 and 0 elsewhere.
For any row index k, (qmBellPrepCircuit *ᵥ qmKet00.ofLp) k
collapses to the column-0 entry qmBellPrepCircuit k 0, because
qmKet00.ofLp is 1 at index 0 and 0 elsewhere.
Bell-prep headline identity: (CNOT ∘ (H ⊗ I)) |00⟩ = |Φ⁺⟩.
The matrix qmBellPrepCircuit applied to the |00⟩ standard basis
vector produces the Bell state |Φ⁺⟩ = (|00⟩ + |11⟩)/√2. This is the
genuine empirical identity the Bell-state-preparation circuit
encodes; the factorisation qmBellPrep_factorisation above is the
defining decomposition.
Proof. Componentwise via ext: expose the matrix-mulVec form
via Matrix.toLpLin_apply, then collapse the mulVec to column 0 via
qmBellPrepCircuit_mulVec_qmKet00, and compare to qmKetPhiPlus.ofLp i
via the four column-0 and qmKetPhiPlus_ofLp_* lemmas.