Teleportation

Sending a quantum state with two ordinary bits, checked for every case.

teleportation.js · output · proof · check · try it in the playground

The question

In quantum teleportation, Alice wants to give Bob a qubit (a quantum bit) without sending the qubit itself. They share a linked pair of qubits in advance. Alice makes a measurement, phones Bob two ordinary bits (one of four outcomes, 0 to 3), and Bob applies a fix that depends on the outcome.

Does Bob always end up with exactly the state Alice had — for every state and every outcome?

A simplified quantum world

The program uses discrete quantum theory: a toy version where amplitudes are just “there or not”, and two ways of reaching the same result cancel each other out. A result survives only if it can be reached an odd number of ways.

It keeps the strange parts — superposition, interference, entanglement — small enough to check exhaustively. Three states are tested: zero, one, and plus (both at once).

What we tell eyecode

// … the shared pair, Alice's measurement and Bob's fixes
// Bob's qubit has amplitude 1 on Z when an odd number of ways lead there.
implied_by(received(S, M, Z), [qubit(Z), findall(Path, path(S, M, Z, Path), Paths), odd(Paths)])
// What Bob holds after each outcome, for each state Alice could send.
implies(
  [name(S), outcome(M), findall(Z, received(S, M, Z), Received)],
  teleported(S, M, Received),
)
// Bob must hold exactly the state Alice sent, whatever the outcome.
// …
contradiction(teleported(S, _, Received), sent(S, Sent), not_identical(Received, Sent))

A state is written as the list of basis values it contains, so plus is ['false', 'true']. A path is one way for Alice’s state to end up as one of Bob’s values; Bob’s fix for outcome M undoes the basis Alice measured in. findall gathers all answers. The contradiction rule is a safety alarm: if Bob’s state ever differs from Alice’s, the run stops with exit code 65.

What eyecode concludes

teleported('zero', 0, ['false'])
teleported('one', 0, ['true'])
teleported('plus', 0, ['false', 'true'])
teleported('plus', 3, ['false', 'true'])

…12 answers in all: 3 states × 4 outcomes. In every one, Bob holds exactly what Alice sent (zero is ['false'], one is ['true'], plus is both), and the alarm never fires.

Why: the proof in plain words

For each of the 12 cases, the proof says:

S is one of the three states — a fact we gave.
M is one of the four outcomes — a fact we gave.
Gathering all the values Bob can receive gives this list — collected.
So this is what Bob holds — rule 37.

Step 3 is where the quantum work happens, and it is a “find all” step.

Checked, not just claimed

19 steps are confirmed against the program lines they cite.
12 steps are taken on trust as collected obligations: for each case, that the list of values Bob receives is complete. A proof can show what is in a list, not that nothing was left out, so the checker records this.
The checker looked for evidence against all 12 lists and found none.

Verdict: checked_with_obligations. 31 steps, 12 on trust. Honestly put: the counting of paths sits inside those 12 obligations.

Try it

eyecode examples/teleportation.js            # the answers
eyecode --proof examples/teleportation.js    # answers with their proof

Break Bob’s fix for outcome 0: in implied_by(bob(0, Y, Z), kg(Y, Z)) replace kg(Y, Z) with id(Y, Z). Now outcome 0 leaves Bob with the wrong state (zero arrives as ['true']), so after the answers eyecode prints 'false' for the contradiction and exits with code 65.

Takeaway

Even a quantum protocol can be checked case by case with a few rules. eyecode covers all 12 cases, and is upfront that the “all answers” lists are the part you are trusting.