Boolean (XOR) oracles

Standard quantum-circuit access to a Boolean function f : Fin (2 ^ n) → Bool: the XOR (bit-flip) oracle on n + 1 qubits,

U_f |x⟩|b⟩ = |x⟩|b ⊕ f(x)⟩,

the unitary query form O_x : |i, b⟩ ↦ |i, b ⊕ xᵢ⟩ of [dW19, qcnotes.tex:1151].

Conventions

• An oracle is not a new kind of object: it is just a Gate (n + 1), built as a basis permutation (Gate.ofPerm), hence unitary for free — "in matrix representation [it] is a permutation matrix and hence unitary" [dW19, qcnotes.tex:1154].
• Register layout matches LeanPool.LeanQuantumAlg.prodEquiv (big-endian): input register = qubits 0..n-1 (most significant bits), target qubit = qubit n (least significant bit); the joint basis label is prodEquiv (x, b).
• The bit flip on the target label b : Fin (2 ^ 1) is Fin.rev (0 ↦ 1, 1 ↦ 0), so if f x then b.rev else b is exactly b ⊕ f x.

Main definitions

• LeanPool.LeanQuantumAlg.Gate.xorPerm f — the basis involution (x, b) ↦ (x, b ⊕ f x).
• LeanPool.LeanQuantumAlg.Gate.xorOracle f — the oracle gate U_f : Gate (n + 1); xorOracle_apply_ket computes its action on basis kets and xorOracle_mem_unitaryGroup gives unitarity.

Pinned Mathlib API: Equiv.permCongr (permCongr_apply), Fin.rev (Fin.rev_rev), Equiv.apply_eq_iff_eq, Equiv.apply_eq_iff_eq_symm_apply, Equiv.symm_apply_eq.

def QuantumAlg.Gate.xorPerm {n : ℕ} (f : Fin (2 ^ n) → Bool) : Equiv.Perm (Fin (2 ^ n) × Fin (2 ^ 1))

The basis involution underlying the XOR oracle: (x, b) ↦ (x, b ⊕ f x), with the bit flip written as Fin.rev.

Equations

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

@[simp]

theorem QuantumAlg.Gate.xorPerm_apply {n : ℕ} (f : Fin (2 ^ n) → Bool) (p : Fin (2 ^ n) × Fin (2 ^ 1)) : (xorPerm f) p = (p.1, if f p.1 = true then p.2.rev else p.2)

@[simp]

theorem QuantumAlg.Gate.xorPerm_symm {n : ℕ} (f : Fin (2 ^ n) → Bool) : Equiv.symm (xorPerm f) = xorPerm f

The XOR oracle is an involution.

def QuantumAlg.Gate.xorOracle {n : ℕ} (f : Fin (2 ^ n) → Bool) : Gate (n + 1)

The XOR (bit-flip) oracle of f, as a permutation gate on n + 1 qubits: U_f |x⟩|b⟩ = |x⟩|b ⊕ f(x)⟩ (input register first/most significant, target qubit last/least significant).

Equations

• QuantumAlg.Gate.xorOracle f = QuantumAlg.Gate.ofPerm (QuantumAlg.prodEquiv.permCongr (QuantumAlg.Gate.xorPerm f))

theorem QuantumAlg.Gate.xorOracle_mem_unitaryGroup {n : ℕ} (f : Fin (2 ^ n) → Bool) : (xorOracle f).op ∈ Matrix.unitaryGroup (Fin (2 ^ (n + 1))) ℂ

theorem QuantumAlg.Gate.xorOracle_apply {n : ℕ} (f : Fin (2 ^ n) → Bool) (ψ : PureState (n + 1)) (i : Fin (2 ^ (n + 1))) : ((xorOracle f).apply ψ).vec.ofLp i = ψ.vec.ofLp (prodEquiv ((xorPerm f) (prodEquiv.symm i)))

theorem QuantumAlg.Gate.xorOracle_apply_ket {n : ℕ} (f : Fin (2 ^ n) → Bool) (x : Fin (2 ^ n)) (b : Fin (2 ^ 1)) : (xorOracle f).apply (PureState.ket (prodEquiv (x, b))) = PureState.ket (prodEquiv (x, if f x = true then b.rev else b))

Action on basis kets: U_f |x⟩|b⟩ = |x⟩|b ⊕ f(x)⟩.