Deutsch–Jozsa (R4)

Category: 3-Local (QM-validity).

The Deutsch–Jozsa algorithm (phase R4 of specs/nqubit-register-plan.md): one query to an oracle for f : {0,1}ⁿ → {0,1} decides whether f is constant or balanced. The circuit is H^⊗n ∘ U_f ∘ H^⊗n on |0ⁿ⟩, with U_f the phase oracle |x⟩ ↦ (-1)^{f(x)}|x⟩.

The amplitude of the all-zeros outcome after the circuit is (1/2ⁿ) ∑ₓ (-1)^{f(x)} (djAmplitude_zero), so the Born probability of measuring |0ⁿ⟩ is:

• 1 if f is constant (deutsch_jozsa_constant) — the amplitude is ±1;
• 0 if f is balanced (deutsch_jozsa_balanced) — the amplitude is 0.

One measurement therefore discriminates the two cases with certainty.

Honest scope. This is the discrimination statement, which needs only Hn_apply_zero (R2) and the diagonal oracle — not Hn unitarity. Unitarity (R3, character orthogonality) is what makes the full output distribution a normalised probability vector; the prob(0ⁿ) = 1 vs 0 discrimination here is self-contained as a squared-amplitude computation.

theorem CSD.Empirical.QM.DeutschJozsa.neg_one_pow_fin (a : Fin 2) : (-1) ^ ↑a = if a = 0 then 1 else -1

(-1)^{a} for a bit a : Fin 2, as a complex sign.

theorem CSD.Empirical.QM.DeutschJozsa.inv_sqrt2_sq : (↑√2)⁻¹ ^ 2 = 2⁻¹

(√2⁻¹)² = 2⁻¹.

theorem CSD.Empirical.QM.DeutschJozsa.inv_sqrt2_pow_mul (n : ℕ) : (↑√2)⁻¹ ^ n * (↑√2)⁻¹ ^ n = (2 ^ n)⁻¹

(√2⁻¹)ⁿ · (√2⁻¹)ⁿ = (2ⁿ)⁻¹.

noncomputable def CSD.Empirical.QM.DeutschJozsa.phaseOracle {n : ℕ} (f : (Fin n → Fin 2) → Fin 2) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The phase oracle U_f : |x⟩ ↦ (-1)^{f(x)} |x⟩ for f : {0,1}ⁿ → {0,1}.

Equations

• CSD.Empirical.QM.DeutschJozsa.phaseOracle f = Matrix.diagonal fun (x : Fin n → Fin 2) => (-1) ^ ↑(f x)

noncomputable def CSD.Empirical.QM.DeutschJozsa.applyUf {n : ℕ} (f : (Fin n → Fin 2) → Fin 2) (ψ : QuantumInfo.QReg n) : QuantumInfo.QReg n

The phase oracle's action on a register state.

Equations

• CSD.Empirical.QM.DeutschJozsa.applyUf f ψ = (Matrix.toEuclideanLin (CSD.Empirical.QM.DeutschJozsa.phaseOracle f)) ψ

theorem CSD.Empirical.QM.DeutschJozsa.applyUf_apply {n : ℕ} (f : (Fin n → Fin 2) → Fin 2) (ψ : QuantumInfo.QReg n) (y : Fin n → Fin 2) : (applyUf f ψ).ofLp y = (-1) ^ ↑(f y) * ψ.ofLp y

theorem CSD.Empirical.QM.DeutschJozsa.Hn_zero_apply {n : ℕ} (y : Fin n → Fin 2) : QuantumInfo.Hn 0 y = (↑√2)⁻¹ ^ n

Hn 0ⁿ y = (√2⁻¹)ⁿ (the all-zeros row of the Hadamard transform).

noncomputable def CSD.Empirical.QM.DeutschJozsa.djCircuit {n : ℕ} (f : (Fin n → Fin 2) → Fin 2) (ψ : QuantumInfo.QReg n) : QuantumInfo.QReg n

The Deutsch–Jozsa circuit H^⊗n ∘ U_f ∘ H^⊗n.

Equations

• CSD.Empirical.QM.DeutschJozsa.djCircuit f ψ = QuantumInfo.applyHn (CSD.Empirical.QM.DeutschJozsa.applyUf f (QuantumInfo.applyHn ψ))

theorem CSD.Empirical.QM.DeutschJozsa.djAmplitude_zero {n : ℕ} (f : (Fin n → Fin 2) → Fin 2) : (djCircuit f (QuantumInfo.basisState 0)).ofLp 0 = (2 ^ n)⁻¹ * ∑ x : Fin n → Fin 2, (-1) ^ ↑(f x)

The all-zeros amplitude after the circuit is (1/2ⁿ) ∑ₓ (-1)^{f(x)}.

def CSD.Empirical.QM.DeutschJozsa.Balanced {n : ℕ} (f : (Fin n → Fin 2) → Fin 2) : Prop

A function f : {0,1}ⁿ → {0,1} is balanced if it is 0 on exactly half its inputs.

Equations

• CSD.Empirical.QM.DeutschJozsa.Balanced f = ({x : Fin n → Fin 2 | f x = 0}.card = {x : Fin n → Fin 2 | f x = 1}.card)

theorem CSD.Empirical.QM.DeutschJozsa.Balanced.signSum_eq_zero {n : ℕ} {f : (Fin n → Fin 2) → Fin 2} (hf : Balanced f) : ∑ x : Fin n → Fin 2, (-1) ^ ↑(f x) = 0

For a balanced f, the signed sum vanishes: ∑ₓ (-1)^{f(x)} = 0.

theorem CSD.Empirical.QM.DeutschJozsa.deutsch_jozsa_balanced {n : ℕ} {f : (Fin n → Fin 2) → Fin 2} (hf : Balanced f) : QuantumInfo.prob (djCircuit f (QuantumInfo.basisState 0)) 0 = 0

Deutsch–Jozsa, balanced case: if f is balanced, the probability of measuring |0ⁿ⟩ is 0.

theorem CSD.Empirical.QM.DeutschJozsa.deutsch_jozsa_constant {n : ℕ} {f : (Fin n → Fin 2) → Fin 2} {c : Fin 2} (hf : ∀ (x : Fin n → Fin 2), f x = c) : QuantumInfo.prob (djCircuit f (QuantumInfo.basisState 0)) 0 = 1

Deutsch–Jozsa, constant case: if f is constant, the probability of measuring |0ⁿ⟩ is 1 — the algorithm reports "constant" with certainty.