Walsh-Hadamard transform and the XOR phase-query pipeline

The reusable machinery shared by the single-query Hadamard-oracle-Hadamard algorithms (Deutsch-Jozsa, Bernstein-Vazirani): the n-qubit Hadamard layer in Walsh-Hadamard closed form [dW19, qcnotes.tex:1005-1006], and the XOR-oracle phase-query pipeline that runs a Boolean oracle on the uniform input register with a |−⟩ target.

The central bridge postOracleState_eq_afterPhaseQuery_tensor rewrites the actual XOR-oracle query as the phase pattern (√(2^n))⁻¹ ∑ x (-1)^{f x}|x⟩ tensored with the unchanged |−⟩ target, so a single query followed by the second Hadamard layer (finalJointState) factors through the input-register finalState.

These pieces sit in a Primitives module so the Deutsch-Jozsa and Bernstein-Vazirani algorithms can both build on them without importing one another; each algorithm keeps only its target-specific content (the constant/balanced promise and amplitude test for Deutsch-Jozsa; Walsh-character orthogonality and string recovery for Bernstein-Vazirani).

Main definitions

• LeanPool.LeanQuantumAlg.WalshHadamard.Oracle n — a Boolean function on 2^n labels, queried through Gate.xorOracle.
• LeanPool.LeanQuantumAlg.WalshHadamard.walshSign — the Walsh-Hadamard sign (-1)^{x·y}, and hadamardLayer its closed-form n-qubit gate.
• LeanPool.LeanQuantumAlg.WalshHadamard.uniformState — the uniform superposition.
• LeanPool.LeanQuantumAlg.WalshHadamard.finalJointState — the post-circuit joint state, with finalJointState_eq_finalState_tensor factoring off the |−⟩ target.

@[reducible, inline]

abbrev QuantumAlg.WalshHadamard.Oracle (n : ℕ) : Type

A Boolean oracle on 2^n input labels. It is queried through Gate.xorOracle, not through a separate oracle type.

Equations

• QuantumAlg.WalshHadamard.Oracle n = (Fin (2 ^ n) → Bool)

@[reducible, inline]

abbrev QuantumAlg.WalshHadamard.oracleGate {n : ℕ} (f : Oracle n) : Gate (n + 1)

The standard XOR query gate for a Boolean oracle.

Equations

• QuantumAlg.WalshHadamard.oracleGate f = QuantumAlg.Gate.xorOracle f

def QuantumAlg.WalshHadamard.phaseSign {n : ℕ} (f : Oracle n) (x : Fin (2 ^ n)) : ℂ

The phase (-1)^{f x}, written as a complex scalar.

Equations

• QuantumAlg.WalshHadamard.phaseSign f x = if f x = true then -1 else 1

The Walsh-Hadamard transform

def QuantumAlg.WalshHadamard.bit {n : ℕ} (x : Fin (2 ^ n)) (k : Fin n) : Bool

The bit of a basis label used in the Walsh-Hadamard character. The bit order only affects nonzero rows; the zero row used by Deutsch-Jozsa is independent of it.

Equations

• QuantumAlg.WalshHadamard.bit x k = (↑x).testBit ↑k

def QuantumAlg.WalshHadamard.dotParity {n : ℕ} (x y : Fin (2 ^ n)) : Bool

Parity of the bitwise inner product of two basis labels.

Equations

• QuantumAlg.WalshHadamard.dotParity x y = decide (Odd {k : Fin n | (QuantumAlg.WalshHadamard.bit x k && QuantumAlg.WalshHadamard.bit y k) = true}.card)

def QuantumAlg.WalshHadamard.walshSign {n : ℕ} (x y : Fin (2 ^ n)) : ℂ

The Walsh-Hadamard sign (-1)^{x · y}.

Equations

• QuantumAlg.WalshHadamard.walshSign x y = if QuantumAlg.WalshHadamard.dotParity x y = true then -1 else 1

noncomputable def QuantumAlg.WalshHadamard.invSqrtCard (n : ℕ) : ℂ

(√(2^n))⁻¹, the normalization scalar of the n-qubit Hadamard layer.

Equations

• QuantumAlg.WalshHadamard.invSqrtCard n = (↑√↑(2 ^ n))⁻¹

@[simp]

theorem QuantumAlg.WalshHadamard.star_invSqrtCard (n : ℕ) : star (invSqrtCard n) = invSqrtCard n

@[simp]

theorem QuantumAlg.WalshHadamard.norm_invSqrtCard (n : ℕ) : ‖invSqrtCard n‖ = (√↑(2 ^ n))⁻¹

theorem QuantumAlg.WalshHadamard.norm_sq_invSqrtCard (n : ℕ) : ‖invSqrtCard n‖ ^ 2 = (↑(2 ^ n))⁻¹

@[simp]

theorem QuantumAlg.WalshHadamard.walshSign_zero_left {n : ℕ} (x : Fin (2 ^ n)) : walshSign 0 x = 1

@[simp]

theorem QuantumAlg.WalshHadamard.walshSign_zero_right {n : ℕ} (x : Fin (2 ^ n)) : walshSign x 0 = 1

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuantumAlg.WalshHadamard.norm_walshSign {n : ℕ} (x y : Fin (2 ^ n)) : ‖walshSign x y‖ = 1

Walsh-character orthogonality

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

Flip bit k of a basis label.

Equations

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

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

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

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

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

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

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

Two distinct labels differ at some bit.

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

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

theorem QuantumAlg.WalshHadamard.sum_walshSign_mul_walshSign {n : ℕ} {y s : Fin (2 ^ n)} (h : y ≠ s) : ∑ x : Fin (2 ^ n), walshSign y x * 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.

theorem QuantumAlg.WalshHadamard.sum_walshSign_mul_walshSign_eq {n : ℕ} (y s : Fin (2 ^ n)) : ∑ x : Fin (2 ^ n), walshSign y x * walshSign s x = if y = s then ↑(2 ^ n) else 0

@[simp]

theorem QuantumAlg.WalshHadamard.invSqrtCard_mul_self (n : ℕ) : invSqrtCard n * invSqrtCard n = (↑(2 ^ n))⁻¹

@[simp]

theorem QuantumAlg.WalshHadamard.norm_phaseSign {n : ℕ} (f : Oracle n) (x : Fin (2 ^ n)) : ‖phaseSign f x‖ = 1

A Boolean phase has unit norm.

noncomputable def QuantumAlg.WalshHadamard.hadamardLayerOp (n : ℕ) : HilbertOperator n

Raw n-qubit Hadamard layer in Walsh-Hadamard closed form.

Equations

• QuantumAlg.WalshHadamard.hadamardLayerOp n y x = QuantumAlg.WalshHadamard.invSqrtCard n * QuantumAlg.WalshHadamard.walshSign y x

theorem QuantumAlg.WalshHadamard.hadamardLayerOp_mem_unitaryGroup (n : ℕ) : hadamardLayerOp n ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ

The Walsh-Hadamard closed-form matrix is unitary.

noncomputable def QuantumAlg.WalshHadamard.hadamardLayer (n : ℕ) : Gate n

The n-qubit Hadamard layer as a unitary gate.

Equations

• QuantumAlg.WalshHadamard.hadamardLayer n = QuantumAlg.Gate.ofUnitary (QuantumAlg.WalshHadamard.hadamardLayerOp n) ⋯

noncomputable def QuantumAlg.WalshHadamard.uniformStateVec (n : ℕ) : StateVector n

Raw uniform input-register vector produced by the first Hadamard layer.

Equations

• QuantumAlg.WalshHadamard.uniformStateVec n = WithLp.toLp 2 fun (x : Fin (2 ^ n)) => QuantumAlg.WalshHadamard.invSqrtCard n

theorem QuantumAlg.WalshHadamard.norm_uniformStateVec (n : ℕ) : ‖uniformStateVec n‖ = 1

The uniform input-register vector has unit norm.

noncomputable def QuantumAlg.WalshHadamard.uniformState (n : ℕ) : PureState n

The uniform input-register state produced by the first Hadamard layer.

Equations

• QuantumAlg.WalshHadamard.uniformState n = QuantumAlg.PureState.ofVec (QuantumAlg.WalshHadamard.uniformStateVec n) ⋯

@[simp]

theorem QuantumAlg.WalshHadamard.uniformState_apply {n : ℕ} (x : Fin (2 ^ n)) : (uniformState n).vec.ofLp x = invSqrtCard n

theorem QuantumAlg.WalshHadamard.hadamardLayer_apply_zero {n : ℕ} : (hadamardLayer n).apply (PureState.ket 0) = uniformState n

The first Hadamard layer sends |0^n⟩ to the uniform superposition.

The XOR phase-query pipeline

noncomputable def QuantumAlg.WalshHadamard.initialBasisState (n : ℕ) : PureState (n + 1)

The pre-Hadamard joint basis state |0^n⟩ ⊗ |−⟩.

Equations

• QuantumAlg.WalshHadamard.initialBasisState n = (QuantumAlg.PureState.ket 0).tensor QuantumAlg.PureState.ketMinus

noncomputable def QuantumAlg.WalshHadamard.initialState (n : ℕ) : PureState (n + 1)

The joint state queried by the XOR oracle, obtained by applying the first Hadamard layer to the input register and leaving the |−⟩ target alone.

Equations

• QuantumAlg.WalshHadamard.initialState n = ((QuantumAlg.WalshHadamard.hadamardLayer n).tensor 1).apply (QuantumAlg.WalshHadamard.initialBasisState n)

theorem QuantumAlg.WalshHadamard.initialState_eq_uniform_tensor {n : ℕ} : initialState n = (uniformState n).tensor PureState.ketMinus

The queried state is the uniform input register tensored with |−⟩.

noncomputable def QuantumAlg.WalshHadamard.postOracleState {n : ℕ} (f : Oracle n) : PureState (n + 1)

The actual post-query joint state, using the XOR oracle gate.

Equations

• QuantumAlg.WalshHadamard.postOracleState f = (QuantumAlg.WalshHadamard.oracleGate f).apply (QuantumAlg.WalshHadamard.initialState n)

noncomputable def QuantumAlg.WalshHadamard.afterPhaseQueryVec {n : ℕ} (f : Oracle n) : StateVector n

The input-register state after rewriting the oracle query by phase kickback: (√(2^n))⁻¹ ∑ x, (-1)^{f x}|x⟩.

Equations

• QuantumAlg.WalshHadamard.afterPhaseQueryVec f = WithLp.toLp 2 fun (x : Fin (2 ^ n)) => QuantumAlg.WalshHadamard.invSqrtCard n * QuantumAlg.WalshHadamard.phaseSign f x

theorem QuantumAlg.WalshHadamard.norm_afterPhaseQueryVec {n : ℕ} (f : Oracle n) : ‖afterPhaseQueryVec f‖ = 1

The phase-query vector has unit norm.

noncomputable def QuantumAlg.WalshHadamard.afterPhaseQuery {n : ℕ} (f : Oracle n) : PureState n

The input register after the XOR oracle has been converted into a phase query.

Equations

• QuantumAlg.WalshHadamard.afterPhaseQuery f = QuantumAlg.PureState.ofVec (QuantumAlg.WalshHadamard.afterPhaseQueryVec f) ⋯

theorem QuantumAlg.WalshHadamard.postOracleState_eq_afterPhaseQuery_tensor {n : ℕ} (f : Oracle n) : postOracleState f = (afterPhaseQuery f).tensor PureState.ketMinus

The actual XOR-oracle query on the uniform input register and |−⟩ target is exactly the phase-query state tensored with the unchanged target.

noncomputable def QuantumAlg.WalshHadamard.finalState {n : ℕ} (f : Oracle n) : PureState n

The final input-register state after the second Hadamard layer, in the phase-query view.

Equations

• QuantumAlg.WalshHadamard.finalState f = (QuantumAlg.WalshHadamard.hadamardLayer n).apply (QuantumAlg.WalshHadamard.afterPhaseQuery f)

noncomputable def QuantumAlg.WalshHadamard.finalJointState {n : ℕ} (f : Oracle n) : PureState (n + 1)

The actual final joint state: apply the second Hadamard layer to the input register and leave the target qubit alone.

Equations

• QuantumAlg.WalshHadamard.finalJointState f = ((QuantumAlg.WalshHadamard.hadamardLayer n).tensor 1).apply (QuantumAlg.WalshHadamard.postOracleState f)

theorem QuantumAlg.WalshHadamard.finalJointState_eq_finalState_tensor {n : ℕ} (f : Oracle n) : finalJointState f = (finalState f).tensor PureState.ketMinus

The actual final joint state factors as the final input-register state and the unchanged |−⟩ target.