TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Dense-coding correctness and resources

Statement

For each input pair $(a, b) \in {0, 1}^{2}$ in the procedure Dense-coding procedure, with $a$ the phase bit and $b$ the flip bit, Alice's encoding $Z_{A}^{a} X_{A}^{b}$ sends $∣ Φ^{+} ⟩$ to the Bell vector $B ∣ a b ⟩$ . Bob's inverse $B^{†}$ therefore returns the computational-basis vector $∣ a b ⟩$ , and the final projective measurement outputs the original two bits with probability one. This realizes two classical output bits using one preshared Bell pair and one transmitted qubit. It is an achievability result, not an optimality claim.

Facts & Assumptions

Given: Bits $a, b \in {0, 1}$ , the preshared $∣ Φ^{+} ⟩$ , and the dense-coding procedure with the stated phase/flip label order.

[A1]

$a$ is the phase bit, $b$ is the flip bit, and the input label is ordered $(a, b)$ .

[F1]

Dense-coding procedure applies $X_{A}^{b}$ then $Z_{A}^{a}$ , sends wire $A$ , then has Bob apply CNOT $A \to B$ , $H_{A}$ , and measure ordered $A, B$ .

[F2]

The Bell vectors defines $Φ^{+}, Ψ^{+}, Φ^{-}, Ψ^{-}$ in label order $00, 01, 10, 11$ .

[F3]

Bell preparation transform and inverse proves $B ∣ 00 ⟩ = Φ^{+}$ , $B ∣ 01 ⟩ = Ψ^{+}$ , $B ∣ 10 ⟩ = Φ^{-}$ , $B ∣ 11 ⟩ = Ψ^{-}$ and that $B^{†}$ decodes these labels.

[F4]

The Pauli matrices gives the exact matrices and basis actions of $X$ and $Z$ .

[F5]

Finite projective measurements assigns outcome weights $tr (ρ P_{a b})$ to computational-basis projectors.

[F6]

Projective measurement outcome weights are probabilities states that these weights are probabilities.

[F7]

The basis-independent trace of an endomorphism of a finite-dimensional vector space defines trace as the sum of diagonal entries in a chosen basis.

[F8]

The computational basis is orthonormal proves that Bob's ordered computational-basis outcomes are orthonormal projectors.

[F9]

Density operator defines a density operator as a non-negative operator with trace one.

Proof

1.1givenA1F2F4algebra

Applying $Z_{A}^{a} X_{A}^{b}$ to $∣ Φ^{+} ⟩ = (∣ 00 ⟩ + ∣ 11 ⟩) / \sqrt{2}$ and using [F4] gives the four cases: $00 \mapsto Φ^{+}$ , $01 \mapsto Ψ^{+}$ , $10 \mapsto Φ^{-}$ , and $11 \mapsto Ψ^{-}$ . In the last case, $Z_{A} X_{A} ∣ 00 ⟩ = - ∣ 10 ⟩$ and $Z_{A} X_{A} ∣ 11 ⟩ = ∣ 01 ⟩$ , so the state is exactly $Ψ^{-}$ in the chosen convention.

2.1step 1.1F2F4algebra

For $x \in {0, 1}$ , [F4] gives $Z^{a} ∣ x ⟩ = (- 1)^{a x} ∣ x ⟩$ . Expanding the left side and then substituting $y = x \oplus b$ gives $(Z^{a} X^{b} \otimes I) ∣ Φ^{+} ⟩ = 2^{- 1 / 2} \sum_{x} (- 1)^{a (x \oplus b)} ∣ x \oplus b, x ⟩ = 2^{- 1 / 2} \sum_{y} (- 1)^{a y} ∣ y, y \oplus b ⟩ = (I \otimes X^{b} Z^{a}) ∣ Φ^{+} ⟩$ . The same matrices give $X Z = - Z X$ , hence $X^{b} Z^{a} = (- 1)^{a b} Z^{a} X^{b}$ . The scalar $λ = (- 1)^{a b}$ leaves the rank-one projector unchanged because $(λ v) (λ v)^{*} = ∣ λ ∣^{2} v v^{*} = v v^{*}$ ; it changes no projective outcome weight, while the direct four-case vectors in step 1.1 fix the exact label phase.

2.2step 1.1F3F5F6F7F8algebra

By [F3], the four encoded vectors in step 1.1 are $B ∣ a b ⟩$ , and $B^{†}$ sends each to $∣ a b ⟩$ . The output projectors are the orthogonal basis projections in [F8]. The rank-one matrix of $∣ a b ⟩$ has a single diagonal entry $1$ at label $(a, b)$ , so its quadratic form is nonnegative and its trace is one by [F7]; it is a density operator by [F9]. Then [F5] and [F7] give weight one at $(a, b)$ and zero at the other labels. By [F6] this is a deterministic output law.

3.1F1algebra∎

The procedure [F1] begins with one shared pair, sends only wire $A$ once, and outputs the two input bits at Bob's measurement. Its instructions contain at most two conditional Pauli gate occurrences for Alice's encoding, one CNOT and one Hadamard for Bob, and two final measured wires. Thus it achieves the stated resource exchange for this procedure; no optimality statement is used.

Depends on

Used by

Entanglement-assisted capacity of a noiseless qubit Example

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)