Bernstein–Vazirani

Category: 3-Local (QM-validity).

The Bernstein–Vazirani algorithm: given a phase oracle for the hidden linear function f_a(x) = a·x = ⟨a,x⟩ (mod 2) with secret string a ∈ {0,1}ⁿ, recover a in a single query. The circuit is the full Hadamard sandwich H^⊗n ∘ U_f ∘ H^⊗n on |0ⁿ⟩, with U_f the phase oracle |x⟩ ↦ (-1)^{⟨a,x⟩} |x⟩ (bvOracle / applyBvUf).

The output amplitude at outcome y is (1/2ⁿ) ∑ₓ (-1)^{⟨y⊕a, x⟩} (bv_amplitude), and the character sum ∑ₓ (-1)^{⟨z,x⟩} is 2ⁿ if z = 0 and 0 otherwise (bitInner_char_sum). Hence the amplitude is the Kronecker delta δ_{y,a}:

• bv_certain: the outcome y = a is obtained with probability 1;
• bv_zero: every other outcome has probability 0.

One query recovers the hidden string a deterministically.

Honest scope. Unlike the single-register reduced Simon analysis, this is the full phase-oracle circuit H^⊗n ∘ U_f ∘ H^⊗n (no second register, no measurement reduction, no classical post-processing): bv_amplitude is the exact output amplitude vector. The only modelling choice is the standard phase-oracle encoding of the linear f_a as a diagonal sign matrix. The load-bearing new content is the 𝔽₂ character sum bitInner_char_sum, proved by the per-qubit factorisation (-1)^{∑ᵢ zᵢxᵢ} = ∏ᵢ (-1)^{zᵢxᵢ} and the ∑∏ → ∏∑ swap (Finset.prod_univ_sum), each factor collapsing to 2 (if zᵢ = 0) or 0 (if zᵢ = 1).

Reuses Simon's bitInner / bxor / Hn_apply_inner / neg_one_bitInner_bxor and Deutsch–Jozsa's inv_sqrt2_pow_mul.

noncomputable def CSD.Empirical.QM.BernsteinVazirani.bvOracle {n : ℕ} (a : Fin n → Fin 2) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The Bernstein–Vazirani phase oracle U_f : |x⟩ ↦ (-1)^{⟨a,x⟩} |x⟩ for the hidden linear function f_a(x) = a·x = bitInner a x (mod 2).

Equations

• CSD.Empirical.QM.BernsteinVazirani.bvOracle a = Matrix.diagonal fun (x : Fin n → Fin 2) => (-1) ^ CSD.Empirical.QM.Simon.bitInner a x

noncomputable def CSD.Empirical.QM.BernsteinVazirani.applyBvUf {n : ℕ} (a : Fin n → Fin 2) (ψ : QuantumInfo.QReg n) : QuantumInfo.QReg n

The phase oracle's action on a register state.

Equations

• CSD.Empirical.QM.BernsteinVazirani.applyBvUf a ψ = (Matrix.toEuclideanLin (CSD.Empirical.QM.BernsteinVazirani.bvOracle a)) ψ

theorem CSD.Empirical.QM.BernsteinVazirani.applyBvUf_apply {n : ℕ} (a : Fin n → Fin 2) (ψ : QuantumInfo.QReg n) (y : Fin n → Fin 2) : (applyBvUf a ψ).ofLp y = (-1) ^ Simon.bitInner a y * ψ.ofLp y

theorem CSD.Empirical.QM.BernsteinVazirani.bitInner_char_sum {n : ℕ} (z : Fin n → Fin 2) : ∑ x : Fin n → Fin 2, (-1) ^ Simon.bitInner z x = if z = 0 then 2 ^ n else 0

The 𝔽₂ character sum ∑ₓ (-1)^{⟨z,x⟩} is 2ⁿ if z = 0 and 0 otherwise. This is the load-bearing fact behind Bernstein–Vazirani: the per-qubit factorisation (-1)^{∑ᵢ zᵢxᵢ} = ∏ᵢ (-1)^{zᵢxᵢ} plus the ∑∏ → ∏∑ swap gives ∏ᵢ (1 + (-1)^{zᵢ}), with each factor 2 (if zᵢ = 0) or 0 (if zᵢ = 1).

theorem CSD.Empirical.QM.BernsteinVazirani.bxor_eq_zero_iff {n : ℕ} (y a : Fin n → Fin 2) : Simon.bxor y a = 0 ↔ y = a

bxor y a = 0 over 𝔽₂ exactly when y = a (bitwise: yᵢ + aᵢ = 0 ↔ yᵢ = aᵢ).

noncomputable def CSD.Empirical.QM.BernsteinVazirani.bvCircuit {n : ℕ} (a : Fin n → Fin 2) (ψ : QuantumInfo.QReg n) : QuantumInfo.QReg n

The Bernstein–Vazirani circuit H^⊗n ∘ U_f ∘ H^⊗n.

Equations

• CSD.Empirical.QM.BernsteinVazirani.bvCircuit a ψ = QuantumInfo.applyHn (CSD.Empirical.QM.BernsteinVazirani.applyBvUf a (QuantumInfo.applyHn ψ))

theorem CSD.Empirical.QM.BernsteinVazirani.bv_amplitude {n : ℕ} (a y : Fin n → Fin 2) : (bvCircuit a (QuantumInfo.basisState 0)).ofLp y = if y = a then 1 else 0

The output amplitude is the Kronecker delta δ_{y,a}. Running the full circuit on |0ⁿ⟩ yields amplitude 1 at the hidden string y = a and 0 everywhere else.

theorem CSD.Empirical.QM.BernsteinVazirani.bv_certain {n : ℕ} (a : Fin n → Fin 2) : QuantumInfo.prob (bvCircuit a (QuantumInfo.basisState 0)) a = 1

Bernstein–Vazirani: the hidden linear string a is measured with certainty after one query.

theorem CSD.Empirical.QM.BernsteinVazirani.bv_zero {n : ℕ} (a y : Fin n → Fin 2) (h : y ≠ a) : QuantumInfo.prob (bvCircuit a (QuantumInfo.basisState 0)) y = 0

Bernstein–Vazirani: every outcome other than the hidden string a has probability 0.