Empirical/QM: Wiesner quantum money (unforgeability)

Category: 3-Local (promotion-ready to 2-Framework on demand).

Wiesner's quantum money (Wiesner 1983): a banknote carries qubits each prepared in one of the four BB84 states, secret to the bank. A forger who could duplicate an unknown banknote would, in particular, clone a single unknown qubit drawn from two non-orthogonal alternatives — which the no-cloning theorem forbids. Unforgeability is therefore a corollary of no-cloning.

This file makes the witness concrete: the two non-orthogonal money states |0⟩ and |+⟩ in EuclideanSpace ℂ (Fin 2) satisfy ⟨0|+⟩ = 1/√2 ∉ {0, 1}, so no_universal_cloner_of_witness (Empirical/QM/NoCloning.lean) rules out any forging isometry that clones both against a fixed blank. The result is not a reworded alias of no-cloning: the content is the proved non-orthogonality of a named, operationally meaningful state pair.

Source

Wiesner 1983, SIGACT News 15(1), 78 ("Conjugate Coding"); unforgeability via Wootters-Zurek 1982 / Dieks 1982 no-cloning.

noncomputable def CSD.Empirical.QuantumMoney.ket0 : EuclideanSpace ℂ (Fin 2)

Money state |0⟩ = e₀.

Equations

• CSD.Empirical.QuantumMoney.ket0 = EuclideanSpace.single 0 1

noncomputable def CSD.Empirical.QuantumMoney.ketPlus : EuclideanSpace ℂ (Fin 2)

Money state |+⟩ = (e₀ + e₁)/√2.

Equations

• CSD.Empirical.QuantumMoney.ketPlus = (↑√2)⁻¹ • (EuclideanSpace.single 0 1 + EuclideanSpace.single 1 1)

theorem CSD.Empirical.QuantumMoney.half : (↑√2)⁻¹ * (↑√2)⁻¹ = 1 / 2

(√2⁻¹)² = ½, the only nonalgebraic fact used below.

theorem CSD.Empirical.QuantumMoney.ket0_inner_self : inner ℂ ket0 ket0 = 1

⟨0|0⟩ = 1, used to get ‖|0⟩‖ = 1.

theorem CSD.Empirical.QuantumMoney.ket0_unit : ‖ket0‖ = 1

‖|0⟩‖ = 1.

theorem CSD.Empirical.QuantumMoney.wiesner_inner : inner ℂ ket0 ketPlus = (↑√2)⁻¹

⟨0|+⟩ = 1/√2.

theorem CSD.Empirical.QuantumMoney.ketPlus_inner_self : inner ℂ ketPlus ketPlus = 1

⟨+|+⟩ = 1, used to get ‖|+⟩‖ = 1.

theorem CSD.Empirical.QuantumMoney.ketPlus_unit : ‖ketPlus‖ = 1

‖|+⟩‖ = 1.

theorem CSD.Empirical.QuantumMoney.wiesner_nonorthogonal : inner ℂ ket0 ketPlus ≠ 0 ∧ inner ℂ ket0 ketPlus ≠ 1

The Wiesner states are non-orthogonal and not equal up to phase: ⟨0|+⟩ ∉ {0, 1}. This is the witness that drives unforgeability.

theorem CSD.Empirical.QuantumMoney.quantum_money_unforgeable {Htensor : Type u_1} [NormedAddCommGroup Htensor] [InnerProductSpace ℂ Htensor] (tensor : EuclideanSpace ℂ (Fin 2) → EuclideanSpace ℂ (Fin 2) → Htensor) (h_tensor_inner : ∀ (a b c d : EuclideanSpace ℂ (Fin 2)), inner ℂ (tensor a b) (tensor c d) = inner ℂ a c * inner ℂ b d) (e0 : EuclideanSpace ℂ (Fin 2)) (he0 : ‖e0‖ = 1) : ¬∃ (U : Htensor → Htensor), (∀ (x y : Htensor), inner ℂ (U x) (U y) = inner ℂ x y) ∧ U (tensor ket0 e0) = tensor ket0 ket0 ∧ U (tensor ketPlus e0) = tensor ketPlus ketPlus

Quantum money unforgeability (Wiesner). Over any tensor structure with the inner-product factorisation ⟨tensor a b, tensor c d⟩ = ⟨a,c⟩·⟨b,d⟩ and a fixed unit blank e0 : Htensor-side input space, no isometry can forge (clone) both Wiesner money states |0⟩ and |+⟩ against the same blank. Immediate from no_universal_cloner_of_witness applied to the proved non-orthogonality witness wiesner_nonorthogonal.

H := EuclideanSpace ℂ (Fin 2) is the single-qubit money space; the tensor target Htensor and the factorising tensor are supplied by the caller (e.g. the Kronecker product on EuclideanSpace ℂ (Fin 2 × Fin 2)), exactly as in no_cloning_two_state.