Hadamard transform on the n-qubit register (R2)

Category: 1-Mathlib (CSD-free).

Phase R2 of specs/nqubit-register-plan.md: the Hadamard transform H^⊗n on the n-qubit register, with entries the product of single-qubit Hadamard entries,

Hn x y = ∏ᵢ hadEntry (xᵢ) (yᵢ) = (-1)^(x·y) / √(2ⁿ),

and the key fact that it sends the all-zeros state to the uniform superposition:

Hn |0ⁿ⟩ = (1/√2)ⁿ · ∑_y |y⟩ (Hn_apply_zero).

This is the first step of every Hadamard-based algorithm (Deutsch–Jozsa, Grover). It needs no unitarity (that is R3, via character orthogonality); only the action on |0ⁿ⟩.

noncomputable def QuantumInfo.hadEntry (a b : Fin 2) : ℂ

The single-qubit Hadamard matrix entry H(a,b) = (-1)^{ab} / √2.

Equations

• QuantumInfo.hadEntry a b = (-1) ^ (↑a * ↑b) / ↑√2

@[simp]

theorem QuantumInfo.hadEntry_zero_right (b : Fin 2) : hadEntry b 0 = (↑√2)⁻¹

noncomputable def QuantumInfo.Hn {n : ℕ} : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The Hadamard transform H^⊗n on the n-qubit register, as a matrix indexed by bitstrings: Hn x y = ∏ᵢ H(xᵢ, yᵢ).

Equations

• QuantumInfo.Hn = Matrix.of fun (x y : Fin n → Fin 2) => ∏ i : Fin n, QuantumInfo.hadEntry (x i) (y i)

@[simp]

theorem QuantumInfo.Hn_apply {n : ℕ} (x y : Fin n → Fin 2) : Hn x y = ∏ i : Fin n, hadEntry (x i) (y i)

noncomputable def QuantumInfo.applyHn {n : ℕ} (ψ : QReg n) : QReg n

The action of the Hadamard transform on a register state.

Equations

• QuantumInfo.applyHn ψ = (Matrix.toEuclideanLin QuantumInfo.Hn) ψ

theorem QuantumInfo.applyHn_apply {n : ℕ} (ψ : QReg n) (y : Fin n → Fin 2) : (applyHn ψ).ofLp y = ∑ x : Fin n → Fin 2, Hn y x * ψ.ofLp x

theorem QuantumInfo.Hn_apply_zero {n : ℕ} (y : Fin n → Fin 2) : (applyHn (basisState 0)).ofLp y = (↑√2)⁻¹ ^ n

Hadamard on the all-zeros state is the uniform superposition. applyHn |0ⁿ⟩ y = (1/√2)ⁿ for every basis outcome y — equal amplitude everywhere.

R3 — character orthogonality ⟹ H^⊗n unitary

The Hadamard transform is unitary (Hn_unitary, Hnᴴ * Hn = 1), so the full output distribution of any Hadamard circuit is a legitimate probability vector — not merely the single all-zeros amplitude of R2.

The route is the per-qubit factorisation rather than a global XOR character sum: the matrix statement (Hnᴴ * Hn) x x' = [x = x'] is the multi-qubit character orthogonality, and it factors over qubits (Finset.prod_univ_sum) into n copies of the single-qubit orthogonality ∑_b H(b,a) H(b,a') = [a = a'] (hadEntry_mul_sum). This avoids defining bitwise XOR on bitstrings; the per-qubit sum is the character sum on Fin 2.

theorem QuantumInfo.hadEntry_comm (a b : Fin 2) : hadEntry a b = hadEntry b a

The single-qubit Hadamard entry is symmetric: H(a,b) = H(b,a).

theorem QuantumInfo.hadEntry_conj (a b : Fin 2) : (starRingEnd ℂ) (hadEntry a b) = hadEntry a b

The single-qubit Hadamard entry is real: conjugation fixes it.

theorem QuantumInfo.sqrt2_mul_self : ↑√2 * ↑√2 = 2

√2 · √2 = 2 over ℂ (the coerced real square root).

theorem QuantumInfo.hadEntry_mul_sum (a a' : Fin 2) : ∑ b : Fin 2, hadEntry b a * hadEntry b a' = if a = a' then 1 else 0

Single-qubit character orthogonality: ∑_{b} H(b,a) H(b,a') = [a = a']. The two columns of the 2×2 Hadamard are orthonormal.

theorem QuantumInfo.Hn_conjTranspose {n : ℕ} : Hn.conjTranspose = Hn

The Hadamard transform is Hermitian: Hnᴴ = Hn (real entries, symmetric).

theorem QuantumInfo.Hn_unitary {n : ℕ} : Hn.conjTranspose * Hn = 1

The Hadamard transform is unitary: Hnᴴ * Hn = 1. This is the multi-qubit character orthogonality; entrywise it reads ∑_y H(x,y) H(y,x') = [x = x'], which factors over qubits into n single-qubit orthogonalities. Hence the output of any Hadamard circuit is a genuine probability vector.

theorem QuantumInfo.Hn_mul_self {n : ℕ} : Hn * Hn = 1

H^⊗n is an involution: applying the Hadamard transform twice is the identity (Hn * Hn = 1), since Hn is both Hermitian and unitary.