From d2c9204ca736ebd1e173a0e46799dab5da8d292b Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:31:08 -0400 Subject: [PATCH 1/2] feat(Classes/BQP): define BQP over Hadamard and Toffoli circuits (#896 M2) Define BQP by polynomial-time uniform families of quantum circuits over the Hadamard, NOT, CNOT and Toffoli gates, accepting by measuring qubit 0, with bounded error 2/3 vs 1/3 (Samuel's 2026-10-30 decision on #896). Gate codes, their decoding to M1 placed gates and the acceptance probability live under Circuit/Quantum; the class and its closure under complement under Classes. Tests cover exact deciders, interference and a family that decides nothing. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../Computability/Circuit/Quantum/Code.lean | 323 ++++++++++++++++++ .../Circuit/Quantum/Uniform.lean | 116 +++++++ .../Computability/Complexity/Classes/BQP.lean | 91 +++++ .../Foundations/Quantum/Measurement.lean | 6 + ComplexityTests/BQP.lean | 169 +++++++++ references.bib | 30 ++ 7 files changed, 738 insertions(+) create mode 100644 Complexity/Computability/Circuit/Quantum/Code.lean create mode 100644 Complexity/Computability/Circuit/Quantum/Uniform.lean create mode 100644 Complexity/Computability/Complexity/Classes/BQP.lean create mode 100644 ComplexityTests/BQP.lean 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}, From bcf47ab9ffeb34bec04cd478f8fa726d309afb88 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:50:55 -0400 Subject: [PATCH 2/2] =?UTF-8?q?feat(Classes/BQP):=20BQP=20=E2=8A=86=20AWPP?= =?UTF-8?q?=20=E2=8A=86=20PP=20via=20path=20sums=20(#896=20M3)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Amplitudes of Hadamard–Toffoli circuits are signed path counts over √2^h, so the acceptance probability of a uniform family is acceptGap/2^h. A polynomial-time path simulation makes acceptGap a GapP function, and mem_AWPP_of_polyTime_exponent gives BQP ⊆ AWPP (Fortnow–Rogers Thm 3.1); AWPP_subset_PP gives BQP ⊆ PP (Adleman–DeMarrais–Huang). Adds List.set_ofFn beside List.getD_ofFn. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Circuit/Quantum/PathSum.lean | 309 ++++++++++++++++++ .../Complexity/Classes/BQP/Counting.lean | 182 +++++++++++ Complexity/Foundations/Data/List/Lookup.lean | 10 + ComplexityTests/BQPCounting.lean | 55 ++++ references.bib | 13 + 6 files changed, 571 insertions(+) create mode 100644 Complexity/Computability/Circuit/Quantum/PathSum.lean create mode 100644 Complexity/Computability/Complexity/Classes/BQP/Counting.lean create mode 100644 ComplexityTests/BQPCounting.lean diff --git a/Complexity.lean b/Complexity.lean index 7accc0251..06ecbcd13 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -938,6 +938,7 @@ 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.PathSum public import Complexity.Computability.Circuit.Quantum.Uniform public import Complexity.Computability.Circuit.Rational public import Complexity.Computability.Circuit.Rational.Affine @@ -1045,6 +1046,7 @@ 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.BQP.Counting 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/PathSum.lean b/Complexity/Computability/Circuit/Quantum/PathSum.lean new file mode 100644 index 000000000..f06efa471 --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/PathSum.lean @@ -0,0 +1,309 @@ +/- +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 +import Complexity.Foundations.Data.List.Lookup + +/-! +# Amplitudes of Hadamard–Toffoli circuits as path sums + +The gates of `Complexity/Computability/Circuit/Quantum/Code.lean` act on basis states either as +permutations (NOT, CNOT, Toffoli) or by branching into two basis states with amplitudes `±1/√2` +(Hadamard). Following one branch per Hadamard gate gives a *path*: a bit string of length `h`, the +number of Hadamard gates (`Cslib.Quantum.hadamardCount`). The classical simulation +`Cslib.Quantum.pathStep` follows a path on a register written as a bit string. It writes the next +path bit into the target of a Hadamard gate, flipping a sign when the old and new bits are both +one, and it applies classical gates directly. Every amplitude of the circuit is then a signed count +of paths divided by `√2^h` (`Cslib.Quantum.run_ofCodes_apply`): +`⟨y|C|x⟩ = (∑_π ±[π ends in y]) / √2^h`. This adapts the argument of Fortnow and Rogers +[Fortnow, Rogers][FortnowRogers1999], Lemma 3.2, from quantum Turing machines to circuits. + +Squaring and summing over the accepting outcomes, the acceptance probability is a signed count of +*pairs* of paths that end in the same accepting register, divided by `2^h` +(`Cslib.Quantum.acceptProb_eq_acceptGap`). Both counts are integers computed from polynomial-time +simulations, which places `BQP` in the counting classes +(`Complexity/Computability/Complexity/Classes/BQP/Counting.lean`). + +## Main definitions + +* `Cslib.Quantum.pathStep`, `Cslib.Quantum.pathRun`: the path simulation. +* `Cslib.Quantum.hadamardCount`: the number of Hadamard gates. +* `Cslib.Quantum.pathTerm`, `Cslib.Quantum.pathGap`: the signed path count of an amplitude. +* `Cslib.Quantum.acceptTerm`, `Cslib.Quantum.acceptGap`: the signed count of pairs of paths of the + acceptance probability. + +## Main results + +* `Cslib.Quantum.ofFn_inputState`: the input basis state is the input word padded with zeros. +* `Cslib.Quantum.run_ofCodes_apply`: amplitudes are path sums. +* `Cslib.Quantum.acceptProb_eq_acceptGap`: the acceptance probability is `acceptGap / 2^h`. + +## References + +* [L. Fortnow, J. Rogers, *Complexity limitations on quantum computation*][FortnowRogers1999] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Finset + +variable {m : ℕ} + +/-- The input basis state as a bit string: the input word padded with zeros. -/ +theorem ofFn_inputState {x : List Bool} (hx : x.length ≤ m) : + List.ofFn (inputState m x) = x ++ List.replicate (m - x.length) false := by + apply List.ext_getElem (by simp; omega) + intro i h₁ h₂ + simp only [List.getElem_ofFn, inputState, List.getElem_append, List.getElem_replicate] + split_ifs with h + · simp [List.getD_eq_getElem?_getD, h] + · simp [List.getD_eq_getElem?_getD, List.getElem?_eq_none (Nat.le_of_not_lt h)] + +/-! ### The path simulation -/ + +/-- One step of the path simulation. The state holds the register bits, the unread path bits and a +sign. A Hadamard gate on `t` writes the next path bit `c` into `t`, flipping the sign when the old +and new bits are both one; a classical gate flips `t` when all its controls are one. -/ +def pathStep : List Bool × List Bool × Bool → GateCode → List Bool × List Bool × Bool + | (s, π, σ), (true, t, _) => + (s.set t (π.headD false), π.tail, σ ^^ (s.getD t false && π.headD false)) + | (s, π, σ), (false, t, cs) => + (s.set t (s.getD t false ^^ cs.all fun c => s.getD c false), π, σ) + +/-- The number of Hadamard gates in a list of gate codes. -/ +def hadamardCount : List GateCode → ℕ + | [] => 0 + | (true, _, _) :: gs => hadamardCount gs + 1 + | (false, _, _) :: gs => hadamardCount gs + +@[simp] theorem hadamardCount_nil : hadamardCount [] = 0 := rfl + +@[simp] theorem hadamardCount_cons_true (t : ℕ) (cs : List ℕ) (gs : List GateCode) : + hadamardCount ((true, t, cs) :: gs) = hadamardCount gs + 1 := rfl + +@[simp] theorem hadamardCount_cons_false (t : ℕ) (cs : List ℕ) (gs : List GateCode) : + hadamardCount ((false, t, cs) :: gs) = hadamardCount gs := rfl + +/-- The Hadamard gates are the codes flagged `true`. -/ +theorem hadamardCount_eq_countP (gs : List GateCode) : + hadamardCount gs = gs.countP fun g => g.1 := by + induction gs with + | nil => rfl + | cons g gs ih => + obtain ⟨_ | _, t, cs⟩ := g <;> simp [ih] + +/-- The final register and sign of the simulation from the register `x` along the path `π`. -/ +def pathRun (gs : List GateCode) (x π : List Bool) : List Bool × Bool := + match gs.foldl pathStep (x, π, false) with + | (s, _, σ) => (s, σ) + +/-- The signed contribution of the path `π` to the amplitude `⟨y|C|x⟩`: `±1` when the simulation +from `x` along `π` ends in `y`, with the sign it accumulates, and `0` otherwise. -/ +def pathTerm (gs : List GateCode) (x y π : List Bool) : ℤ := + match pathRun gs x π with + | (s, σ) => if s = y then (if σ then -1 else 1) else 0 + +/-- The amplitude gap: the sum of `pathTerm` over all paths of one bit per Hadamard gate. -/ +def pathGap (gs : List GateCode) (x y : List Bool) : ℤ := + ∑ π : Fin (hadamardCount gs) → Bool, pathTerm gs x y (List.ofFn π) + +/-- The signed contribution of a pair of paths to the acceptance probability: the product of +their signs when both end in the same register with qubit `0` equal to one, and `0` otherwise. -/ +def acceptTerm (gs : List GateCode) (x π π' : List Bool) : ℤ := + match pathRun gs x π, pathRun gs x π' with + | (s, σ), (s', σ') => + if s = s' ∧ s.headD false = true then (if σ ^^ σ' then -1 else 1) else 0 + +/-- The acceptance gap: the sum of `acceptTerm` over all pairs of paths. -/ +def acceptGap (gs : List GateCode) (x : List Bool) : ℤ := + ∑ π : Fin (hadamardCount gs) → Bool, ∑ π' : Fin (hadamardCount gs) → Bool, + acceptTerm gs x (List.ofFn π) (List.ofFn π') + +/-- The sign `±1` of a Boolean, in `ℂ`. -/ +private abbrev sgn (σ : Bool) : ℂ := if σ then -1 else 1 + +private theorem sgn_xor (σ τ : Bool) : sgn (σ ^^ τ) = sgn σ * sgn τ := by + cases σ <;> cases τ <;> simp [sgn] + +/-- The contribution of a path, for a simulation started with sign `σ`. -/ +private def term (gs : List GateCode) (x y : List Bool) (σ : Bool) (π : List Bool) : ℤ := + if (gs.foldl pathStep (x, π, σ)).1 = y then + (if (gs.foldl pathStep (x, π, σ)).2.2 then -1 else 1) else 0 + +private theorem pathRun_eq (gs : List GateCode) (x π : List Bool) : + pathRun gs x π = ((gs.foldl pathStep (x, π, false)).1, (gs.foldl pathStep (x, π, false)).2.2) := + rfl + +private theorem pathTerm_eq_term (gs : List GateCode) (x y π : List Bool) : + pathTerm gs x y π = term gs x y false π := + rfl + +/-- **Amplitudes are path sums** (generalized over the initial sign). -/ +private theorem sgn_mul_run_ofCodes_apply (gs : List GateCode) + (hgs : ∀ g ∈ gs, g.WellFormed m) (x y : Fin m → Bool) (σ : Bool) : + sgn σ * (Circuit.run (Circuit.ofCodes m gs) x).ofLp y = + (∑ π : Fin (hadamardCount gs) → Bool, + (term gs (List.ofFn x) (List.ofFn y) σ (List.ofFn π) : ℂ)) * + (((Real.sqrt 2)⁻¹ : ℝ) : ℂ) ^ hadamardCount gs := by + induction gs generalizing x σ with + | nil => + have hterm (π : List Bool) : term [] (List.ofFn x) (List.ofFn y) σ π = + if x = y then (if σ then -1 else 1) else 0 := by + by_cases h : x = y <;> simp [term, h] + simp only [Circuit.ofCodes_nil, Circuit.run, Circuit.eval_nil, ket_apply, hterm] + rw [Finset.sum_const, Finset.card_univ, Fintype.card_fun, Fintype.card_fin, Fintype.card_bool] + simp only [hadamardCount_nil, pow_zero, one_smul, mul_one] + by_cases h : x = y + · subst h + cases σ <;> simp [sgn] + · simp [h, Ne.symm h] + | cons g gs ih => + have hgs' : ∀ g ∈ gs, g.WellFormed m := fun g' hg' => hgs g' (List.mem_cons_of_mem _ hg') + obtain ⟨pg, hpg⟩ := Option.isSome_iff_exists.mp + (GateCode.isSome_toPlacedGate?_iff.mpr (hgs g List.mem_cons_self)) + have hofCodes : Circuit.ofCodes m (g :: gs) = pg :: Circuit.ofCodes m gs := by + simp [Circuit.ofCodes, hpg] + have hrun (z : Fin m → Bool) : Circuit.run (Circuit.ofCodes m (g :: gs)) z = + Circuit.eval (Circuit.ofCodes m gs) (pg.eval (ket z)) := by + rw [hofCodes, Circuit.run, Circuit.eval_cons] + obtain ⟨h, t, cs⟩ := g + cases h + · -- a classical gate moves the basis state + have ht : t < m := (hgs _ List.mem_cons_self).2.2 t List.mem_cons_self + have hget : (List.ofFn x).getD t false = x ⟨t, ht⟩ := List.getD_ofFn_of_lt x ht false + have hset (b : Bool) : (List.ofFn x).set t b = List.ofFn (Function.update x ⟨t, ht⟩ b) := + List.set_ofFn x ⟨t, ht⟩ b + rw [hrun, GateCode.eval_toPlacedGate_ket hpg ht, ← Circuit.run, ih hgs'] + simp only [term, List.foldl_cons, pathStep, hget, hset] + rfl + · -- a Hadamard gate branches over the next path bit + have ht : t < m := (hgs _ List.mem_cons_self).1 + have hcs : cs = [] := (hgs _ List.mem_cons_self).2 + subst hcs + have hget : (List.ofFn x).getD t false = x ⟨t, ht⟩ := List.getD_ofFn_of_lt x ht false + have hset (b : Bool) : (List.ofFn x).set t b = List.ofFn (Function.update x ⟨t, ht⟩ b) := + List.set_ofFn x ⟨t, ht⟩ b + have hterm (c : Bool) (π' : Fin (hadamardCount gs) → Bool) : + term ((true, t, []) :: gs) (List.ofFn x) (List.ofFn y) σ + (List.ofFn (Fin.cons c π' : Fin (hadamardCount gs + 1) → Bool)) = + term gs (List.ofFn (Function.update x ⟨t, ht⟩ c)) (List.ofFn y) + (σ ^^ (x ⟨t, ht⟩ && c)) (List.ofFn π') := by + simp only [term, List.ofFn_succ, Fin.cons_zero, Fin.cons_succ, List.foldl_cons, pathStep, + List.headD_cons, List.tail_cons, hget, hset] + rw [hrun, GateCode.eval_toPlacedGate_hadamard_ket hpg ht, map_sum, hadamardCount_cons_true, + ← (Fin.consEquiv fun _ => Bool).sum_comp, Fintype.sum_prod_type, Finset.sum_mul, + WithLp.ofLp_sum, Finset.sum_apply, Finset.mul_sum] + refine Finset.sum_congr rfl fun c _ => ?_ + simp only [Fin.consEquiv_apply, hterm, map_smul, WithLp.ofLp_smul, Pi.smul_apply, + smul_eq_mul] + have hih := ih hgs' (Function.update x ⟨t, ht⟩ c) (σ ^^ (x ⟨t, ht⟩ && c)) + rw [Circuit.run, sgn_xor] at hih + rw [pow_succ] + simp only [sgn] at hih ⊢ + linear_combination (((Real.sqrt 2)⁻¹ : ℝ) : ℂ) * hih + +/-- **Amplitudes are path sums**: for well-formed codes, the amplitude `⟨y|C|x⟩` of the decoded +circuit is the amplitude gap `pathGap` divided by `√2^h`, where `h` counts the Hadamard gates. -/ +theorem run_ofCodes_apply (gs : List GateCode) (hgs : ∀ g ∈ gs, g.WellFormed m) + (x y : Fin m → Bool) : + (Circuit.run (Circuit.ofCodes m gs) x).ofLp y = + (pathGap gs (List.ofFn x) (List.ofFn y) : ℂ) * + (((Real.sqrt 2)⁻¹ : ℝ) : ℂ) ^ hadamardCount gs := by + have h := sgn_mul_run_ofCodes_apply gs hgs x y false + simp only [sgn, Bool.false_eq_true, ite_false, one_mul] at h + rw [h, pathGap, Int.cast_sum] + rfl + +/-- The simulation keeps the register length. -/ +private theorem length_foldl_pathStep (gs : List GateCode) (s π : List Bool) (σ : Bool) : + (gs.foldl pathStep (s, π, σ)).1.length = s.length := by + induction gs generalizing s π σ with + | nil => rfl + | cons g gs ih => + obtain ⟨_ | _, t, cs⟩ := g <;> simp only [List.foldl_cons, pathStep, ih, List.length_set] + +private theorem pathTerm_eq (gs : List GateCode) (x y π : List Bool) : + pathTerm gs x y π = + if (pathRun gs x π).1 = y then (if (pathRun gs x π).2 then -1 else 1) else 0 := + rfl + +private theorem acceptTerm_eq (gs : List GateCode) (x π π' : List Bool) : + acceptTerm gs x π π' = + if (pathRun gs x π).1 = (pathRun gs x π').1 ∧ (pathRun gs x π).1.headD false = true then + (if (pathRun gs x π).2 ^^ (pathRun gs x π').2 then -1 else 1) else 0 := + rfl + +/-- Summing the products of two path contributions over the accepting outcomes gives the +contribution of the pair. -/ +private theorem sum_accepting_pathTerm_mul (hm : 0 < m) (gs : List GateCode) (x π π' : List Bool) + (hx : x.length = m) : + ∑ y ∈ accepting m, pathTerm gs x (List.ofFn y) π * pathTerm gs x (List.ofFn y) π' = + acceptTerm gs x π π' := by + have hs : (pathRun gs x π).1.length = m := (length_foldl_pathStep gs x π false).trans hx + simp only [pathTerm_eq, acceptTerm_eq] + generalize pathRun gs x π = r at hs ⊢ + generalize pathRun gs x π' = r' + obtain ⟨s, σ⟩ := r + obtain ⟨s', σ'⟩ := r' + dsimp only at hs ⊢ + let y₀ : Fin m → Bool := fun i => s.getD i false + have hs₀ : s = List.ofFn y₀ := by + apply List.ext_getElem (by simp [hs]) + intro i h₁ h₂ + simp [y₀, List.getD_eq_getElem?_getD, h₁] + have hiff (y : Fin m → Bool) : s = List.ofFn y ↔ y = y₀ := by + rw [hs₀, List.ofFn_inj, eq_comm] + simp only [hiff, ite_mul, zero_mul] + rw [Finset.sum_ite_eq' (accepting m) y₀] + have hacc : y₀ ∈ accepting m ↔ s.headD false = true := by + rw [mem_accepting hm] + simp only [y₀] + cases s with + | nil => simp at hs; omega + | cons b s => rfl + by_cases h₀ : y₀ ∈ accepting m + · simp only [h₀, ite_true, ← hs₀, hacc.mp h₀, and_true] + by_cases hss : s = s' + · subst hss + cases σ <;> cases σ' <;> simp + · simp [hss, Ne.symm hss] + · simp only [h₀, ite_false, mt hacc.mpr h₀, Bool.false_eq_true, and_false] + +/-- The squared amplitude gaps of the accepting outcomes sum to the acceptance gap. -/ +private theorem sum_accepting_pathGap_sq (hm : 0 < m) (gs : List GateCode) (x : List Bool) + (hx : x.length = m) : + ∑ y ∈ accepting m, pathGap gs x (List.ofFn y) ^ 2 = acceptGap gs x := by + simp only [pathGap, sq, Finset.sum_mul_sum, acceptGap] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun π _ => ?_ + rw [Finset.sum_comm] + exact Finset.sum_congr rfl fun π' _ => sum_accepting_pathTerm_mul hm gs x _ _ hx + +/-- **The acceptance probability is a gap over `2^h`**: for well-formed codes on `m > 0` qubits, +the acceptance probability is `acceptGap` divided by `2^h`, where `h` counts the Hadamard +gates. -/ +theorem acceptProb_eq_acceptGap (hm : 0 < m) (gs : List GateCode) + (hgs : ∀ g ∈ gs, g.WellFormed m) (x : List Bool) : + acceptProb m gs x = + (acceptGap gs (List.ofFn (inputState m x)) : ℝ) / 2 ^ hadamardCount gs := by + have hnorm (g : ℤ) : + ‖(g : ℂ) * (((Real.sqrt 2)⁻¹ : ℝ) : ℂ) ^ hadamardCount gs‖ ^ 2 = + (g : ℝ) ^ 2 / 2 ^ hadamardCount gs := by + rw [norm_mul, norm_pow, Complex.norm_real, Real.norm_eq_abs, abs_inv, + abs_of_nonneg (Real.sqrt_nonneg 2), Complex.norm_intCast, mul_pow, sq_abs, ← pow_mul, + mul_comm (hadamardCount gs) 2, pow_mul, inv_pow, Real.sq_sqrt (by norm_num), inv_pow, + div_eq_mul_inv] + rw [acceptProb, measureProb] + simp only [run_ofCodes_apply gs hgs, hnorm, ← Finset.sum_div] + congr 1 + exact_mod_cast sum_accepting_pathGap_sq hm gs _ (by simp) + +end Cslib.Quantum diff --git a/Complexity/Computability/Complexity/Classes/BQP/Counting.lean b/Complexity/Computability/Complexity/Classes/BQP/Counting.lean new file mode 100644 index 000000000..c931057a4 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/BQP/Counting.lean @@ -0,0 +1,182 @@ +/- +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.Complexity.Classes.BQP +public import Complexity.Computability.Circuit.Quantum.PathSum +public import Complexity.Computability.Complexity.Classes.AWPP +import Complexity.Computability.Complexity.Classes.SharpP.Aggregation +import Complexity.Computability.Complexity.Classes.SharpP.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Tactic.PolyTime + +/-! +# `BQP ⊆ AWPP ⊆ PP` + +The acceptance probability of a uniform family of Hadamard–Toffoli circuits is a gap function +divided by a power of two, `acceptGap / 2^h` (`Cslib.Quantum.acceptProb_eq_acceptGap`). Here both +are computed classically. The path simulation `Cslib.Quantum.pathStep` runs in polynomial time +(`Cslib.Quantum.computableInPolyTime_pathStep`), so the acceptance gap is a sum, over pairs of +polynomially long paths, of a polynomial-time integer, which is a `GapP` function; the number `h` +of Hadamard gates is computed in unary. Fenner's characterization of AWPP +(`Cslib.Complexity.AWPP`) then gives `BQP ⊆ AWPP` (`Cslib.Complexity.BQP_subset_AWPP`), and +`AWPP ⊆ PP` gives `BQP ⊆ PP` (`Cslib.Complexity.BQP_subset_PP`). + +`BQP ⊆ PP` is due to Adleman, DeMarrais and Huang +[Adleman, DeMarrais, Huang][AdlemanDeMarraisHuang1997]. `BQP ⊆ AWPP` is Theorem 3.1 of +[Fortnow, Rogers][FortnowRogers1999], proved there through Lemma 3.2: the acceptance probability of +a quantum Turing machine running for `t` steps, with amplitudes in `{0, ±3/5, ±4/5, ±1}`, is a GapP +function divided by `5^{2t}`. For circuits over the Hadamard and Toffoli gates the denominator is +`2^h` instead. Fortnow and Rogers work with quantum Turing machines; this file works with the +uniform circuit families of `Cslib.Complexity.BQP`. + +## Main results + +* `Cslib.Quantum.computableInPolyTime_pathStep`, + `Cslib.Quantum.computableInPolyTime_foldl_pathStep`: the path simulation runs in polynomial + time. +* `Cslib.Complexity.acceptGap_mem_GapP`: the acceptance gap of a uniform family is `GapP`. +* `Cslib.Complexity.BQP_subset_AWPP`, `Cslib.Complexity.BQP_subset_PP`. + +## References + +* [L. Adleman, J. DeMarrais, M.-D. Huang, *Quantum computability*][AdlemanDeMarraisHuang1997] +* [L. Fortnow, J. Rogers, *Complexity limitations on quantum computation*][FortnowRogers1999] +* [S. Fenner, *PP-Lowness and a Simple Definition of AWPP*][Fenner2003] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Turing.MultiTapeTM + +/-- One simulation step, written with polynomial-time list operations. -/ +private theorem pathStep_eq (p : (List Bool × List Bool × Bool) × GateCode) : + pathStep p.1 p.2 = + if p.2.1 then + (if p.2.2.1 < p.1.1.length then + p.1.1.take p.2.2.1 ++ p.1.2.1.headD false :: p.1.1.drop (p.2.2.1 + 1) else p.1.1, + p.1.2.1.tail, p.1.2.2 ^^ (p.1.1.getD p.2.2.1 false && p.1.2.1.headD false)) + else + (if p.2.2.1 < p.1.1.length then + p.1.1.take p.2.2.1 ++ + (p.1.1.getD p.2.2.1 false ^^ p.2.2.2.all fun c => p.1.1.getD c false) :: + p.1.1.drop (p.2.2.1 + 1) else p.1.1, + p.1.2.1, p.1.2.2) := by + obtain ⟨⟨s, π, σ⟩, ⟨_ | _, t, cs⟩⟩ := p <;> + simp only [pathStep, List.set_eq_take_append_cons_drop] <;> rfl + +/-- **The path simulation step runs in polynomial time**, with the register and the unread path +as raw bit strings. -/ +theorem computableInPolyTime_pathStep : + ComputableInPolyTime (fun p : (List Bool × List Bool × Bool) × GateCode => pathStep p.1 p.2) + (encPair (encPair encBits (encPair encBits encBool)) encGateCode) + (encPair encBits (encPair encBits encBool)) := by + simp only [pathStep_eq] + fun_prop + +/-- A simulation step never lengthens the encoded state. -/ +private theorem length_encPair_pathStep (st : List Bool × List Bool × Bool) (g : GateCode) : + (encPair encBits (encPair encBits encBool) (pathStep st g)).length ≤ + (encPair encBits (encPair encBits encBool) st).length + 0 := by + obtain ⟨s, π, σ⟩ := st + obtain ⟨_ | _, t, cs⟩ := g <;> simp [pathStep] + +/-- **The path simulation runs in polynomial time** on computed gate codes and initial states. -/ +theorem computableInPolyTime_foldl_pathStep {γ : Type} {encIn : γ ↪ List Bool} + {gs : γ → List GateCode} {init : γ → List Bool × List Bool × Bool} + (hgs : ComputableInPolyTime gs encIn (encList encGateCode)) + (hinit : ComputableInPolyTime init encIn (encPair encBits (encPair encBits encBool))) : + ComputableInPolyTime (fun c => (gs c).foldl pathStep (init c)) encIn + (encPair encBits (encPair encBits encBool)) := + ComputableInPolyTime.foldl_of_bounded_growth hgs hinit computableInPolyTime_pathStep + length_encPair_pathStep + +end Cslib.Quantum + +namespace Cslib.Complexity + +open Quantum Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} + +/-- **The acceptance gap of a uniform family is a `GapP` function** of the instance. -/ +theorem acceptGap_mem_GapP (F : UniformCircuitFamily) : + (fun a => acceptGap (F.gates (enc a).length) + (List.ofFn (inputState (F.width (enc a).length) (enc a)))) ∈ GapP enc := by + have hgates := F.computableInPolyTime_gates + have hwidth := F.computableInPolyTime_width + -- the input register and the number of Hadamard gates + let X : α → List Bool := fun a => + enc a ++ List.replicate (F.width (enc a).length - (enc a).length) false + have hX : ComputableInPolyTime X enc encBits := by dsimp only [X]; fun_prop + let h : α → ℕ := fun a => hadamardCount (F.gates (enc a).length) + have hh : ComputableInPolyTime h enc encUnary := by + simp only [h, hadamardCount_eq_countP] + fun_prop + -- the simulations along the two paths of a pair + let run₁ : (α × List Bool) × List Bool → List Bool × List Bool × Bool := fun p => + (F.gates (enc p.1.1).length).foldl pathStep (X p.1.1, p.1.2, false) + let run₂ : (α × List Bool) × List Bool → List Bool × List Bool × Bool := fun p => + (F.gates (enc p.1.1).length).foldl pathStep (X p.1.1, p.2, false) + have hrun₁ : ComputableInPolyTime run₁ (encPair (encPair enc encBits) encBits) + (encPair encBits (encPair encBits encBool)) := + computableInPolyTime_foldl_pathStep (by fun_prop) (by fun_prop) + have hrun₂ : ComputableInPolyTime run₂ (encPair (encPair enc encBits) encBits) + (encPair encBits (encPair encBits encBool)) := + computableInPolyTime_foldl_pathStep (by fun_prop) (by fun_prop) + let T : (α × List Bool) × List Bool → ℤ := fun p => + if (run₁ p).1 = (run₂ p).1 ∧ (run₁ p).1.headD false = true then + (if (run₁ p).2.2 ^^ (run₂ p).2.2 then -1 else 1) else 0 + have hT : T ∈ GapP (encPair (encPair enc encBits) encBits) := + mem_GapP_of_polyTime (by dsimp only [T]; fun_prop) + have hinner := GapP.sum_bits_mem hT (r := fun p : α × List Bool => h p.1) (by fun_prop) + have houter := GapP.sum_bits_mem hinner hh + convert houter using 2 with a + rw [ofFn_inputState (F.le_width _)] + rfl + +/-- **`BQP ⊆ AWPP`** [Fortnow, Rogers][FortnowRogers1999]: the acceptance probability of a uniform +family is a `GapP` function divided by `2^h`, with `h` computed in polynomial time. -/ +theorem BQP_subset_AWPP : BQP enc ⊆ AWPP enc := by + rintro A ⟨F, hF⟩ + refine mem_AWPP_of_polyTime_exponent (acceptGap_mem_GapP F) + (r := fun a => hadamardCount (F.gates (enc a).length)) + (by + have := F.computableInPolyTime_gates + simp only [hadamardCount_eq_countP] + fun_prop) (fun a => ?_) + have hp := acceptProb_eq_acceptGap (F.width_pos (enc a).length) _ + (F.wellFormed (enc a).length) (enc a) + set g := acceptGap (F.gates (enc a).length) + (List.ofFn (inputState (F.width (enc a).length) (enc a))) + set r := hadamardCount (F.gates (enc a).length) + have hpos : (0 : ℝ) < 2 ^ r := by positivity + have h0 := F.acceptProb_nonneg (enc a) + have h1 := F.acceptProb_le_one (enc a) + change F.acceptProb (enc a) = _ at hp + rw [hp, le_div_iff₀ hpos, zero_mul] at h0 + rw [hp, div_le_iff₀ hpos, one_mul] at h1 + refine ⟨⟨by exact_mod_cast h0, by exact_mod_cast h1⟩, fun ha => ?_, fun ha => ?_⟩ + · have := (hF a).1 ha + rw [hp, le_div_iff₀ hpos] at this + have : (2 : ℝ) * 2 ^ r ≤ 3 * g := by linarith + exact_mod_cast this + · have := (hF a).2 ha + rw [hp, div_le_iff₀ hpos] at this + have : (3 : ℝ) * g ≤ 2 ^ r := by linarith + exact_mod_cast this + +/-- **`BQP ⊆ PP`** [Adleman, DeMarrais, Huang][AdlemanDeMarraisHuang1997]. -/ +theorem BQP_subset_PP : BQP enc ⊆ PP enc := + fun _ hA => AWPP_subset_PP (BQP_subset_AWPP hA) + +end Cslib.Complexity diff --git a/Complexity/Foundations/Data/List/Lookup.lean b/Complexity/Foundations/Data/List/Lookup.lean index f2c393806..ba37be219 100644 --- a/Complexity/Foundations/Data/List/Lookup.lean +++ b/Complexity/Foundations/Data/List/Lookup.lean @@ -28,6 +28,7 @@ import Mathlib.Data.List.OfFn * `List.getD_take_drop`: reading an in-range entry of `(l.drop k).take w` reads index `k + i` of `l`. * `List.getD_ofFn_of_lt`, `List.getD_ofFn`: reading `List.ofFn f` at a valid index returns `f`. +* `List.set_ofFn`: updating `List.ofFn f` tabulates the updated function. * `List.forall_mem_set_of_forall_mem`, `List.getD_le_of_forall_le`: preserve invariants under updates and bound defaulted reads of numeric register files. * `List.getD_map_range`: read a function tabulated over a bounded range. @@ -87,6 +88,15 @@ theorem List.getD_ofFn {α : Type*} {n : ℕ} (f : Fin n → α) (i : Fin n) (d (List.ofFn f).getD i d = f i := List.getD_ofFn_of_lt f i.isLt d +/-- Updating `List.ofFn f` at `i : Fin n` tabulates the updated function. -/ +theorem List.set_ofFn {α : Type*} {n : ℕ} (f : Fin n → α) (i : Fin n) (a : α) : + (List.ofFn f).set i a = List.ofFn (Function.update f i a) := by + classical + apply List.ext_getElem (by simp) + intro j hj _ + simp only [List.getElem_set, List.getElem_ofFn, Function.update_apply, Fin.ext_iff] + split_ifs <;> first | rfl | omega + /-- A property of all the entries of a list holds of all the entries of an update by a value having it. -/ theorem List.forall_mem_set_of_forall_mem {α : Type*} {p : α → Prop} {l : List α} {i : ℕ} {x : α} diff --git a/ComplexityTests/BQPCounting.lean b/ComplexityTests/BQPCounting.lean new file mode 100644 index 000000000..38706a002 --- /dev/null +++ b/ComplexityTests/BQPCounting.lean @@ -0,0 +1,55 @@ +/- +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.Counting +import ComplexityTests.BQP + +/-! `BQP ⊆ AWPP ⊆ PP`: concrete path counts, interference in the counts, and the inclusions +applied to a language in `BQP`. -/ + +namespace ComplexityTests.BQPCounting + +open Cslib Cslib.Quantum Cslib.Complexity Turing.MultiTapeTM ComplexityTests.BQP + +/-! ### Path simulation -/ + +-- The Toffoli code flips its target only when both controls are one. +example : pathRun [(false, 2, [0, 1])] [true, true, false] [] = ([true, true, true], false) := by + decide +example : pathRun [(false, 2, [0, 1])] [true, false, false] [] = ([true, false, false], false) := by + decide + +-- A Hadamard gate writes the path bit and records the sign `(-1)^{1·1}`. +example : pathRun [(true, 0, [])] [true] [true] = ([true], true) := by decide +example : pathRun [(true, 0, [])] [true] [false] = ([false], false) := by decide + +/-! ### Amplitudes and acceptance as counts -/ + +-- `H|1⟩ = (|0⟩ - |1⟩)/√2`: the amplitude gaps of the two outcomes are `1` and `-1`. +example : pathGap [(true, 0, [])] [true] [false] = 1 := by decide +example : pathGap [(true, 0, [])] [true] [true] = -1 := by decide + +-- One Hadamard gate: one of the four pairs of paths accepts, so the probability is `1 / 2^1`. +example : acceptGap [(true, 0, [])] [false] = 1 := by decide + +-- Two Hadamard gates interfere. From `|0⟩` the four accepting pairs cancel (probability `0`); +-- from `|1⟩` they add up to `4 = 2^2` (probability `1`). +example : acceptGap [(true, 0, []), (true, 0, [])] [false] = 0 := by decide +example : acceptGap [(true, 0, []), (true, 0, [])] [true] = 4 := by decide + +-- The count agrees with the quantum acceptance probability of `hadamardOnce`. +example : acceptProb 1 [(true, 0, [])] [] = 1 / 2 := by + rw [acceptProb_eq_acceptGap (by norm_num) _ (by decide)] + have : List.ofFn (inputState 1 []) = [false] := by decide + rw [this, show acceptGap [(true, 0, [])] [false] = 1 by decide] + norm_num + +/-! ### The inclusions -/ + +example : FirstBit ∈ AWPP encBits := BQP_subset_AWPP firstBit_mem_BQP +example : FirstBitᶜ ∈ PP encBits := BQP_subset_PP (compl_mem_BQP firstBit_mem_BQP) + +end ComplexityTests.BQPCounting diff --git a/references.bib b/references.bib index de1189a35..510183533 100644 --- a/references.bib +++ b/references.bib @@ -1732,6 +1732,19 @@ @article{FortnowReingold1996 doi = {10.1006/inco.1996.0001} } +@article{FortnowRogers1999, + author = {Fortnow, Lance and Rogers, John}, + title = {Complexity Limitations on Quantum Computation}, + journal = {Journal of Computer and System Sciences}, + volume = {59}, + number = {2}, + pages = {240--252}, + year = {1999}, + doi = {10.1006/jcss.1999.1651}, + eprint = {cs/9811023}, + archivePrefix = {arXiv} +} + @article{FortnowSanthanam2006, author = {Fortnow, Lance and Santhanam, Rahul}, title = {Recent Work on Hierarchies for Semantic Classes},