The Hadamard test (expectation-value estimator)

Category: 3-Local (QM-validity).

The Hadamard test is the parent of the swap test in the ancilla-interferometry family: one ancilla qubit interferes a system state ψ with its image Uψ under a system operator U through a controlled-U:

H_anc ∘ cU ∘ H_anc on |0⟩ ⊗ ψ.

Tracking the ancilla:

• H_anc : |0⟩⊗ψ ↦ (|0⟩+|1⟩)/√2 ⊗ ψ;
• cU : ↦ (|0⟩⊗ψ + |1⟩⊗Uψ)/√2 (apply U on the system iff ancilla = 1);
• H_anc : ↦ (1/2)[ |0⟩⊗(ψ+Uψ) + |1⟩⊗(ψ−Uψ) ].

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

P(0) = (1/4)‖ψ+Uψ‖² = (1 + Re⟨ψ,Uψ⟩)/2 (hadamard_test_prob),

for unit ψ and unit Uψ. The two cross terms combine as ⟨ψ,Uψ⟩ + ⟨Uψ,ψ⟩ = ⟨ψ,Uψ⟩ + conj⟨ψ,Uψ⟩ = 2·Re⟨ψ,Uψ⟩. So the ancilla-0 frequency estimates Re⟨ψ,Uψ⟩. Symmetrically P(1) = (1 − Re⟨ψ,Uψ⟩)/2 (hadamard_test_prob1), hence the sign reading P(0) − P(1) = Re⟨ψ,Uψ⟩ (hadamard_test_prob_diff), and P(0) = 1 when Uψ = ψ (hadamard_test_eq_one).

Model. Combined space EuclideanSpace ℂ (Fin 2 × ι) for an arbitrary Fintype ι (the system index — any finite dimension). The system state ψ : EuclideanSpace ℂ ι enters as (a,i) ↦ [a=0]·ψ i (hadInit); U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι is a plain ℂ-linear system operator. The two gates (hadAnc on the ancilla factor via hadEntry, cU applying U to the system slice on ancilla 1) are amplitude functions; the two-Hadamard collapse (hadEntry orthogonality) gives the explicit ancilla-0 amplitude (1/2)(ψ i + (Uψ) i) (hadTest_apply).

The swap test is this at U = SWAP on the doubled register. Taking ι := κ × κ, U := swap (the (i,j) ↦ (j,i) linear map), ψ := ψ⊗φ, one has Re⟨ψ⊗φ, swap(ψ⊗φ)⟩ = Re⟨ψ⊗φ, φ⊗ψ⟩ = Re(⟨ψ,φ⟩·⟨φ,ψ⟩) = ‖⟨ψ,φ⟩‖² (already real), so hadamard_test_prob at U = swap is (1 + ‖⟨ψ,φ⟩‖²)/2 = swap_test_prob. The genuine unification is swap_test_via_hadamard below.

The Im variant is the standard S†-phase circuit: inserting S† = diag(1,−i) on the ancilla before the second Hadamard gives P(0) = (1 + Im⟨ψ,Uψ⟩)/2. It is the same expansion with a −i weight on the |1⟩ branch; not formalised here.

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 Re⟨ψ,Uψ⟩ to a target precision) is the statistical wrapper, noted but not formalised here. The hypothesis ‖Uψ‖ = 1 is automatic for unitary U and keeps U a plain linear map.

(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.HadamardTest.hadInit {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) : Fin 2 × ι → ℂ

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

Equations

• CSD.Empirical.QM.HadamardTest.hadInit ψ p = if p.1 = 0 then ψ.ofLp p.2 else 0

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

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

Equations

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

noncomputable def CSD.Empirical.QM.HadamardTest.sliceAt {ι : Type u_1} (s : Fin 2 × ι → ℂ) (a : Fin 2) : EuclideanSpace ℂ ι

The system slice at ancilla value a: (fun j => state (a,j)) : EuclideanSpace ℂ ι.

Equations

• CSD.Empirical.QM.HadamardTest.sliceAt s a = WithLp.toLp 2 fun (j : ι) => s (a, j)

noncomputable def CSD.Empirical.QM.HadamardTest.cU {ι : Type u_1} (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (s : Fin 2 × ι → ℂ) : Fin 2 × ι → ℂ

Controlled-U on the system slice, controlled on ancilla = 1: (a,i) ↦ (U (sliceAt state 1)) i if a = 1, else state (a,i).

Equations

• CSD.Empirical.QM.HadamardTest.cU U s p = if p.1 = 1 then (U (CSD.Empirical.QM.HadamardTest.sliceAt s 1)).ofLp p.2 else s p

noncomputable def CSD.Empirical.QM.HadamardTest.hadTest {ι : Type u_1} (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) : Fin 2 × ι → ℂ

The Hadamard-test circuit H_anc ∘ cU ∘ H_anc on |0⟩ ⊗ ψ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.Empirical.QM.HadamardTest.hadTestProb0 {ι : Type u_1} [Fintype ι] (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) : ℝ

The ancilla-0 marginal probability P(0) = ∑_i ‖hadTest(0,i)‖².

Equations

• CSD.Empirical.QM.HadamardTest.hadTestProb0 U ψ = ∑ i : ι, ‖CSD.Empirical.QM.HadamardTest.hadTest U ψ (0, i)‖ ^ 2

noncomputable def CSD.Empirical.QM.HadamardTest.hadTestProb1 {ι : Type u_1} [Fintype ι] (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) : ℝ

The ancilla-1 marginal probability P(1) = ∑_i ‖hadTest(1,i)‖².

Equations

• CSD.Empirical.QM.HadamardTest.hadTestProb1 U ψ = ∑ i : ι, ‖CSD.Empirical.QM.HadamardTest.hadTest U ψ (1, i)‖ ^ 2

Amplitude lemmas

theorem CSD.Empirical.QM.HadamardTest.hadInit_apply {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (b : Fin 2) (i : ι) : hadInit ψ (b, i) = if b = 0 then ψ.ofLp i else 0

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

theorem CSD.Empirical.QM.HadamardTest.sliceAt_apply {ι : Type u_1} (s : Fin 2 × ι → ℂ) (a : Fin 2) (j : ι) : (sliceAt s a).ofLp j = s (a, j)

theorem CSD.Empirical.QM.HadamardTest.cU_apply {ι : Type u_1} (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (s : Fin 2 × ι → ℂ) (a : Fin 2) (i : ι) : cU U s (a, i) = if a = 1 then (U (sliceAt s 1)).ofLp i else s (a, i)

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

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

theorem CSD.Empirical.QM.HadamardTest.hadEntry_one_one : QuantumInfo.hadEntry 1 1 = -(↑√2)⁻¹

H(1,1) = -(√2)⁻¹ (the (-1) interference entry).

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

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

theorem CSD.Empirical.QM.HadamardTest.cU_had1_apply {ι : Type u_1} (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) (a : Fin 2) (i : ι) : cU U (hadAnc (hadInit ψ)) (a, i) = if a = 1 then (↑√2)⁻¹ * (U ψ).ofLp i else (↑√2)⁻¹ * ψ.ofLp i

After the controlled-U the two pointer branches carry ψ and Uψ: ancilla 1 applies U.

theorem CSD.Empirical.QM.HadamardTest.hadTest_apply {ι : Type u_1} (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) (i : ι) : hadTest U ψ (0, i) = 1 / 2 * (ψ.ofLp i + (U ψ).ofLp i)

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

hadTest U ψ (0,i) = (1/2)(ψ i + (Uψ) i).

theorem CSD.Empirical.QM.HadamardTest.hadTest_apply_one {ι : Type u_1} (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) (i : ι) : hadTest U ψ (1, i) = 1 / 2 * (ψ.ofLp i - (U ψ).ofLp i)

The ancilla-1 amplitude after the full circuit. The (-1) interference entry flips the sign of the Uψ branch:

hadTest U ψ (1,i) = (1/2)(ψ i − (Uψ) i).

Inner-product infrastructure

theorem CSD.Empirical.QM.HadamardTest.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.HadamardTest.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.HadamardTest.hadamard_test_prob {ι : Type u_1} [Fintype ι] (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (hU : ‖U ψ‖ = 1) : hadTestProb0 U ψ = (1 + (inner ℂ ψ (U ψ)).re) / 2

Hadamard test (output-probability identity). For a unit state ψ with unit image Uψ, the ancilla-0 marginal probability is (1 + Re⟨ψ,Uψ⟩)/2. The two cross terms combine as ⟨ψ,Uψ⟩ + ⟨Uψ,ψ⟩ = ⟨ψ,Uψ⟩ + conj⟨ψ,Uψ⟩ = 2·Re⟨ψ,Uψ⟩ (conjugate-linearity in the first argument fixes the order).

theorem CSD.Empirical.QM.HadamardTest.hadamard_test_prob1 {ι : Type u_1} [Fintype ι] (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (hU : ‖U ψ‖ = 1) : hadTestProb1 U ψ = (1 - (inner ℂ ψ (U ψ)).re) / 2

Hadamard test, ancilla-1 marginal. P(1) = (1 − Re⟨ψ,Uψ⟩)/2.

theorem CSD.Empirical.QM.HadamardTest.hadamard_test_prob_diff {ι : Type u_1} [Fintype ι] (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (hU : ‖U ψ‖ = 1) : hadTestProb0 U ψ - hadTestProb1 U ψ = (inner ℂ ψ (U ψ)).re

Sign reading. P(0) − P(1) = Re⟨ψ,Uψ⟩: the difference of the two ancilla frequencies is exactly the estimated expectation value.

theorem CSD.Empirical.QM.HadamardTest.hadamard_test_eq_one {ι : Type u_1} [Fintype ι] (U : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (h : U ψ = ψ) : hadTestProb0 U ψ = 1

Fixed point: Uψ = ψ ⟹ P(0) = 1 (the estimator reads Re⟨ψ,ψ⟩ = 1).

The swap test as the Hadamard test at U = SWAP

The swap test (Algorithms/SwapTest.lean, model EuclideanSpace ℂ (Fin 2 × κ × κ)) is the Hadamard test at ι := κ × κ, U := swapMap (the (i,j) ↦ (j,i) linear reindexing), ψ := ψ⊗φ (tensorEuc). The two combined spaces coincide (Fin 2 × κ × κ = Fin 2 × (κ × κ)), and at the amplitude level the controlled-U collapses to the controlled-swap (hadTest_swap_apply), so the two ancilla-0 probabilities are literally equal (swap_test_via_hadamard). Its closed form is the overlap (1 + ‖⟨ψ,φ⟩‖²)/2 (hadamard_test_swap_closed), derived natively through hadamard_test_prob: the inner identity Re⟨ψ⊗φ, swap(ψ⊗φ)⟩ = Re(⟨ψ,φ⟩·⟨φ,ψ⟩) = ‖⟨ψ,φ⟩‖² (re_inner_tensorEuc_swap) together with the tensor unit norms ‖ψ⊗φ‖ = ‖swap(ψ⊗φ)‖ = 1 (tensorEuc_norm_one, swapMap_tensorEuc_norm_one). No dependence on SwapTest.swap_test_prob.

noncomputable def CSD.Empirical.QM.HadamardTest.swapMap {κ : Type u_2} : EuclideanSpace ℂ (κ × κ) →ₗ[ℂ] EuclideanSpace ℂ (κ × κ)

The system swap (i,j) ↦ (j,i) as a ℂ-linear self-map of EuclideanSpace ℂ (κ × κ) (the system operator that turns the Hadamard test into the swap test).

Equations

• CSD.Empirical.QM.HadamardTest.swapMap = { toFun := fun (v : EuclideanSpace ℂ (κ × κ)) => WithLp.toLp 2 fun (p : κ × κ) => v.ofLp (p.2, p.1), map_add' := ⋯, map_smul' := ⋯ }

theorem CSD.Empirical.QM.HadamardTest.swapMap_apply {κ : Type u_2} (v : EuclideanSpace ℂ (κ × κ)) (i j : κ) : (swapMap v).ofLp (i, j) = v.ofLp (j, i)

noncomputable def CSD.Empirical.QM.HadamardTest.tensorEuc {κ : Type u_2} (ψ φ : EuclideanSpace ℂ κ) : EuclideanSpace ℂ (κ × κ)

The product state ψ⊗φ as an EuclideanSpace ℂ (κ × κ): (i,j) ↦ ψ i · φ j.

Equations

• CSD.Empirical.QM.HadamardTest.tensorEuc ψ φ = WithLp.toLp 2 fun (p : κ × κ) => ψ.ofLp p.1 * φ.ofLp p.2

theorem CSD.Empirical.QM.HadamardTest.tensorEuc_apply {κ : Type u_2} (ψ φ : EuclideanSpace ℂ κ) (i j : κ) : (tensorEuc ψ φ).ofLp (i, j) = ψ.ofLp i * φ.ofLp j

theorem CSD.Empirical.QM.HadamardTest.hadTest_swap_apply {κ : Type u_2} (ψ φ : EuclideanSpace ℂ κ) (i j : κ) : hadTest swapMap (tensorEuc ψ φ) (0, i, j) = SwapTest.swapTest ψ φ (0, i, j)

Amplitude unification. At U = swapMap, ψ = ψ⊗φ the Hadamard-test ancilla-0 amplitude equals the swap-test amplitude: both are (1/2)(ψ i φ j + ψ j φ i).

theorem CSD.Empirical.QM.HadamardTest.swap_test_via_hadamard {κ : Type u_2} [Fintype κ] (ψ φ : EuclideanSpace ℂ κ) : SwapTest.swapTestProb0 ψ φ = hadTestProb0 swapMap (tensorEuc ψ φ)

The swap test is the Hadamard test at U = SWAP. The two ancilla-0 marginal probabilities are literally equal (sum over κ × κ of the equal per-cell amplitudes).

theorem CSD.Empirical.QM.HadamardTest.inner_tensorEuc {κ : Type u_2} [Fintype κ] (ψ φ ψ' φ' : EuclideanSpace ℂ κ) : inner ℂ (tensorEuc ψ φ) (tensorEuc ψ' φ') = inner ℂ ψ ψ' * inner ℂ φ φ'

Tensor inner product factorisation: ⟨ψ⊗φ, ψ'⊗φ'⟩ = ⟨ψ,ψ'⟩·⟨φ,φ'⟩ (Fubini split of the κ × κ coordinate sum into a product of two κ-sums).

theorem CSD.Empirical.QM.HadamardTest.swapMap_tensorEuc {κ : Type u_2} (ψ φ : EuclideanSpace ℂ κ) : swapMap (tensorEuc ψ φ) = tensorEuc φ ψ

swap(ψ⊗φ) = φ⊗ψ (the swap reindexing exchanges the two factors).

theorem CSD.Empirical.QM.HadamardTest.tensorEuc_norm_one {κ : Type u_2} [Fintype κ] (ψ φ : EuclideanSpace ℂ κ) (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) : ‖tensorEuc ψ φ‖ = 1

Tensor unit norm: ‖ψ⊗φ‖ = 1 for unit ψ, φ (via ‖ψ⊗φ‖² = ‖ψ‖²·‖φ‖²).

theorem CSD.Empirical.QM.HadamardTest.swapMap_tensorEuc_norm_one {κ : Type u_2} [Fintype κ] (ψ φ : EuclideanSpace ℂ κ) (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) : ‖swapMap (tensorEuc ψ φ)‖ = 1

Swapped tensor unit norm: ‖swap(ψ⊗φ)‖ = 1 (= ‖φ⊗ψ‖); discharges the ‖Uψ‖ = 1 hypothesis of hadamard_test_prob at U = swapMap.

theorem CSD.Empirical.QM.HadamardTest.re_inner_tensorEuc_swap {κ : Type u_2} [Fintype κ] (ψ φ : EuclideanSpace ℂ κ) : (inner ℂ (tensorEuc ψ φ) (swapMap (tensorEuc ψ φ))).re = ‖inner ℂ ψ φ‖ ^ 2

The key inner identity: Re⟨ψ⊗φ, swap(ψ⊗φ)⟩ = ‖⟨ψ,φ⟩‖². Since ⟨ψ⊗φ, φ⊗ψ⟩ = ⟨ψ,φ⟩·⟨φ,ψ⟩ = ⟨ψ,φ⟩·conj⟨ψ,φ⟩ = ‖⟨ψ,φ⟩‖² is already real, Re is the identity.

theorem CSD.Empirical.QM.HadamardTest.hadamard_test_swap_closed {κ : Type u_2} [Fintype κ] (ψ φ : EuclideanSpace ℂ κ) (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) : hadTestProb0 swapMap (tensorEuc ψ φ) = (1 + ‖inner ℂ ψ φ‖ ^ 2) / 2

The Hadamard test at U = SWAP computes the overlap. Derived natively through hadamard_test_prob (no SwapTest.swap_test_prob): the ancilla-0 probability on ψ⊗φ is (1 + ‖⟨ψ,φ⟩‖²)/2 — the squared overlap / fidelity — via the inner identity re_inner_tensorEuc_swap and the tensor unit norms.