QWIRE
1 program
Added 2026-03-11T10:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: QWire
Provenance: commit 738eed743d · authored 2026-03-11T18:48:50+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Bell State and Quantum Teleportation Circuit
Provenance: commit 738eed743d · authored 2026-03-11T18:48:50+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
(* Bell state preparation in QWIRE *)
Require Import Quantum.
Require Import Dirac.
Open Scope matrix_scope.
(* Hadamard gate applied to |0> gives |+> state *)
Definition hadamard_example : Matrix 2 1 :=
hadamard × ket 0.
(* Bell state |Phi+> = (|00> + |11>) / sqrt(2) *)
Definition bell_phi_plus : Matrix 4 1 :=
(I 2 ⊗ hadamard) × (cnot × (ket 0 ⊗ ket 0)).
(* Verify Bell state has correct norm *)
Lemma bell_phi_plus_norm :
inner_product bell_phi_plus bell_phi_plus = 1.
Proof.
unfold bell_phi_plus, inner_product.
solve_matrix.
Qed.
(* Teleportation circuit: Alice has qubit psi, shares Bell pair with Bob *)
(* After Alice measures, Bob applies corrections to recover psi *)
Definition teleport_circuit (psi : Matrix 2 1) : Matrix 2 1 :=
(* Step 1: Create Bell pair *)
let bell_pair := (I 2 ⊗ hadamard) × (cnot × (ket 0 ⊗ ket 0)) in
(* Step 2: Alice's CNOT between psi and her qubit *)
let after_cnot := (cnot ⊗ I 2) × (psi ⊗ bell_pair) in
(* Result: psi teleported to Bob's qubit after measurement and correction *)
after_cnot.