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.

Teleportation correctness and resources

Statement

For every normalized qubit input, the procedure Qubit teleportation procedure has four outcomes, each of probability $1 / 4$ . Conditioned on outcome $(a, b)$ , the receiver's byproduct is $X^{b} Z^{a} ∣ ψ ⟩$ and the prescribed correction returns $∣ ψ ⟩$ exactly. The same corrected branch identity holds when the input is entangled with any finite reference. Under the separate resource record Teleportation protocol resource record, the procedure uses one preshared Bell-pair resource and two classical bits sent from Alice to Bob; it sends no qubit during the protocol and makes no optimality claim.

Facts & Assumptions

Given: A normalized input qubit, the shared Bell pair, and the procedure's ordered measurement and correction instructions.

[A1]

The input qubit vector is normalized.

[F1]

Qubit teleportation procedure uses the resource $∣ Φ^{+} ⟩_{B C}$ , applies CNOT then $H_{A}$ , measures ordered wires $A, B$ , sends $(a, b)$ , and applies $X_{C}^{b}$ then $Z_{C}^{a}$ .

[F2]

Teleportation outcomes are equiprobable proves $\Pr [(a, b)] = 1 / 4$ for every label.

[F3]

Teleportation Pauli correction identity proves that the byproduct $X^{b} Z^{a}$ is inverted by $Z^{a} X^{b}$ .

[F4]

Teleportation preserves a finite reference proves the corrected output equals the input jointly with every finite reference.

[F5]

Teleportation protocol resource record records the shared pair, two classical bits, zero transmitted qubits, gate occurrences, and measurement record as distinct resources.

[F6]

Teleportation Bell-basis expansion gives each measured branch vector as $\frac{1}{2} ∣ a b ⟩ \otimes X^{b} Z^{a} ∣ ψ ⟩$ .

Proof

1.1givenA1F1F2F6

By [F2], each of the four possible labels has probability $1 / 4$ , so every branch has positive probability and the conditional branch is defined. The Bell expansion [F6] identifies its receiver vector as $X^{b} Z^{a} ∣ ψ ⟩$ .

2.1step 1.1F1F3

Applying the correction from [F1] to the byproduct in step 1.1 gives $Z^{a} X^{b} X^{b} Z^{a} ∣ ψ ⟩ = ∣ ψ ⟩$ by [F3]. Hence every branch has the exact corrected output.

3.1step 2.1F4

For a joint input with any finite reference, the same branchwise output statement is the conclusion of [F4]. This verifies the protocol preserves the full input-reference vector, not only its reduced input state.

4.1F1F5∎

The resource record [F5] separates one preshared Bell-pair use, the two classical bits sent from Alice to Bob, zero qubits sent after the pair is available, the two Alice gates, the two-bit Alice measurement record, and up to two conditional Bob Pauli gates. These are counts of the stated procedure only; no lower bound or physical preparation claim follows.

Depends on

Used by

Teleportation branch and Pauli correction Example

Dependency tree · two levels

23 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)