Bernstein-Vazirani algorithm

The Bernstein-Vazirani problem gives oracle access to the inner-product function x ↦ x · s mod 2 of an unknown string s, and asks to find s [dW19, qcnotes.tex:1282-1283]. The original problem is due to Bernstein and Vazirani (1997).

The circuit is exactly the Deutsch-Jozsa circuit [dW19, qcnotes.tex:1288]: after one query, the input register holds the phase pattern (1/√N) ∑_x (-1)^{x·s} |x⟩ [dW19, qcnotes.tex:1293-1294], and the second Hadamard layer maps it exactly to the classical state |s⟩ [dW19, qcnotes.tex:1296]. One query therefore recovers the whole hidden string.

This module reuses the shared Walsh-Hadamard pipeline (WalshHadamard.finalJointState applied to the inner-product oracle): the query is the actual XOR-oracle gate, bridged by phase kickback. The new mathematical content is Walsh-character orthogonality, proved by a pair-cancellation involution (flip a bit on which the two characters disagree).

Conventions

• Bit order: WalshHadamard.bit x k = x.val.testBit k.val, as in the WalshHadamard primitive. The recovered string is expressed in the same convention used by the oracle, so the statement is convention-consistent.
• Big-endian basis labelling as in Core/State.lean.

Main results

• LeanPool.LeanQuantumAlg.BernsteinVazirani.oracle — the inner-product oracle of a hidden string, as a WalshHadamard Boolean oracle.
• LeanPool.LeanQuantumAlg.BernsteinVazirani.sum_walshSign_mul_walshSign — Walsh-character orthogonality via the bit-flip involution.
• LeanPool.LeanQuantumAlg.BernsteinVazirani.finalState_oracle — the final input register is exactly |s⟩.
• LeanPool.LeanQuantumAlg.BernsteinVazirani.main — the joint register after the circuit is exactly |s⟩ ⊗ |−⟩: one query recovers the hidden string.

def QuantumAlg.BernsteinVazirani.oracle {n : ℕ} (s : Fin (2 ^ n)) : WalshHadamard.Oracle n

The Bernstein-Vazirani oracle for hidden string s: the inner-product function x ↦ x · s mod 2 [dW19, qcnotes.tex:1283], queried through Gate.xorOracle like any Deutsch-Jozsa oracle.

Equations

• QuantumAlg.BernsteinVazirani.oracle s x = QuantumAlg.WalshHadamard.dotParity x s

Walsh-sign algebra

theorem QuantumAlg.BernsteinVazirani.dotParity_comm {n : ℕ} (x y : Fin (2 ^ n)) : WalshHadamard.dotParity x y = WalshHadamard.dotParity y x

The bitwise inner-product parity is symmetric.

theorem QuantumAlg.BernsteinVazirani.walshSign_comm {n : ℕ} (x y : Fin (2 ^ n)) : WalshHadamard.walshSign x y = WalshHadamard.walshSign y x

The Walsh sign is symmetric.

theorem QuantumAlg.BernsteinVazirani.walshSign_mul_self {n : ℕ} (x y : Fin (2 ^ n)) : WalshHadamard.walshSign x y * WalshHadamard.walshSign x y = 1

A Walsh sign squares to 1.

Bit-flip involution

def QuantumAlg.BernsteinVazirani.flipBit {n : ℕ} (x : Fin (2 ^ n)) (k : Fin n) : Fin (2 ^ n)

Flip bit k of a basis label.

Equations

• QuantumAlg.BernsteinVazirani.flipBit x k = ⟨↑x ^^^ 2 ^ ↑k, ⋯⟩

theorem QuantumAlg.BernsteinVazirani.bit_flipBit {n : ℕ} (x : Fin (2 ^ n)) (k k' : Fin n) : WalshHadamard.bit (flipBit x k) k' = (WalshHadamard.bit x k' ^^ decide (k = k'))

theorem QuantumAlg.BernsteinVazirani.flipBit_flipBit {n : ℕ} (x : Fin (2 ^ n)) (k : Fin n) : flipBit (flipBit x k) k = x

theorem QuantumAlg.BernsteinVazirani.flipBit_ne {n : ℕ} (x : Fin (2 ^ n)) (k : Fin n) : flipBit x k ≠ x

theorem QuantumAlg.BernsteinVazirani.dotParity_flipBit {n : ℕ} (x z : Fin (2 ^ n)) (k : Fin n) : WalshHadamard.dotParity (flipBit x k) z = (WalshHadamard.dotParity x z ^^ WalshHadamard.bit z k)

Flipping bit k of x toggles the parity x · z exactly when bit k of z is set.

theorem QuantumAlg.BernsteinVazirani.exists_bit_ne {n : ℕ} {y s : Fin (2 ^ n)} (h : y ≠ s) : ∃ (k : Fin n), WalshHadamard.bit y k ≠ WalshHadamard.bit s k

Two distinct labels differ at some bit.

theorem QuantumAlg.BernsteinVazirani.walshSign_mul_walshSign_flipBit {n : ℕ} {y s : Fin (2 ^ n)} {k : Fin n} (hk : WalshHadamard.bit y k ≠ WalshHadamard.bit s k) (x : Fin (2 ^ n)) : WalshHadamard.walshSign y (flipBit x k) * WalshHadamard.walshSign s (flipBit x k) = -(WalshHadamard.walshSign y x * WalshHadamard.walshSign s x)

Flipping a bit on which y and s disagree negates the product of their Walsh signs.

theorem QuantumAlg.BernsteinVazirani.sum_walshSign_mul_walshSign {n : ℕ} {y s : Fin (2 ^ n)} (h : y ≠ s) : ∑ x : Fin (2 ^ n), WalshHadamard.walshSign y x * WalshHadamard.walshSign s x = 0

Walsh-character orthogonality: for y ≠ s the signed sum over all basis labels cancels in pairs under the bit-flip involution.

Circuit correctness

theorem QuantumAlg.BernsteinVazirani.phaseSign_oracle {n : ℕ} (s x : Fin (2 ^ n)) : WalshHadamard.phaseSign (oracle s) x = WalshHadamard.walshSign s x

Querying the inner-product oracle phases each basis label by its Walsh sign with the hidden string [dW19, qcnotes.tex:1293].

theorem QuantumAlg.BernsteinVazirani.finalState_oracle {n : ℕ} (s : Fin (2 ^ n)) : WalshHadamard.finalState (oracle s) = PureState.ket s

The second Hadamard layer maps the Bernstein-Vazirani phase pattern exactly to the classical state |s⟩ [dW19, qcnotes.tex:1296].

noncomputable def QuantumAlg.BernsteinVazirani.timedFinalJointState {n : ℕ} (s : Fin (2 ^ n)) : Timed (PureState (n + 1))

The final Bernstein-Vazirani joint state, annotated with one oracle query.

Equations

• QuantumAlg.BernsteinVazirani.timedFinalJointState s = QuantumAlg.Timed.trusted 1 (QuantumAlg.WalshHadamard.finalJointState (QuantumAlg.BernsteinVazirani.oracle s))

@[simp]

theorem QuantumAlg.BernsteinVazirani.timedFinalJointState_ret {n : ℕ} (s : Fin (2 ^ n)) : (timedFinalJointState s).ret = WalshHadamard.finalJointState (oracle s)

@[simp]

theorem QuantumAlg.BernsteinVazirani.timedFinalJointState_time {n : ℕ} (s : Fin (2 ^ n)) : (timedFinalJointState s).time = 1

def QuantumAlg.BernsteinVazirani.resourceProfile (n : ℕ) : ResourceProfile

Public resource profile for the Bernstein-Vazirani circuit: one oracle query and two n-qubit Hadamard layers plus the target Hadamard.

Equations

• QuantumAlg.BernsteinVazirani.resourceProfile n = { oracleQueries := 1, hadamardGates := 2 * n + 1, elementaryGates := 2 * n + 1, classicalOps := 0 }

@[simp]

theorem QuantumAlg.BernsteinVazirani.resourceProfile_oracleQueries (n : ℕ) : (resourceProfile n).oracleQueries = 1

@[simp]

theorem QuantumAlg.BernsteinVazirani.resourceProfile_hadamardGates (n : ℕ) : (resourceProfile n).hadamardGates = 2 * n + 1

@[simp]

theorem QuantumAlg.BernsteinVazirani.resourceProfile_elementaryGates (n : ℕ) : (resourceProfile n).elementaryGates = 2 * n + 1

theorem QuantumAlg.BernsteinVazirani.resourceProfile_exact (n : ℕ) : (resourceProfile n).HasExactCounts 1 (2 * n + 1) (2 * n + 1) 0

noncomputable def QuantumAlg.BernsteinVazirani.profiledFinalJointState {n : ℕ} (s : Fin (2 ^ n)) : Profiled (PureState (n + 1))

The final Bernstein-Vazirani joint state with its public resource profile.

Equations

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

@[simp]

theorem QuantumAlg.BernsteinVazirani.profiledFinalJointState_ret {n : ℕ} (s : Fin (2 ^ n)) : (profiledFinalJointState s).ret = WalshHadamard.finalJointState (oracle s)

@[simp]

theorem QuantumAlg.BernsteinVazirani.profiledFinalJointState_resources {n : ℕ} (s : Fin (2 ^ n)) : (profiledFinalJointState s).resources = resourceProfile n

theorem QuantumAlg.BernsteinVazirani.main {n : ℕ} (s : Fin (2 ^ n)) : WalshHadamard.finalJointState (oracle s) = (PureState.ket s).tensor PureState.ketMinus

Bernstein-Vazirani correctness: running the Deutsch-Jozsa circuit with the inner-product oracle of hidden string s leaves the joint register in exactly |s⟩ ⊗ |−⟩ [dW19, qcnotes.tex:1296], so a single query recovers the hidden string (Bernstein and Vazirani 1997).

theorem QuantumAlg.BernsteinVazirani.timedFinalJointState_correct {n : ℕ} (s : Fin (2 ^ n)) : (timedFinalJointState s).ret = (PureState.ket s).tensor PureState.ketMinus

Bernstein-Vazirani correctness, phrased through the TimeM return value.

theorem QuantumAlg.BernsteinVazirani.main_with_resources {n : ℕ} (s : Fin (2 ^ n)) : (profiledFinalJointState s).ret = (PureState.ket s).tensor PureState.ketMinus ∧ (profiledFinalJointState s).resources.HasExactCounts 1 (2 * n + 1) (2 * n + 1) 0

Bernstein-Vazirani supporting theorem for the public statement: the profiled circuit returns |s⟩ ⊗ |-⟩ and records the accepted exact resource counts.