diff --git a/Complexity.lean b/Complexity.lean index e6f116c6e..7accc0251 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -937,6 +937,8 @@ public import Complexity.Computability.Circuit.Pi public import Complexity.Computability.Circuit.Pointwise public import Complexity.Computability.Circuit.Program public import Complexity.Computability.Circuit.Quantum.Basic +public import Complexity.Computability.Circuit.Quantum.Code +public import Complexity.Computability.Circuit.Quantum.Uniform public import Complexity.Computability.Circuit.Rational public import Complexity.Computability.Circuit.Rational.Affine public import Complexity.Computability.Circuit.Rational.BlockDivision @@ -1042,6 +1044,7 @@ public import Complexity.Computability.Complexity.Classes.BPP.KarpLipton public import Complexity.Computability.Complexity.Classes.BPP.Reduction public import Complexity.Computability.Complexity.Classes.BPP.WorstCaseHardness public import Complexity.Computability.Complexity.Classes.BPPpath +public import Complexity.Computability.Complexity.Classes.BQP public import Complexity.Computability.Complexity.Classes.BooleanHierarchy public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Closure public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Kadin diff --git a/Complexity/Computability/Circuit/Quantum/Code.lean b/Complexity/Computability/Circuit/Quantum/Code.lean new file mode 100644 index 000000000..0ee18bbd6 --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/Code.lean @@ -0,0 +1,323 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Quantum.Basic + +/-! +# Quantum circuits over Hadamard and Toffoli gates, written as data + +This file fixes the gate set of the class `BQP` (`Cslib.Complexity.BQP`): the Hadamard gate and the +classical reversible gates NOT, CNOT and Toffoli of +`Complexity/Computability/Circuit/Quantum/Basic.lean`. Their matrix entries lie in +`{0, ±1, ±1/√2}`. + +A gate is written as a triple `(h, t, cs) : Bool × ℕ × List ℕ` (`Cslib.Quantum.GateCode`): +`(true, t, [])` is the Hadamard gate on qubit `t`, and `(false, t, cs)` with at most two control +qubits `cs` flips qubit `t` when every qubit of `cs` is one, that is NOT, CNOT or Toffoli. A code +is *well formed* on `m` qubits when its qubits are distinct and below `m` +(`Cslib.Quantum.GateCode.WellFormed`); it then denotes a placed gate +(`Cslib.Quantum.GateCode.toPlacedGate?`), and a list of codes denotes a circuit +(`Cslib.Quantum.Circuit.ofCodes`). Codes are what a polynomial-time machine outputs in the +definition of uniform circuit families. + +A run starts in the basis state `|x 0^{m - n}⟩` holding the input word `x` of length `n` on the +first qubits (`Cslib.Quantum.inputState`), and accepts when the final measurement finds qubit `0` +in state `1` (`Cslib.Quantum.accepting`, `Cslib.Quantum.acceptProb`), as in +[Arora, Barak][AroraBarak09], Chapter 10. + +Classical reversible gates permute basis states, updating the bit of their target +(`Cslib.Quantum.GateCode.eval_toPlacedGate_ket`). Appending a NOT gate on qubit `0` exchanges +acceptance and rejection (`Cslib.Quantum.acceptProb_append_not`). + +## Main definitions + +* `Cslib.Quantum.GateCode`, `Cslib.Quantum.GateCode.WellFormed`, + `Cslib.Quantum.GateCode.toPlacedGate?`: gate codes and the gates they denote. +* `Cslib.Quantum.Circuit.ofCodes`: the circuit denoted by a list of gate codes. +* `Cslib.Quantum.inputState`, `Cslib.Quantum.accepting`, `Cslib.Quantum.acceptProb`: the input + basis state, the accepting outcomes and the acceptance probability. + +## Main results + +* `Cslib.Quantum.splitEquiv_symm_update`: placing a classical gate that changes one bit. +* `Cslib.Quantum.GateCode.eval_toPlacedGate_ket`: a classical gate code updates its target bit. +* `Cslib.Quantum.acceptProb_nonneg`, `Cslib.Quantum.acceptProb_le_one`. +* `Cslib.Quantum.acceptProb_append_not`: a final NOT on qubit `0` complements the acceptance + probability. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Finset + +variable {m k : ℕ} + +/-- Placing a bit string that differs from `x ∘ A` only at position `i` changes `x` only at the +qubit `A i`. -/ +theorem splitEquiv_symm_update (A : Fin k ↪ Fin m) (x : Fin m → Bool) (i : Fin k) (b : Bool) : + (splitEquiv A).symm (Function.update (x ∘ A) i b, (splitEquiv A x).2) = + Function.update x (A i) b := by + funext j + by_cases hj : ∃ i', A i' = j + · obtain ⟨i', rfl⟩ := hj + rw [splitEquiv_symm_apply_wire] + simp only [Function.update_apply, A.injective.eq_iff, Function.comp_apply] + · rw [splitEquiv_symm_apply_of_not _ _ _ _ hj, splitEquiv_apply_snd, + Function.update_of_ne fun h => hj ⟨i, h.symm⟩] + +/-- A classical reversible gate that changes only its bit `i`, to `f z` on input `z`, maps `|x⟩` to +the basis state that changes only the qubit `A i`, to `f (x ∘ A)`. -/ +theorem PlacedGate.eval_ofPerm_ket_of_update (σ : Equiv.Perm (Fin k → Bool)) (A : Fin k ↪ Fin m) + (i : Fin k) (f : (Fin k → Bool) → Bool) (hσ : ∀ z, σ z = Function.update z i (f z)) + (x : Fin m → Bool) : + (PlacedGate.mk k (Gate.ofPerm σ) A).eval (ket x) = + ket (Function.update x (A i) (f (x ∘ A))) := by + rw [eval_ofPerm_ket, hσ, splitEquiv_symm_update] + +/-! ### Gate codes -/ + +/-- A **gate code** `(h, t, cs)`: `(true, t, [])` is the Hadamard gate on qubit `t`, and +`(false, t, cs)` with at most two controls `cs` flips qubit `t` when every qubit in `cs` is one +(the NOT, CNOT and Toffoli gates). -/ +abbrev GateCode := Bool × ℕ × List ℕ + +namespace GateCode + +/-- The placed gate denoted by a gate code on `m` qubits, or `none` when the code is not well +formed: its qubits must be distinct and below `m`. -/ +noncomputable def toPlacedGate? (m : ℕ) : GateCode → Option (PlacedGate m) + | (true, t, []) => + if h : t < m then some ⟨1, Gate.hadamard, ⟨![⟨t, h⟩], fun i j _ => Subsingleton.elim i j⟩⟩ + else none + | (false, t, []) => + if h : t < m then some ⟨1, Gate.not, ⟨![⟨t, h⟩], fun i j _ => Subsingleton.elim i j⟩⟩ + else none + | (false, t, [c]) => + if h : c < m ∧ t < m ∧ c ≠ t then + some ⟨2, Gate.cnot, ⟨![⟨c, h.1⟩, ⟨t, h.2.1⟩], by + intro i j hij + fin_cases i <;> fin_cases j <;> first | rfl | (simp [Fin.ext_iff] at hij; omega)⟩⟩ + else none + | (false, t, [c₁, c₂]) => + if h : c₁ < m ∧ c₂ < m ∧ t < m ∧ c₁ ≠ c₂ ∧ c₁ ≠ t ∧ c₂ ≠ t then + some ⟨3, Gate.toffoli, ⟨![⟨c₁, h.1⟩, ⟨c₂, h.2.1⟩, ⟨t, h.2.2.1⟩], by + intro i j hij + fin_cases i <;> fin_cases j <;> first | rfl | (simp [Fin.ext_iff] at hij; omega)⟩⟩ + else none + | _ => none + +/-- A gate code is **well formed** on `m` qubits: a Hadamard gate without controls, or a classical +gate with at most two controls, on distinct qubits below `m`. -/ +def WellFormed (m : ℕ) : GateCode → Prop + | (true, t, cs) => t < m ∧ cs = [] + | (false, t, cs) => cs.length ≤ 2 ∧ (t :: cs).Nodup ∧ ∀ i ∈ t :: cs, i < m + +instance (m : ℕ) : DecidablePred (WellFormed m) + | (true, _, _) => inferInstanceAs (Decidable (_ ∧ _)) + | (false, _, _) => inferInstanceAs (Decidable (_ ∧ _)) + +/-- **Exactly the well-formed codes denote gates.** -/ +theorem isSome_toPlacedGate?_iff {g : GateCode} : + (toPlacedGate? m g).isSome ↔ WellFormed m g := by + match g with + | (true, t, []) => simp [WellFormed, toPlacedGate?] + | (true, t, _ :: _) => simp [WellFormed, toPlacedGate?] + | (false, t, []) => simp [WellFormed, toPlacedGate?] + | (false, t, [c]) => + simp only [WellFormed, toPlacedGate?] + split_ifs with h <;> simp only [Option.isSome_some, Option.isSome_none] <;> + simp only [List.length_singleton, List.nodup_cons, List.not_mem_nil, not_false_eq_true, + List.nodup_nil, and_true, List.mem_cons, forall_eq_or_imp, true_iff, false_iff, + Bool.false_eq_true] <;> grind + | (false, t, [c₁, c₂]) => + simp only [WellFormed, toPlacedGate?] + split_ifs with h <;> simp only [Option.isSome_some, Option.isSome_none] <;> + simp only [List.length_cons, List.length_nil, List.nodup_cons, List.mem_cons, + List.not_mem_nil, List.nodup_nil, forall_eq_or_imp, true_iff, false_iff, + Bool.false_eq_true] <;> grind + | (false, t, _ :: _ :: _ :: _) => simp [WellFormed, toPlacedGate?] + +/-- **A classical gate code updates its target bit**: the well-formed code `(false, t, cs)` maps +`|x⟩` to the basis state that changes only qubit `t`, flipping it when every control is one. -/ +theorem eval_toPlacedGate_ket {t : ℕ} {cs : List ℕ} {g : PlacedGate m} + (hg : toPlacedGate? m (false, t, cs) = some g) (ht : t < m) (x : Fin m → Bool) : + g.eval (ket x) = ket (Function.update x ⟨t, ht⟩ + (x ⟨t, ht⟩ ^^ cs.all fun c => (List.ofFn x).getD c false)) := by + have hread (i : Fin m) : (List.ofFn x).getD i false = x i := by + simp [List.getD_eq_getElem?_getD] + match cs, hg with + | [], hg => + simp only [toPlacedGate?, ht, ↓reduceDIte, Option.some.injEq] at hg + subst hg + refine (PlacedGate.eval_ofPerm_ket_of_update _ _ 0 (fun z => !z 0) (fun z => ?_) x).trans ?_ + · funext i + rw [Subsingleton.elim i 0, Function.update_self] + rfl + · simp only [List.all_nil, Bool.xor_true] + rfl + | [c], hg => + simp only [toPlacedGate?] at hg + split_ifs at hg with h + simp only [Option.some.injEq] at hg + subst hg + refine (PlacedGate.eval_ofPerm_ket_of_update _ _ 1 (fun z => z 1 ^^ z 0) (fun _ => rfl) + x).trans ?_ + rw [List.all_cons, List.all_nil, Bool.and_true, + show (List.ofFn x).getD c false = x ⟨c, h.1⟩ from hread ⟨c, h.1⟩] + rfl + | [c₁, c₂], hg => + simp only [toPlacedGate?] at hg + split_ifs at hg with h + simp only [Option.some.injEq] at hg + subst hg + refine (PlacedGate.eval_ofPerm_ket_of_update _ _ 2 (fun z => z 2 ^^ (z 0 && z 1)) + (fun _ => rfl) x).trans ?_ + rw [List.all_cons, List.all_cons, List.all_nil, Bool.and_true, + show (List.ofFn x).getD c₁ false = x ⟨c₁, h.1⟩ from hread ⟨c₁, h.1⟩, + show (List.ofFn x).getD c₂ false = x ⟨c₂, h.2.1⟩ from hread ⟨c₂, h.2.1⟩] + rfl + | _ :: _ :: _ :: _, hg => simp [toPlacedGate?] at hg + +/-- **The Hadamard gate code branches on its target**: the well-formed code `(true, t, [])` maps +`|x⟩` to `∑_c (-1)^{x_t c} / √2 · |x[t ↦ c]⟩`. -/ +theorem eval_toPlacedGate_hadamard_ket {t : ℕ} {g : PlacedGate m} + (hg : toPlacedGate? m (true, t, []) = some g) (ht : t < m) (x : Fin m → Bool) : + g.eval (ket x) = ∑ c : Bool, ((if x ⟨t, ht⟩ && c then -1 else 1) * + (((Real.sqrt 2)⁻¹ : ℝ) : ℂ)) • ket (Function.update x ⟨t, ht⟩ c) := by + simp only [toPlacedGate?, ht, ↓reduceDIte, Option.some.injEq] at hg + subst hg + have hupd (y : Fin m → Bool) (c : Bool) : y = Function.update x ⟨t, ht⟩ c ↔ + y ⟨t, ht⟩ = c ∧ ∀ j ≠ ⟨t, ht⟩, y j = x j := by + constructor + · rintro rfl + exact ⟨Function.update_self .., fun j hj => Function.update_of_ne hj ..⟩ + · rintro ⟨h₁, h₂⟩ + funext j + by_cases hj : j = ⟨t, ht⟩ + · rw [hj, h₁, Function.update_self] + · rw [h₂ j hj, Function.update_of_ne hj] + ext y + rw [PlacedGate.eval_ket_apply, PlacedGate.matrix_apply, Fintype.sum_bool] + simp only [WithLp.ofLp_add, WithLp.ofLp_smul, Pi.add_apply, Pi.smul_apply, ket_apply, + smul_eq_mul, mul_ite, mul_one, mul_zero, hupd] + have hcond : (∀ j, (¬∃ i, (⟨![⟨t, ht⟩], fun i j _ => Subsingleton.elim i j⟩ : Fin 1 ↪ Fin m) i = + j) → y j = x j) ↔ ∀ j ≠ ⟨t, ht⟩, y j = x j := by + refine forall_congr' fun j => ⟨fun h hj => h ?_, fun h hj => h ?_⟩ + · rintro ⟨i, rfl⟩ + exact hj (by rw [Subsingleton.elim i 0]; rfl) + · rintro rfl + exact hj ⟨0, rfl⟩ + by_cases hagree : ∀ j ≠ ⟨t, ht⟩, y j = x j + · rw [ite_eq_left_of_eq_true _ _ (eq_true (hcond.mpr hagree)), Gate.hadamard_apply] + have hw (i : Fin 1) : + (⟨![⟨t, ht⟩], fun i j _ => Subsingleton.elim i j⟩ : Fin 1 ↪ Fin m) i = ⟨t, ht⟩ := by + rw [Subsingleton.elim i 0] + rfl + simp only [iff_true_intro hagree, and_true, Function.comp_apply, hw] + cases y ⟨t, ht⟩ <;> cases x ⟨t, ht⟩ <;> simp + · rw [ite_eq_right_of_eq_false _ _ (eq_false (mt hcond.mp hagree))] + simp only [iff_false_intro hagree, and_false, ite_false, add_zero] + +end GateCode + +/-- The circuit on `m` qubits denoted by a list of gate codes, applied first to last. Codes that are +not well formed are skipped. -/ +noncomputable def Circuit.ofCodes (m : ℕ) (gs : List GateCode) : Circuit m := + gs.filterMap (GateCode.toPlacedGate? m) + +@[simp] theorem Circuit.ofCodes_nil : Circuit.ofCodes m [] = [] := rfl + +theorem Circuit.ofCodes_append (gs hs : List GateCode) : + Circuit.ofCodes m (gs ++ hs) = Circuit.ofCodes m gs ++ Circuit.ofCodes m hs := + List.filterMap_append + +/-! ### Input, acceptance and acceptance probability -/ + +/-- The basis state `|x 0^{m - n}⟩` of an `m`-qubit register holding the input word `x` on its +first qubits (truncated when `x` is longer than `m`). -/ +def inputState (m : ℕ) (x : List Bool) : Fin m → Bool := fun i => x.getD i false + +/-- The accepting outcomes: qubit `0` reads `1`. -/ +def accepting (m : ℕ) : Finset (Fin m → Bool) := + univ.filter fun y => ∃ h : 0 < m, y ⟨0, h⟩ = true + +/-- The **acceptance probability** of the circuit with gate codes `gs` on `m` qubits on input `x`: +started in `|x 0^{m - n}⟩`, the final measurement finds qubit `0` in state `1`. -/ +noncomputable def acceptProb (m : ℕ) (gs : List GateCode) (x : List Bool) : ℝ := + measureProb (Circuit.run (Circuit.ofCodes m gs) (inputState m x)) (accepting m) + +theorem acceptProb_nonneg (m : ℕ) (gs : List GateCode) (x : List Bool) : + 0 ≤ acceptProb m gs x := + measureProb_nonneg _ _ + +theorem acceptProb_le_one (m : ℕ) (gs : List GateCode) (x : List Bool) : + acceptProb m gs x ≤ 1 := by + have h := measureProb_le_measureProb_univ + (Circuit.run (Circuit.ofCodes m gs) (inputState m x)) (accepting m) + rwa [measureProb_univ, Circuit.norm_run, one_pow] at h + +theorem mem_accepting (hm : 0 < m) {y : Fin m → Bool} : + y ∈ accepting m ↔ y ⟨0, hm⟩ = true := by + simp [accepting, hm] + +/-- The probability of the rejecting outcomes is one minus the acceptance probability. -/ +private theorem measureProb_compl_accepting (ψ : Qubits m) (hψ : ‖ψ‖ = 1) : + measureProb ψ (accepting m)ᶜ = 1 - measureProb ψ (accepting m) := by + have h := measureProb_univ ψ + rw [hψ, one_pow, ← union_compl (accepting m), measureProb, + sum_union disjoint_compl_right] at h + rw [measureProb, measureProb] + linarith + +/-- **A final NOT on qubit `0` exchanges acceptance and rejection.** -/ +theorem acceptProb_append_not (hm : 0 < m) (gs : List GateCode) (x : List Bool) : + acceptProb m (gs ++ [(false, 0, [])]) x = 1 - acceptProb m gs x := by + obtain ⟨g, hg⟩ : ∃ g, GateCode.toPlacedGate? m (false, 0, []) = some g := + Option.isSome_iff_exists.mp (GateCode.isSome_toPlacedGate?_iff.mpr + (by simp [GateCode.WellFormed, hm])) + set ψ := Circuit.run (Circuit.ofCodes m gs) (inputState m x) + let flip : (Fin m → Bool) → Fin m → Bool := fun y => Function.update y ⟨0, hm⟩ (!y ⟨0, hm⟩) + have hflip : Function.Involutive flip := by + intro y + funext j + by_cases hj : j = ⟨0, hm⟩ <;> simp [flip, hj] + have hket (z : Fin m → Bool) : g.eval (ket z) = ket (flip z) := by + rw [GateCode.eval_toPlacedGate_ket hg hm z] + simp only [List.all_nil, Bool.xor_true] + rfl + -- the NOT gate reads the amplitude of the flipped outcome + have happly (y : Fin m → Bool) : (g.eval ψ).ofLp y = ψ.ofLp (flip y) := by + have hrow (z : Fin m → Bool) : + (g.matrix : Matrix _ _ ℂ) y z = if z = flip y then 1 else 0 := by + rw [← PlacedGate.eval_ket_apply, hket, ket_apply] + refine if_congr ⟨fun h => ?_, fun h => ?_⟩ rfl rfl + · rw [h, hflip] + · rw [h, hflip] + simp only [PlacedGate.eval, unitaryEquiv_apply, Matrix.mulVec, dotProduct, hrow, ite_mul, + one_mul, zero_mul, sum_ite_eq', mem_univ, ite_true] + have hrun : Circuit.run (Circuit.ofCodes m (gs ++ [(false, 0, [])])) (inputState m x) = + g.eval ψ := by + simp only [Circuit.run, Circuit.ofCodes_append, Circuit.eval_append, ψ] + simp [Circuit.ofCodes, hg] + rw [acceptProb, hrun, acceptProb, ← measureProb_compl_accepting ψ (Circuit.norm_run _ _)] + simp only [measureProb, happly] + refine sum_nbij' flip flip (fun y hy => ?_) (fun y hy => ?_) (fun y _ => hflip y) + (fun y _ => hflip y) (fun y _ => rfl) + · rw [mem_accepting hm] at hy + simp [mem_accepting hm, flip, hy] + · rw [mem_compl, mem_accepting hm] at hy + simpa [mem_accepting hm, flip] using hy + +end Cslib.Quantum diff --git a/Complexity/Computability/Circuit/Quantum/Uniform.lean b/Complexity/Computability/Circuit/Quantum/Uniform.lean new file mode 100644 index 000000000..b612a5435 --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/Uniform.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Quantum.Code +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List + +/-! +# Polynomial-time uniform families of quantum circuits + +A uniform family of quantum circuits (`Cslib.Quantum.UniformCircuitFamily`) gives, for inputs of +length `n`, an `m`-qubit register with `m = width n ≥ n` and the gate codes `gates n` of a circuit +over the Hadamard, NOT, CNOT and Toffoli gates +(`Complexity/Computability/Circuit/Quantum/Code.lean`). +Both are computed from `n`, written in unary, by a polynomial-time machine. This follows the +library's convention for uniform Boolean circuits +(`Cslib.Complexity.CircuitValue.exists_uniformCircuits`) and [Arora, Barak][AroraBarak09], +Chapter 10: a polynomial-time machine that, given `n` in unary, outputs the descriptions of the +gates. Wires and the register width are written in unary, so they are +polynomially bounded. On an input word `x` the family runs its circuit for `n = |x|` from +`|x 0^{m - n}⟩` and accepts when the final measurement finds qubit `0` in state `1` +(`Cslib.Quantum.UniformCircuitFamily.acceptProb`). + +Appending a NOT gate on qubit `0` gives a family with complementary acceptance probability +(`Cslib.Quantum.UniformCircuitFamily.appendNot`). + +## Main definitions + +* `Cslib.Quantum.encGateCode`: the encoding of gate codes. +* `Cslib.Quantum.UniformCircuitFamily`: polynomial-time uniform families of circuits. +* `Cslib.Quantum.UniformCircuitFamily.acceptProb`: the acceptance probability on an input word. +* `Cslib.Quantum.UniformCircuitFamily.appendNot`: the family with a final NOT on qubit `0`. + +## Main results + +* `Cslib.Quantum.UniformCircuitFamily.acceptProb_appendNot`: the acceptance probability of + `appendNot` is one minus that of the family. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Turing.MultiTapeTM + +/-- The encoding of gate codes `(h, t, cs)`: the Hadamard flag, then the target and the list of +controls in unary. -/ +abbrev encGateCode : GateCode ↪ List Bool := encPair encBool (encPair encUnary (encList encUnary)) + +/-- A **polynomial-time uniform family of quantum circuits** over the Hadamard, NOT, CNOT and +Toffoli gates. On inputs of length `n` it uses a register of `width n` qubits, at least `n` and at +least one, and the well-formed gate codes `gates n`. The width and the gate codes are computed from +`n` in unary in polynomial time. -/ +structure UniformCircuitFamily where + /-- The number of qubits used on inputs of length `n`. -/ + width : ℕ → ℕ + /-- The gate codes of the circuit used on inputs of length `n`, applied first to last. -/ + gates : ℕ → List GateCode + computableInPolyTime_width : ComputableInPolyTime width encUnary encUnary + computableInPolyTime_gates : ComputableInPolyTime gates encUnary (encList encGateCode) + le_width : ∀ n, n ≤ width n + width_pos : ∀ n, 0 < width n + wellFormed : ∀ n, ∀ g ∈ gates n, g.WellFormed (width n) + +namespace UniformCircuitFamily + +/-- The **acceptance probability** of the family on the input word `x`: its circuit for inputs of +length `|x|`, started in `|x 0^{m - |x|}⟩`, ends with qubit `0` measured in state `1`. -/ +noncomputable def acceptProb (F : UniformCircuitFamily) (x : List Bool) : ℝ := + Quantum.acceptProb (F.width x.length) (F.gates x.length) x + +theorem acceptProb_nonneg (F : UniformCircuitFamily) (x : List Bool) : 0 ≤ F.acceptProb x := + Quantum.acceptProb_nonneg _ _ _ + +theorem acceptProb_le_one (F : UniformCircuitFamily) (x : List Bool) : F.acceptProb x ≤ 1 := + Quantum.acceptProb_le_one _ _ _ + +/-- The family with a final NOT gate on qubit `0`. -/ +def appendNot (F : UniformCircuitFamily) : UniformCircuitFamily where + width := F.width + gates n := F.gates n ++ [(false, 0, [])] + computableInPolyTime_width := F.computableInPolyTime_width + computableInPolyTime_gates := by + have := F.computableInPolyTime_gates + fun_prop + le_width := F.le_width + width_pos := F.width_pos + wellFormed n g hg := by + rcases List.mem_append.mp hg with hg | hg + · exact F.wellFormed n g hg + · rw [List.mem_singleton.mp hg] + simp [GateCode.WellFormed, F.width_pos n] + +/-- **A final NOT on qubit `0` complements the acceptance probability.** -/ +@[simp] theorem acceptProb_appendNot (F : UniformCircuitFamily) (x : List Bool) : + F.appendNot.acceptProb x = 1 - F.acceptProb x := + acceptProb_append_not (F.width_pos _) _ _ + +end UniformCircuitFamily + +end Cslib.Quantum diff --git a/Complexity/Computability/Complexity/Classes/BQP.lean b/Complexity/Computability/Complexity/Classes/BQP.lean new file mode 100644 index 000000000..3ef377f94 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/BQP.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Quantum.Uniform + +/-! +# The class BQP + +`BQP` is the class of problems decided with bounded error by polynomial-time uniform families of +quantum circuits [Bernstein, Vazirani][BernsteinVazirani1997], in the circuit formulation of +[Arora, Barak][AroraBarak09], Chapter 10: `A ∈ BQP enc` when a family +`F : Cslib.Quantum.UniformCircuitFamily` accepts the encoding of every member of `A` with +probability at least `2 / 3`, and the encoding of every other instance with probability at most +`1 / 3`. + +## Gate set + +The circuits use the Hadamard gate and the classical reversible gates NOT, CNOT and Toffoli +(`Cslib.Quantum.GateCode`), a fixed finite gate set whose matrix entries lie in +`{0, ±1, ±1/√2}`. Arora and Barak instead allow any elementary operation, a unitary acting on at +most three qubits, whose description a polynomial-time machine outputs. The two definitions give +the same class. Toffoli and Hadamard gates are universal for quantum computation +[Shi][Shi2003], [Aharonov][Aharonov2003]; with the Solovay–Kitaev approximation theorem, circuits +over them simulate circuits over arbitrary elementary operations with polynomial overhead and small +error. This equivalence is cited, not formalized here. A fixed finite gate set matters: +Adleman, DeMarrais and Huang show that arbitrary complex amplitudes would put uncountably many +languages into `BQP` [Adleman, DeMarrais, Huang][AdlemanDeMarraisHuang1997]. + +Acceptance is the measurement of qubit `0`, after a single measurement of the whole register in the +computational basis at the end; Arora and Barak note that intermediate measurements and mixed +states add no power. + +## Main definitions + +* `Cslib.Complexity.BQP`. + +## Main results + +* `Cslib.Complexity.compl_mem_BQP`: `BQP` is closed under complement. + +## References + +* [E. Bernstein, U. Vazirani, *Quantum complexity theory*][BernsteinVazirani1997] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +* [Y. Shi, *Both Toffoli and Controlled-NOT need little help to do universal quantum + computation*][Shi2003] +* [D. Aharonov, *A simple proof that Toffoli and Hadamard are quantum universal*][Aharonov2003] +* [L. Adleman, J. DeMarrais, M.-D. Huang, *Quantum computability*][AdlemanDeMarraisHuang1997] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Quantum + +variable {α : Type} + +/-- The problems decided with bounded error by polynomial-time uniform families of quantum +circuits over the Hadamard, NOT, CNOT and Toffoli gates, with respect to the encoding `enc` of +instances: members are accepted with probability at least `2 / 3`, and other instances with +probability at most `1 / 3`. -/ +def BQP (enc : α ↪ List Bool) : Set (Set α) := + {A | ∃ F : UniformCircuitFamily, ∀ a, + (a ∈ A → 2 / 3 ≤ F.acceptProb (enc a)) ∧ (a ∉ A → F.acceptProb (enc a) ≤ 1 / 3)} + +variable {enc : α ↪ List Bool} {A : Set α} + +theorem mem_BQP : A ∈ BQP enc ↔ ∃ F : UniformCircuitFamily, ∀ a, + (a ∈ A → 2 / 3 ≤ F.acceptProb (enc a)) ∧ (a ∉ A → F.acceptProb (enc a) ≤ 1 / 3) := + Iff.rfl + +/-- **`BQP` is closed under complement**: a final NOT gate on qubit `0` exchanges acceptance and +rejection. -/ +theorem compl_mem_BQP (hA : A ∈ BQP enc) : Aᶜ ∈ BQP enc := by + obtain ⟨F, hF⟩ := hA + refine ⟨F.appendNot, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ + · have := (hF a).2 ha + rw [UniformCircuitFamily.acceptProb_appendNot] + linarith + · have := (hF a).1 (Set.notMem_compl_iff.mp ha) + rw [UniformCircuitFamily.acceptProb_appendNot] + linarith + +end Cslib.Complexity diff --git a/Complexity/Foundations/Quantum/Measurement.lean b/Complexity/Foundations/Quantum/Measurement.lean index 63b40ca6c..b13c06033 100644 --- a/Complexity/Foundations/Quantum/Measurement.lean +++ b/Complexity/Foundations/Quantum/Measurement.lean @@ -34,6 +34,7 @@ query index (`Complexity/Computability/QueryComplexity/Quantum/Search.lean`). ## Main results * `Cslib.Quantum.measureProb_univ`: the outcome probabilities sum to `‖ψ‖²`. +* `Cslib.Quantum.measureProb_ket`: a basis state is measured with certainty. * `Cslib.Quantum.measure_toOuterMeasure_apply`: the measurement probabilities are `measureProb`. ## References @@ -70,6 +71,11 @@ theorem measureProb_nonneg (ψ : EuclideanSpace ℂ ι) (S : Finset ι) : 0 ≤ theorem measureProb_univ [Fintype ι] (ψ : EuclideanSpace ℂ ι) : measureProb ψ univ = ‖ψ‖ ^ 2 := (EuclideanSpace.norm_sq_eq ψ).symm +/-- Measuring a basis state `|x⟩` gives outcome `x` with certainty. -/ +theorem measureProb_ket [DecidableEq ι] (x : ι) (S : Finset ι) : + measureProb (ket x) S = if x ∈ S then 1 else 0 := by + simp [measureProb, apply_ite] + theorem measureProb_le_measureProb_univ [Fintype ι] (ψ : EuclideanSpace ℂ ι) (S : Finset ι) : measureProb ψ S ≤ measureProb ψ univ := sum_le_sum_of_subset_of_nonneg (subset_univ S) fun _ _ _ => by positivity diff --git a/ComplexityTests/BQP.lean b/ComplexityTests/BQP.lean new file mode 100644 index 000000000..6a838bba7 --- /dev/null +++ b/ComplexityTests/BQP.lean @@ -0,0 +1,169 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.Classes.BQP + +/-! `BQP`: uniform families that decide a language exactly, interference, closure under +complement, and a family whose acceptance probability `1 / 2` decides nothing. -/ + +namespace ComplexityTests.BQP + +open Cslib Cslib.Quantum Cslib.Complexity Turing.MultiTapeTM + +/-! ### Gate codes -/ + +-- A Toffoli gate with controls `0, 1` and target `2` is well formed on three qubits, but not on +-- two, nor with a repeated qubit, nor with three controls; Hadamard gates take no controls. +example : GateCode.WellFormed 3 (false, 2, [0, 1]) := by decide +example : ¬GateCode.WellFormed 2 (false, 2, [0, 1]) := by decide +example : ¬GateCode.WellFormed 3 (false, 1, [1]) := by decide +example : ¬GateCode.WellFormed 5 (false, 0, [1, 2, 3]) := by decide +example : GateCode.WellFormed 1 (true, 0, []) := by decide +example : ¬GateCode.WellFormed 2 (true, 0, [1]) := by decide + +-- The Toffoli code maps `|110⟩` to `|111⟩`. +example : ∃ g, GateCode.toPlacedGate? 3 (false, 2, [0, 1]) = some g ∧ + g.eval (ket ![true, true, false]) = ket ![true, true, true] := by + obtain ⟨g, hg⟩ := Option.isSome_iff_exists.mp + (GateCode.isSome_toPlacedGate?_iff.mpr (by decide : GateCode.WellFormed 3 (false, 2, [0, 1]))) + refine ⟨g, hg, ?_⟩ + rw [GateCode.eval_toPlacedGate_ket hg (by decide)] + congr 1 + funext i + fin_cases i <;> rfl + +/-! ### A family that reads the first input bit -/ + +/-- The family with one qubit more than the input and no gates: it measures the first input bit. -/ +def readFirst : UniformCircuitFamily where + width n := n + 1 + gates _ := [] + computableInPolyTime_width := by fun_prop + computableInPolyTime_gates := ComputableInPolyTime.const _ + le_width n := Nat.le_succ n + width_pos n := Nat.succ_pos n + wellFormed _ _ h := by simp at h + +/-- With no gates, the input basis state is measured, so the first input bit is read exactly. -/ +theorem acceptProb_readFirst (x : List Bool) : + readFirst.acceptProb x = if x.headD false then 1 else 0 := by + change measureProb (Circuit.run (Circuit.ofCodes (x.length + 1) []) (inputState _ x)) + (accepting _) = _ + simp only [Circuit.ofCodes_nil, Circuit.run, Circuit.eval_nil, measureProb_ket, + mem_accepting (Nat.succ_pos _), inputState] + cases x <;> rfl + +/-- The words whose first bit is one. -/ +def FirstBit : Set (List Bool) := {x | x.headD false = true} + +/-- Deciding the first bit, exactly: a member and a nonmember of `BQP`. -/ +theorem firstBit_mem_BQP : FirstBit ∈ BQP encBits := by + refine ⟨readFirst, fun x => ⟨fun hx => ?_, fun hx => ?_⟩⟩ + · rw [encBits_apply, acceptProb_readFirst] + simp only [show x.headD false = true from hx, ite_true] + norm_num + · rw [encBits_apply, acceptProb_readFirst] + simp only [show x.headD false = false from Bool.eq_false_iff.mpr hx, Bool.false_eq_true, + ite_false] + norm_num + +example : FirstBitᶜ ∈ BQP encBits := compl_mem_BQP firstBit_mem_BQP + +-- The bounds are not vacuous: `readFirst` accepts `[true]` with probability one, so it does not +-- witness that the complement of `FirstBit` is in `BQP`. +example : ¬(readFirst.acceptProb (encBits [true]) ≤ 1 / 3) := by + rw [encBits_apply, acceptProb_readFirst] + norm_num + +/-! ### Interference -/ + +/-- Two Hadamard gates on qubit `0`: they cancel. -/ +def hadamardTwice : UniformCircuitFamily where + width n := n + 1 + gates _ := [(true, 0, []), (true, 0, [])] + computableInPolyTime_width := by fun_prop + computableInPolyTime_gates := ComputableInPolyTime.const _ + le_width n := Nat.le_succ n + width_pos n := Nat.succ_pos n + wellFormed n g hg := by + simp only [List.mem_cons, List.not_mem_nil, or_false, or_self] at hg + subst hg + exact ⟨Nat.succ_pos n, rfl⟩ + +-- `HH = I`: the two gates interfere, and the family reads the first bit like `readFirst`. +example (x : List Bool) : hadamardTwice.acceptProb x = readFirst.acceptProb x := by + have hrun (m : ℕ) (hm : 0 < m) (z : Fin m → Bool) : + Circuit.run (Circuit.ofCodes m [(true, 0, []), (true, 0, [])]) z = ket z := by + simp only [Circuit.ofCodes, List.filterMap_cons, List.filterMap_nil, GateCode.toPlacedGate?, + hm, ↓reduceDIte, Circuit.run, Circuit.eval_cons, Circuit.eval_nil, PlacedGate.eval, + ← unitaryEquiv_mul, PlacedGate.matrix, ← map_mul, Gate.hadamard_mul_self, map_one, + unitaryEquiv_one] + change measureProb (Circuit.run (Circuit.ofCodes (x.length + 1) [(true, 0, []), (true, 0, [])]) + (inputState _ x)) (accepting _) = + measureProb (Circuit.run (Circuit.ofCodes (x.length + 1) []) (inputState _ x)) (accepting _) + rw [hrun _ (Nat.succ_pos _)] + simp only [Circuit.ofCodes_nil, Circuit.run, Circuit.eval_nil] + +/-! ### A family that decides nothing -/ + +/-- One Hadamard gate on qubit `0`. -/ +def hadamardOnce : UniformCircuitFamily where + width n := n + 1 + gates _ := [(true, 0, [])] + computableInPolyTime_width := by fun_prop + computableInPolyTime_gates := ComputableInPolyTime.const _ + le_width n := Nat.le_succ n + width_pos n := Nat.succ_pos n + wellFormed n g hg := by + rw [List.mem_singleton.mp hg] + exact ⟨Nat.succ_pos n, rfl⟩ + +/-- A Hadamard gate on qubit `0` makes it read `1` with probability `1 / 2`, whatever the input. -/ +theorem acceptProb_hadamardOnce (x : List Bool) : hadamardOnce.acceptProb x = 1 / 2 := by + set m := x.length + 1 + have hm : 0 < m := Nat.succ_pos _ + obtain ⟨g, hg⟩ : ∃ g, GateCode.toPlacedGate? m (true, 0, []) = some g := + Option.isSome_iff_exists.mp (GateCode.isSome_toPlacedGate?_iff.mpr + (⟨hm, rfl⟩ : GateCode.WellFormed m (true, 0, []))) + set z := inputState m x + have hrun : Circuit.run (Circuit.ofCodes m [(true, 0, [])]) z = g.eval (ket z) := by + simp [Circuit.ofCodes, hg, Circuit.run] + have hnorm (c : ℂ) (hc : ‖c‖ = 1) : ‖c * (((Real.sqrt 2)⁻¹ : ℝ) : ℂ)‖ ^ 2 = 1 / 2 := by + rw [norm_mul, hc, one_mul, Complex.norm_real, Real.norm_eq_abs, abs_inv, + abs_of_nonneg (Real.sqrt_nonneg 2), inv_pow, Real.sq_sqrt (by norm_num)] + norm_num + -- only the outcome `z[0 ↦ 1]` is accepting and reachable + have hentry (y : Fin m → Bool) (hy : y ∈ accepting m) : + ‖(g.eval (ket z)).ofLp y‖ ^ 2 = if y = Function.update z ⟨0, hm⟩ true then 1 / 2 else 0 := by + rw [mem_accepting hm] at hy + have hne : y ≠ Function.update z ⟨0, hm⟩ false := fun h => by + simp [h] at hy + rw [GateCode.eval_toPlacedGate_hadamard_ket hg hm, Fintype.sum_bool] + simp only [WithLp.ofLp_add, WithLp.ofLp_smul, Pi.add_apply, Pi.smul_apply, ket_apply, + smul_eq_mul, mul_ite, mul_one, mul_zero, hne, ite_false, add_zero] + split_ifs <;> first | exact hnorm _ (by simp) | simp + have hmem : Function.update z ⟨0, hm⟩ true ∈ accepting m := by + rw [mem_accepting hm, Function.update_self] + simp only [UniformCircuitFamily.acceptProb, acceptProb, hadamardOnce] + change measureProb (Circuit.run (Circuit.ofCodes m [(true, 0, [])]) z) (accepting m) = 1 / 2 + rw [hrun, measureProb, Finset.sum_congr rfl hentry, Finset.sum_ite_eq' _ _ _] + simp only [hmem, ite_true] + +/-- Acceptance probability `1 / 2` is neither at least `2 / 3` nor at most `1 / 3`, so +`hadamardOnce` decides no set of words with bounded error. -/ +example (A : Set (List Bool)) : ¬∀ x, + (x ∈ A → 2 / 3 ≤ hadamardOnce.acceptProb (encBits x)) ∧ + (x ∉ A → hadamardOnce.acceptProb (encBits x) ≤ 1 / 3) := by + intro h + by_cases hx : ([] : List Bool) ∈ A + · have := (h []).1 hx + rw [acceptProb_hadamardOnce] at this + norm_num at this + · have := (h []).2 hx + rw [acceptProb_hadamardOnce] at this + norm_num at this + +end ComplexityTests.BQP diff --git a/references.bib b/references.bib index 248ed73df..de1189a35 100644 --- a/references.bib +++ b/references.bib @@ -39,6 +39,17 @@ @inproceedings{Adleman1978 doi = {10.1109/SFCS.1978.37} } +@article{AdlemanDeMarraisHuang1997, + author = {Adleman, Leonard M. and DeMarrais, Jonathan and Huang, Ming-Deh A.}, + title = {Quantum Computability}, + journal = {SIAM Journal on Computing}, + volume = {26}, + number = {5}, + pages = {1524--1540}, + year = {1997}, + doi = {10.1137/S0097539795293639} +} + @article{AFvMV2006, author = {Antunes, Lu{\'i}s and Fortnow, Lance and van Melkebeek, Dieter and Vinodchandran, N. V.}, @@ -49,6 +60,14 @@ @article{AFvMV2006 year = {2006} } +@misc{Aharonov2003, + author = {Aharonov, Dorit}, + title = {A Simple Proof that {T}offoli and {H}adamard are Quantum Universal}, + year = {2003}, + eprint = {quant-ph/0301040}, + archivePrefix = {arXiv} +} + @article{Ajtai1983, author = {Ajtai, Mikl{\'o}s}, title = {{$\Sigma^1_1$}-Formulae on Finite Structures}, @@ -615,6 +634,17 @@ @article{BermanHartmanis1977 doi = {10.1137/0206023} } +@article{BernsteinVazirani1997, + author = {Bernstein, Ethan and Vazirani, Umesh}, + title = {Quantum Complexity Theory}, + journal = {SIAM Journal on Computing}, + volume = {26}, + number = {5}, + pages = {1411--1473}, + year = {1997}, + doi = {10.1137/S0097539796300921} +} + @article{Bird2011, author = {Bird, Richard S.}, title = {A Simple Division-Free Algorithm for Computing Determinants},