The swap test (overlap / fidelity estimator)

Category: 3-Local (QM-validity).

The swap test opens the ancilla-interferometry algorithm family (beside the Hadamard-oracle family Deutsch–Jozsa / Simon / Bernstein–Vazirani). One ancilla qubit interferes two system copies ψ, φ through a controlled swap:

H_anc ∘ cSWAP ∘ H_anc on |0⟩ ⊗ ψ ⊗ φ.

Tracking the ancilla:

• H_anc : |0⟩⊗ψ⊗φ ↦ (|0⟩+|1⟩)/√2 ⊗ ψ⊗φ;
• cSWAP : ↦ (|0⟩⊗ψ⊗φ + |1⟩⊗φ⊗ψ)/√2;
• H_anc : ↦ (1/2)[ |0⟩⊗(ψ⊗φ + φ⊗ψ) + |1⟩⊗(ψ⊗φ − φ⊗ψ) ].

The ancilla-0 marginal (swapTestProb0) is the headline:

P(0) = (1/4)‖ψ⊗φ + φ⊗ψ‖² = (1 + |⟨ψ,φ⟩|²)/2 (swap_test_prob),

using the key tensor identity ⟨ψ⊗φ, φ⊗ψ⟩ = ⟨ψ,φ⟩·⟨φ,ψ⟩ = |⟨ψ,φ⟩|². Hence P(0) = 1 when ψ = φ (swap_test_equal) and P(0) = 1/2 when ⟨ψ,φ⟩ = 0 (swap_test_orthogonal): the test reads off |⟨ψ,φ⟩|², the squared overlap / fidelity.

Model. Combined space EuclideanSpace ℂ (Fin 2 × ι × ι) for an arbitrary Fintype ι (the system index — any finite dimension). The two system states ψ φ : EuclideanSpace ℂ ι enter as the product amplitude (a,i,j) ↦ [a=0]·ψ i·φ j (swapInit). The two gates (hadAnc on the ancilla factor via hadEntry, cSwap swapping the two ι factors on ancilla 1) are amplitude functions; the two-Hadamard collapse (hadEntry orthogonality) gives the explicit ancilla-0 amplitude (1/2)(ψ i φ j + φ i ψ j) (swapTest_apply).

Honest scope. This is the exact single-shot output-probability identity — the inner-product-geometry (QM-validity) statement. The estimation (repeating the test to resolve |⟨ψ,φ⟩|² to a target precision) is the statistical wrapper, noted but not formalised here. No tensor caveats beyond the explicit Fin 2 × ι × ι model.

(For ι = Empty the unit hypotheses ‖ψ‖ = 1 are unsatisfiable, so the headlines hold vacuously there; non-vacuous content needs an inhabited system ι.)

Definitions

noncomputable def CSD.Empirical.QM.SwapTest.swapInit {ι : Type u_1} (ψ φ : EuclideanSpace ℂ ι) : Fin 2 × ι × ι → ℂ

|0⟩ ⊗ ψ ⊗ φ: the product amplitude (a,i,j) ↦ [a=0]·ψ i·φ j.

Equations

• CSD.Empirical.QM.SwapTest.swapInit ψ φ p = if p.1 = 0 then ψ.ofLp p.2.1 * φ.ofLp p.2.2 else 0

noncomputable def CSD.Empirical.QM.SwapTest.hadAnc {ι : Type u_1} (s : Fin 2 × ι × ι → ℂ) : Fin 2 × ι × ι → ℂ

Hadamard on the ancilla (Fin 2) factor only: (a,i,j) ↦ ∑_b H(a,b)·state(b,i,j).

Equations

• CSD.Empirical.QM.SwapTest.hadAnc s p = ∑ b : Fin 2, QuantumInfo.hadEntry p.1 b * s (b, p.2.1, p.2.2)

noncomputable def CSD.Empirical.QM.SwapTest.cSwap {ι : Type u_1} (s : Fin 2 × ι × ι → ℂ) : Fin 2 × ι × ι → ℂ

Controlled swap of the two system factors, controlled on ancilla = 1: (a,i,j) ↦ state(a,j,i) if a = 1, else state(a,i,j).

Equations

• CSD.Empirical.QM.SwapTest.cSwap s p = if p.1 = 1 then s (p.1, p.2.2, p.2.1) else s (p.1, p.2.1, p.2.2)

noncomputable def CSD.Empirical.QM.SwapTest.swapTest {ι : Type u_1} (ψ φ : EuclideanSpace ℂ ι) : Fin 2 × ι × ι → ℂ

The swap-test circuit H_anc ∘ cSWAP ∘ H_anc on |0⟩ ⊗ ψ ⊗ φ.

Equations

• CSD.Empirical.QM.SwapTest.swapTest ψ φ = CSD.Empirical.QM.SwapTest.hadAnc (CSD.Empirical.QM.SwapTest.cSwap (CSD.Empirical.QM.SwapTest.hadAnc (CSD.Empirical.QM.SwapTest.swapInit ψ φ)))

noncomputable def CSD.Empirical.QM.SwapTest.swapTestProb0 {ι : Type u_1} [Fintype ι] (ψ φ : EuclideanSpace ℂ ι) : ℝ

The ancilla-0 marginal probability P(0) = ∑_{i,j} ‖swapTest(0,i,j)‖².

Equations

• CSD.Empirical.QM.SwapTest.swapTestProb0 ψ φ = ∑ i : ι, ∑ j : ι, ‖CSD.Empirical.QM.SwapTest.swapTest ψ φ (0, i, j)‖ ^ 2

Amplitude lemmas

theorem CSD.Empirical.QM.SwapTest.swapInit_apply {ι : Type u_1} (ψ φ : EuclideanSpace ℂ ι) (b : Fin 2) (i j : ι) : swapInit ψ φ (b, i, j) = if b = 0 then ψ.ofLp i * φ.ofLp j else 0

theorem CSD.Empirical.QM.SwapTest.hadAnc_apply {ι : Type u_1} (s : Fin 2 × ι × ι → ℂ) (a : Fin 2) (i j : ι) : hadAnc s (a, i, j) = ∑ b : Fin 2, QuantumInfo.hadEntry a b * s (b, i, j)

theorem CSD.Empirical.QM.SwapTest.cSwap_apply {ι : Type u_1} (s : Fin 2 × ι × ι → ℂ) (a : Fin 2) (i j : ι) : cSwap s (a, i, j) = if a = 1 then s (a, j, i) else s (a, i, j)

theorem CSD.Empirical.QM.SwapTest.hadEntry_zero_left (b : Fin 2) : QuantumInfo.hadEntry 0 b = (↑√2)⁻¹

H(0,b) = (√2)⁻¹ (the all-zero ancilla row).

theorem CSD.Empirical.QM.SwapTest.had1_apply {ι : Type u_1} (ψ φ : EuclideanSpace ℂ ι) (a : Fin 2) (i j : ι) : hadAnc (swapInit ψ φ) (a, i, j) = (↑√2)⁻¹ * (ψ.ofLp i * φ.ofLp j)

After the first Hadamard the ancilla is in a uniform superposition over the unchanged product: hadAnc (swapInit ψ φ) (a,i,j) = (√2)⁻¹·ψ i·φ j for every a.

theorem CSD.Empirical.QM.SwapTest.cswap_had1_apply {ι : Type u_1} (ψ φ : EuclideanSpace ℂ ι) (a : Fin 2) (i j : ι) : cSwap (hadAnc (swapInit ψ φ)) (a, i, j) = if a = 1 then (↑√2)⁻¹ * (ψ.ofLp j * φ.ofLp i) else (↑√2)⁻¹ * (ψ.ofLp i * φ.ofLp j)

After the controlled swap the two pointer branches carry the two orderings: ancilla 1 swaps i,j.

theorem CSD.Empirical.QM.SwapTest.swapTest_apply {ι : Type u_1} (ψ φ : EuclideanSpace ℂ ι) (i j : ι) : swapTest ψ φ (0, i, j) = 1 / 2 * (ψ.ofLp i * φ.ofLp j + φ.ofLp i * ψ.ofLp j)

The ancilla-0 amplitude after the full circuit. The two-Hadamard collapse on the ancilla (hadEntry orthogonality) leaves the symmetric combination:

swapTest ψ φ (0,i,j) = (1/2)(ψ i φ j + φ i ψ j).

Inner-product infrastructure

theorem CSD.Empirical.QM.SwapTest.inner_eq_sum {ι : Type u_1} [Fintype ι] (x y : EuclideanSpace ℂ ι) : inner ℂ x y = ∑ i : ι, (starRingEnd ((fun (x : ι) => ℂ) i)) (x.ofLp i) * y.ofLp i

The Euclidean inner product in coordinates: ⟨x,y⟩ = ∑ i, conj (x i) · y i.

theorem CSD.Empirical.QM.SwapTest.mul_conj_eq (z : ℂ) : z * (starRingEnd ℂ) z = ↑(‖z‖ ^ 2)

z · conj z = ‖z‖² (the Complex.ofReal form, used to keep the cast atom canonical).

The headline

theorem CSD.Empirical.QM.SwapTest.swap_test_prob {ι : Type u_1} [Fintype ι] (ψ φ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) : swapTestProb0 ψ φ = (1 + ‖inner ℂ ψ φ‖ ^ 2) / 2

Swap test (output-probability identity). For unit states ψ, φ, the ancilla-0 marginal probability is (1 + |⟨ψ,φ⟩|²)/2. The cross terms factor through the tensor identity ⟨ψ⊗φ, φ⊗ψ⟩ = ⟨ψ,φ⟩·⟨φ,ψ⟩ = ‖⟨ψ,φ⟩‖² (conjugate-linearity in the first argument fixes the order).

theorem CSD.Empirical.QM.SwapTest.swap_test_equal {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) : swapTestProb0 ψ ψ = 1

Equal states: P(0) = 1 (overlap 1).

theorem CSD.Empirical.QM.SwapTest.swap_test_orthogonal {ι : Type u_1} [Fintype ι] (ψ φ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) (h : inner ℂ ψ φ = 0) : swapTestProb0 ψ φ = 1 / 2

Orthogonal states: P(0) = 1/2 (overlap 0).