TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Bell preparation transform and inverse

Statement

On the ordered two-qubit register, let $B : = {CNOT}_{1 \to 2} (H \otimes I)$ , where operator products act right-to-left. For $a, b \in {0, 1}$ ,

$B ∣ a b ⟩ = \frac{∣ 0, b ⟩ + (- 1)^{a} ∣ 1, b \oplus 1 ⟩}{\sqrt{2}} = (I \otimes X^{b}) (Z^{a} \otimes I) ∣ Φ^{+} ⟩ .$

In the label order $00, 01, 10, 11$ , these are respectively $∣ Φ^{+} ⟩, ∣ Ψ^{+} ⟩, ∣ Φ^{-} ⟩, ∣ Ψ^{-} ⟩$ . They form an orthonormal basis of $Q_{2} \otimes Q_{2}$ , and $B^{†} = (H \otimes I) {CNOT}_{1 \to 2}$ maps those four vectors back to their labels.

Facts & Assumptions

Given: The ordered two-qubit computational basis, $a, b \in {0, 1}$ , and the operators in the Statement.

[A1]

$a$ and $b$ are bits; $\oplus$ is addition modulo $2$ .

[F1]

The Bell vectors defines $∣ Φ^{+} ⟩, ∣ Φ^{-} ⟩, ∣ Ψ^{+} ⟩, ∣ Ψ^{-} ⟩$ and fixes the label order $00, 01, 10, 11$ as phase bit then flip bit.

[F2]

Exact one-qubit gates and rotations gives $H = 2^{- 1 / 2} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array})$ and verifies $H^{*} = H$ and $H^{2} = I$ .

[F3]

CNOT and Control-Target Order defines ${CNOT}_{1 \to 2} ∣ a, t ⟩ = ∣ a, t \oplus a ⟩$ in control-first order.

[F4]

Ordered tensor registers, their inner product, and wire permutations makes the ordered product basis lexicographic in the factor indices; for $Q_{2} \otimes Q_{2}$ it consists of $∣ 00 ⟩, ∣ 01 ⟩, ∣ 10 ⟩, ∣ 11 ⟩$ .

[F5]

The computational basis is orthonormal proves that the ordered computational basis of each $Q_{2}$ factor is orthonormal.

[F6]

Tensor products of finitely many linear maps defines $H \otimes I$ by $(H \otimes I) (x \otimes y) = H x \otimes y$ and extends this rule linearly.

[F7]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ defines $T^{*}$ by $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ .

[F8]

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix identifies the matrix of an adjoint in orthonormal bases with the conjugate transpose.

Proof

1.1givenA1F2F6algebra

The matrix in [F2] gives $H ∣ a ⟩ = (∣ 0 ⟩ + (- 1)^{a} ∣ 1 ⟩) / \sqrt{2}$ for each bit $a$ . By [F6], $(H \otimes I) ∣ a b ⟩ = (∣ 0, b ⟩ + (- 1)^{a} ∣ 1, b ⟩) / \sqrt{2}$ .

1.2F2F3F4F5F6algebra

From [F3], applying CNOT twice fixes every basis vector because $(t \oplus a) \oplus a = t$ . Its matrix permutes the orthonormal basis [F4], so its inverse is its transpose and equals itself. The matrix of $H \otimes I$ in [F4] is real symmetric and its square is the identity by [F2]. Thus both factors are self-adjoint involutions, and direct composition gives $(H \otimes I) {CNOT}_{1 \to 2} B = I = B (H \otimes I) {CNOT}_{1 \to 2}$ .

2.1step 1.1F3algebra

Apply the control-first action in [F3] to the two terms of step 1.1. The control-zero term is fixed, while the control-one term changes its target from $b$ to $b \oplus 1$ . Therefore $B ∣ a b ⟩ = (∣ 0, b ⟩ + (- 1)^{a} ∣ 1, b \oplus 1 ⟩) / \sqrt{2}$ .

3.1step 2.1F1F5algebra

Substituting $00, 01, 10, 11$ into step 2.1 gives $Φ^{+}, Ψ^{+}, Φ^{-}, Ψ^{-}$ in that order, exactly as defined in [F1]. Each has norm one because it is a signed sum of two distinct orthonormal computational basis vectors from [F5], divided by $\sqrt{2}$ . The inner product of $Φ^{+}$ with $Φ^{-}$ and of $Ψ^{+}$ with $Ψ^{-}$ is $(1 - 1) / 2 = 0$ ; cross-pair inner products are zero because their computational supports are disjoint.

4.1step 3.1F4F5algebra

The four vectors in step 3.1 are an orthonormal set of four vectors in the four-dimensional space whose product basis is listed in [F4]; hence they are an orthonormal basis.

5.1step 3.1step 1.2F2F3F6F7F8algebra∎

In matrices, $(A B)_{i j} = \sum_{k} A_{i k} B_{k j}$ , so conjugating and transposing this finite sum gives $(A B)^{†} = B^{†} A^{†}$ . By [F7]–[F8] this is the adjoint product rule in the register pairing. Since both factors in [F6] and [F3] are self-adjoint by step 1.2, $B^{†} = (H \otimes I) {CNOT}_{1 \to 2}$ . Applying CNOT sends the four Bell vectors to $\frac{∣ 0 ⟩ + ∣ 1 ⟩}{\sqrt{2}} \otimes ∣ 0 ⟩$ , $\frac{∣ 0 ⟩ + ∣ 1 ⟩}{\sqrt{2}} \otimes ∣ 1 ⟩$ , $\frac{∣ 0 ⟩ - ∣ 1 ⟩}{\sqrt{2}} \otimes ∣ 0 ⟩$ , and $\frac{∣ 0 ⟩ - ∣ 1 ⟩}{\sqrt{2}} \otimes ∣ 1 ⟩$ , respectively. By the matrix in [F2], $H$ sends the first factors in these expressions to $∣ 0 ⟩, ∣ 0 ⟩, ∣ 1 ⟩, ∣ 1 ⟩$ , respectively, so the reverse sequence recovers $00, 01, 10, 11$ .

Depends on

Used by

Dense-coding procedure Algorithm
Dense-coding correctness and resources Theorem

Dependency tree · two levels

36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Watrous, The Theory of Quantum Information (2018), §6.3.1 (standard reference, not scraped)
Richard Cleve, Quantum Information Processing course notes for QIC 710 / CS 768 / PHYS 767 / CO 681 / AMATH 871 / PMATH 871, version dated October 13, 2026 (standard reference, not scraped)