Deutsch-Jozsa algorithm

The Deutsch-Jozsa problem gives oracle access to a Boolean function on N = 2^n inputs, promised either constant or balanced: all values equal, or exactly half zero and half one [dW19, qcnotes.tex:1179, 1181-1182].

The algorithm uses one phase query between two layers of Hadamards [dW19, qcnotes.tex:1193]. The Walsh-Hadamard layer and the XOR phase-query pipeline are the shared LeanPool.LeanQuantumAlg.WalshHadamard primitive; this module adds only the Deutsch-Jozsa-specific content. After the query, the second Hadamard layer makes the amplitude of |0^n⟩ equal to (2^n)⁻¹ * ∑ x, (-1)^{f x} [dW19, qcnotes.tex:1245, 1251]. This scalar is 1 or -1 for constant inputs and 0 for balanced inputs [dW19, qcnotes.tex:1253, 1255], so testing whether the |0^n⟩ amplitude is nonzero decides the promise problem exactly.

Main results

• LeanPool.LeanQuantumAlg.deutschJozsa_query_phase — one XOR query with a |−⟩ target is the phase query used by the algorithm (via WalshHadamard + phase kickback).
• LeanPool.LeanQuantumAlg.DeutschJozsa.circuitZeroAmplitude_eq_zeroAmplitude_mul — the actual final joint amplitude (from WalshHadamard.finalJointState) is a nonzero scalar multiple of the standard signed phase average.
• LeanPool.LeanQuantumAlg.DeutschJozsa.main — under the explicit constant/balanced promise, the nonzero final amplitude test is equivalent to the oracle being constant.

The constant/balanced promise

def QuantumAlg.DeutschJozsa.IsConstant {n : ℕ} (f : WalshHadamard.Oracle n) : Prop

The constant side of the Deutsch-Jozsa promise.

Equations

• QuantumAlg.DeutschJozsa.IsConstant f = ∃ (c : Bool), ∀ (x : Fin (2 ^ n)), f x = c

def QuantumAlg.DeutschJozsa.trueInputs {n : ℕ} (f : WalshHadamard.Oracle n) : Finset (Fin (2 ^ n))

Inputs on which the oracle returns true.

Equations

• QuantumAlg.DeutschJozsa.trueInputs f = {x : Fin (2 ^ n) | f x = true}

def QuantumAlg.DeutschJozsa.falseInputs {n : ℕ} (f : WalshHadamard.Oracle n) : Finset (Fin (2 ^ n))

Inputs on which the oracle returns false.

Equations

• QuantumAlg.DeutschJozsa.falseInputs f = {x : Fin (2 ^ n) | (!f x) = true}

def QuantumAlg.DeutschJozsa.IsBalanced {n : ℕ} (f : WalshHadamard.Oracle n) : Prop

The balanced side of the Deutsch-Jozsa promise: exactly as many true inputs as false inputs.

Equations

• QuantumAlg.DeutschJozsa.IsBalanced f = ((QuantumAlg.DeutschJozsa.trueInputs f).card = (QuantumAlg.DeutschJozsa.falseInputs f).card)

def QuantumAlg.DeutschJozsa.Promise {n : ℕ} (f : WalshHadamard.Oracle n) : Prop

The explicit Deutsch-Jozsa promise.

Equations

• QuantumAlg.DeutschJozsa.Promise f = (QuantumAlg.DeutschJozsa.IsConstant f ∨ QuantumAlg.DeutschJozsa.IsBalanced f)

The |0^n⟩ amplitude test

noncomputable def QuantumAlg.DeutschJozsa.inputZeroAmplitude {n : ℕ} (f : WalshHadamard.Oracle n) : ℂ

The final input-register amplitude of the all-zero basis state |0^n⟩, in the phase-query view.

Equations

• QuantumAlg.DeutschJozsa.inputZeroAmplitude f = (QuantumAlg.WalshHadamard.finalState f).vec.ofLp 0

noncomputable def QuantumAlg.DeutschJozsa.circuitZeroAmplitude {n : ℕ} (f : WalshHadamard.Oracle n) : ℂ

The actual final joint amplitude of |0^n⟩ ⊗ |0⟩. It is a nonzero scalar multiple of the input-register |0^n⟩ amplitude because the target qubit remains |−⟩.

Equations

• QuantumAlg.DeutschJozsa.circuitZeroAmplitude f = (QuantumAlg.WalshHadamard.finalJointState f).vec.ofLp (QuantumAlg.prodEquiv (0, 0))

def QuantumAlg.DeutschJozsa.zeroAmplitudeNumerator {n : ℕ} (f : WalshHadamard.Oracle n) : ℂ

The numerator of the final |0^n⟩ amplitude after the second Hadamard layer: ∑ x, (-1)^{f x}.

Equations

• QuantumAlg.DeutschJozsa.zeroAmplitudeNumerator f = ∑ x : Fin (2 ^ n), QuantumAlg.WalshHadamard.phaseSign f x

noncomputable def QuantumAlg.DeutschJozsa.zeroAmplitude {n : ℕ} (f : WalshHadamard.Oracle n) : ℂ

The standard signed-average formula for the final |0^n⟩ amplitude.

Equations

• QuantumAlg.DeutschJozsa.zeroAmplitude f = (↑(2 ^ n))⁻¹ * QuantumAlg.DeutschJozsa.zeroAmplitudeNumerator f

def QuantumAlg.DeutschJozsa.ReportsConstant {n : ℕ} (f : WalshHadamard.Oracle n) : Prop

The algorithm reports "constant" exactly when the actual final joint amplitude |0^n⟩ ⊗ |0⟩ is nonzero. Under the Deutsch-Jozsa promise, this test is exact.

Equations

• QuantumAlg.DeutschJozsa.ReportsConstant f = (QuantumAlg.DeutschJozsa.circuitZeroAmplitude f ≠ 0)

theorem QuantumAlg.DeutschJozsa.zeroAmplitudeNumerator_eq_card_sub {n : ℕ} (f : WalshHadamard.Oracle n) : zeroAmplitudeNumerator f = ↑(falseInputs f).card - ↑(trueInputs f).card

The signed phase sum is the number of false inputs minus the number of true inputs.

theorem QuantumAlg.DeutschJozsa.inputZeroAmplitude_eq_zeroAmplitude {n : ℕ} (f : WalshHadamard.Oracle n) : inputZeroAmplitude f = zeroAmplitude f

Applying the closed-form second Hadamard layer to the post-query input state makes the final |0^n⟩ amplitude equal to the standard signed average.

theorem QuantumAlg.DeutschJozsa.circuitZeroAmplitude_eq_zeroAmplitude_mul {n : ℕ} (f : WalshHadamard.Oracle n) : circuitZeroAmplitude f = zeroAmplitude f * PureState.invSqrt2

The actual final joint amplitude tested by the algorithm is the input |0^n⟩ amplitude times the nonzero |0⟩ component of |−⟩.

theorem QuantumAlg.DeutschJozsa.zeroAmplitude_of_balanced {n : ℕ} (f : WalshHadamard.Oracle n) (hf : IsBalanced f) : zeroAmplitude f = 0

Balanced oracles have zero final |0^n⟩ amplitude.

theorem QuantumAlg.DeutschJozsa.zeroAmplitude_of_constant {n : ℕ} (f : WalshHadamard.Oracle n) (hf : IsConstant f) : ∃ (c : Bool), zeroAmplitude f = if c = true then -1 else 1

Constant oracles have final |0^n⟩ amplitude exactly 1 or -1, depending on the constant value.

theorem QuantumAlg.DeutschJozsa.reportsConstant_of_constant {n : ℕ} (f : WalshHadamard.Oracle n) (hf : IsConstant f) : ReportsConstant f

Constant oracles are reported as constant by the amplitude test.

theorem QuantumAlg.DeutschJozsa.not_reportsConstant_of_balanced {n : ℕ} (f : WalshHadamard.Oracle n) (hf : IsBalanced f) : ¬ReportsConstant f

Balanced oracles are not reported as constant by the amplitude test.

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

The final Deutsch-Jozsa joint state, annotated with one oracle query.

Equations

• QuantumAlg.DeutschJozsa.timedFinalJointState f = QuantumAlg.Timed.trusted 1 (QuantumAlg.WalshHadamard.finalJointState f)

@[simp]

theorem QuantumAlg.DeutschJozsa.timedFinalJointState_ret {n : ℕ} (f : WalshHadamard.Oracle n) : (timedFinalJointState f).ret = WalshHadamard.finalJointState f

@[simp]

theorem QuantumAlg.DeutschJozsa.timedFinalJointState_time {n : ℕ} (f : WalshHadamard.Oracle n) : (timedFinalJointState f).time = 1

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

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

Equations

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

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

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

The final Deutsch-Jozsa joint state with its public resource profile.

Equations

• QuantumAlg.DeutschJozsa.profiledFinalJointState f = QuantumAlg.Profiled.trusted (QuantumAlg.DeutschJozsa.resourceProfile n) (QuantumAlg.WalshHadamard.finalJointState f)

@[simp]

theorem QuantumAlg.DeutschJozsa.profiledFinalJointState_ret {n : ℕ} (f : WalshHadamard.Oracle n) : (profiledFinalJointState f).ret = WalshHadamard.finalJointState f

@[simp]

theorem QuantumAlg.DeutschJozsa.profiledFinalJointState_resources {n : ℕ} (f : WalshHadamard.Oracle n) : (profiledFinalJointState f).resources = resourceProfile n

theorem QuantumAlg.DeutschJozsa.reportsConstant_iff_timedFinalJointState {n : ℕ} (f : WalshHadamard.Oracle n) : ReportsConstant f ↔ (timedFinalJointState f).ret.vec.ofLp (prodEquiv (0, 0)) ≠ 0

The TimeM return value is the same final state used by the amplitude test.

theorem QuantumAlg.DeutschJozsa.deutschJozsa_query_phase {n : ℕ} (f : WalshHadamard.Oracle n) (x : Fin (2 ^ n)) : ((WalshHadamard.oracleGate f).apply ((PureState.ket x).tensor PureState.ketMinus)).vec = WalshHadamard.phaseSign f x • ((PureState.ket x).tensor PureState.ketMinus).vec

One Deutsch-Jozsa oracle query with the target qubit in |-⟩ is the phase query |x⟩ ↦ (-1)^{f x}|x⟩.

theorem QuantumAlg.DeutschJozsa.main {n : ℕ} (f : WalshHadamard.Oracle n) (hf : Promise f) : ReportsConstant f ↔ IsConstant f

Deutsch-Jozsa correctness: under the explicit promise that the oracle is constant or balanced, the one-query amplitude test reports "constant" iff the oracle is constant.

theorem QuantumAlg.DeutschJozsa.timedFinalJointState_correct {n : ℕ} (f : WalshHadamard.Oracle n) (hf : Promise f) : (timedFinalJointState f).ret.vec.ofLp (prodEquiv (0, 0)) ≠ 0 ↔ IsConstant f

Deutsch-Jozsa correctness, phrased through the TimeM return value.

theorem QuantumAlg.DeutschJozsa.main_with_resources {n : ℕ} (f : WalshHadamard.Oracle n) (hf : Promise f) : ((profiledFinalJointState f).ret.vec.ofLp (prodEquiv (0, 0)) ≠ 0 ↔ IsConstant f) ∧ (profiledFinalJointState f).resources.HasExactCounts 1 (2 * n + 1) (2 * n + 1) 0

Deutsch-Jozsa supporting theorem for the public statement: under the constant/balanced promise, the profiled circuit decides the constant side exactly and records the accepted exact resource counts.