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/5] 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 e6f116c6e2..7accc0251c 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 0000000000..0ee18bbd6c --- /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 0000000000..b612a5435e --- /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 0000000000..3ef377f94e --- /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 63b40ca6c3..b13c060331 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 0000000000..6a838bba71 --- /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 248ed73df9..de1189a35b 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/5] =?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 7accc0251c..06ecbcd13e 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 0000000000..f06efa4713 --- /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 0000000000..c931057a4e --- /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 f2c3938068..ba37be2198 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 0000000000..38706a002f --- /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 de1189a35b..510183533b 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}, From e2446386ca64e311fa7ab4f31f2399dba2e373fb Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 00:56:54 -0400 Subject: [PATCH 3/5] =?UTF-8?q?feat(abstracts):=20candidate=20abstract=20f?= =?UTF-8?q?or=20BQP=20=E2=8A=86=20PP=20(#896)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Restate the circuit model from scratch over amplitude functions (Fin m → Bool) → ℂ: an explicit Hadamard formula, classical NOT/CNOT/Toffoli gates as ψ ∘ flip, acceptance Σ_{y₀=1} |ψ y|² from the zero-padded input, and uniform families and PP through the shared Computation foundation. The bridge proves the formulas agree with Circuit.run ∘ Circuit.ofCodes on well-formed codes, that the restated class is Cslib.Complexity.BQP, and derives the headline from BQP_subset_PP. The audit allows only Encoding and Computation. The renderer maps ℂ, ‖ and ± for pdflatex. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- ComplexityTests/Abstracts/BQPTests.lean | 71 +++++ abstracts/ComplexityAbstracts.lean | 2 + .../ComplexityAbstracts/BQPAbstract.lean | 200 ++++++++++++++ abstracts/ComplexityAbstracts/BQPBridge.lean | 251 ++++++++++++++++++ abstracts/README.md | 1 + abstracts/catalogue.json | 14 + scripts/abstract_to_tex.py | 3 + scripts/test_abstract_to_tex.py | 9 + 8 files changed, 551 insertions(+) create mode 100644 ComplexityTests/Abstracts/BQPTests.lean create mode 100644 abstracts/ComplexityAbstracts/BQPAbstract.lean create mode 100644 abstracts/ComplexityAbstracts/BQPBridge.lean diff --git a/ComplexityTests/Abstracts/BQPTests.lean b/ComplexityTests/Abstracts/BQPTests.lean new file mode 100644 index 0000000000..2ac7b64375 --- /dev/null +++ b/ComplexityTests/Abstracts/BQPTests.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract tests) + +import ComplexityAbstracts.BQPAbstract +import ComplexityTests.BQP + +/-! # Concrete clients of the public `BQP ⊆ PP` abstract + +The explicit gate formulas act as expected on small registers: Toffoli flips its target exactly +when both controls are one, and one Hadamard gate on qubit `0` accepts with probability `1/2`. The +first-bit language, decided exactly by a family without gates, is in the public `BQP`, so the +headline places it in the public `PP`. +-/ + +namespace ComplexityTests.Abstracts.BQPTests + +open ComplexityAbstracts ComplexityAbstracts.BQPAbstract + +/-! ### The explicit gates -/ + +-- Toffoli with controls `0, 1` and target `2` maps `110` to `111` and fixes `100`. +example : flip 2 [0, 1] (![true, true, false] : Fin 3 → Bool) = ![true, true, true] := by decide +example : flip 2 [0, 1] (![true, false, false] : Fin 3 → Bool) = ![true, false, false] := by + decide + +-- NOT on qubit `1`, and CNOT from qubit `0` to qubit `1`. +example : flip 1 [] (![false, false] : Fin 2 → Bool) = ![false, true] := by decide +example : flip 1 [0] (![true, true] : Fin 2 → Bool) = ![true, false] := by decide + +-- Well-formedness: a Toffoli gate needs three distinct qubits in range; Hadamard has no controls. +example : WellFormed 3 (false, 2, [0, 1]) := ⟨by decide, by decide, by decide⟩ +example : ¬WellFormed 3 (false, 1, [1]) := fun h => absurd h.2.1 (by decide) +example : ¬WellFormed 2 (true, 0, [1]) := fun h => absurd h.2 (by decide) + +/-- A single Hadamard gate on qubit `0` accepts with probability `1/2`, on every input. -/ +theorem acceptProb_hadamard (x : List Bool) : + acceptProb (x.length + 1) [(true, 0, [])] x = 1 / 2 := by + have hwf : ∀ g ∈ [((true, 0, []) : GateCode)], + Cslib.Quantum.GateCode.WellFormed (x.length + 1) g := by + intro g hg + rw [List.mem_singleton.mp hg] + exact ⟨Nat.succ_pos _, rfl⟩ + exact (BQPBridge.acceptProb_eq hwf x).trans (ComplexityTests.BQP.acceptProb_hadamardOnce x) + +/-! ### Membership and the headline -/ + +/-- The library's `BQP` is contained in the public one. -/ +theorem mem_BQP_of_mem {α : Type} {enc : α ↪ List Bool} {A : Set α} + (hA : A ∈ Cslib.Complexity.BQP enc) : A ∈ BQP enc := by + obtain ⟨width, gates, ⟨hwidth, hgates, hn⟩, hdec⟩ := BQPBridge.mem_BQP_iff.mpr hA + have hwf (m : ℕ) (g : GateCode) (h : Cslib.Quantum.GateCode.WellFormed m g) : + WellFormed m g := by + obtain ⟨_ | _, t, cs⟩ := g <;> exact h + exact ⟨width, gates, ⟨hwidth, hgates, fun n => ⟨(hn n).1, (hn n).2.1, + fun g hg => hwf _ g ((hn n).2.2 g hg)⟩⟩, hdec⟩ + +/-- Words whose first bit is one are in the public `BQP`. -/ +theorem firstBit_mem_BQP : + ComplexityTests.BQP.FirstBit ∈ BQP ComplexityTests.Abstracts.Encoding.encBits := + mem_BQP_of_mem ComplexityTests.BQP.firstBit_mem_BQP + +/-- The headline then places them in the public `PP`. -/ +example : ComplexityTests.BQP.FirstBit ∈ PP ComplexityTests.Abstracts.Encoding.encBits := + BQP_subset_PP _ firstBit_mem_BQP + +end ComplexityTests.Abstracts.BQPTests diff --git a/abstracts/ComplexityAbstracts.lean b/abstracts/ComplexityAbstracts.lean index c551d512fc..fd467a7408 100644 --- a/abstracts/ComplexityAbstracts.lean +++ b/abstracts/ComplexityAbstracts.lean @@ -1,3 +1,5 @@ +import ComplexityAbstracts.BQPAbstract +import ComplexityAbstracts.BQPBridge import ComplexityAbstracts.BarringtonAbstract import ComplexityAbstracts.BarringtonBridge import ComplexityAbstracts.BravermanAbstract diff --git a/abstracts/ComplexityAbstracts/BQPAbstract.lean b/abstracts/ComplexityAbstracts/BQPAbstract.lean new file mode 100644 index 0000000000..2ded8a5b3e --- /dev/null +++ b/abstracts/ComplexityAbstracts/BQPAbstract.lean @@ -0,0 +1,200 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract library) + +import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation +import ComplexityAbstracts.BQPBridge + +/-! # BQP is contained in PP + +A quantum computer that answers correctly with probability at least `2/3` can be simulated by a +classical machine that decides by an unbounded-error majority vote. Adleman, DeMarrais and Huang +proved `BQP ⊆ PP` for quantum machines with algebraic amplitudes. The proof sums over computation +paths. Each Hadamard gate splits a path in two with amplitude `±2^{-1/2}`, and classical gates +permute basis strings. The acceptance probability is therefore `g / 2^h`, where `h` counts the +Hadamard gates and `g` is a difference of two counts of polynomially checkable path pairs. Deciding +whether it exceeds `1/2` is a question about a strict majority of certificates, which is the class +`PP`. Fortnow and Rogers sharpened the containment to `BQP ⊆ AWPP`. The library proves that +containment as an intermediate step, but this abstract does not state it. + +The model is restated from scratch below. A state of an `m`-qubit register is an amplitude function +on basis strings. Each gate is an explicit formula on amplitudes. A uniform family is computed by +one polynomial-time machine, using the shared foundation `Computation.PolyTime`. The class `PP` uses +the shared `Computation.PolyTimeVerifier`. + +**Gate set.** Circuits use one fixed finite gate set: the Hadamard gate and the classical reversible +gates NOT, CNOT and Toffoli. Their matrix entries lie in `{0, ±1, ±2^{-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 are +universal [Shi; Aharonov], and with the Solovay–Kitaev theorem, circuits over them simulate circuits +of arbitrary elementary operations with polynomial overhead and small error. This equivalence is a +cited remark; it is not formalized here. A fixed finite gate set matters: Adleman, DeMarrais and +Huang show that with arbitrary complex amplitudes, `BQP` would contain uncountably many languages. + +A reader only needs to inspect the definitions and the theorem statement in this file, and the +displayed shared foundations, to check that it states the intended claim. Lean checks the proof +through `BQPBridge`. The bridge proves that the formulas here agree with the library's unitary +circuit semantics on well-formed gates. `#check_abstract` audits that the public statements depend +only on this file, the shared foundations `Encoding` and `Computation`, and the background libraries +Lean, Mathlib and upstream CSLib. + +## References + +* [L. Adleman, J. DeMarrais, M.-D. Huang, *Quantum computability*][AdlemanDeMarraisHuang1997] +* [L. Fortnow, J. Rogers, *Complexity limitations on quantum computation*][FortnowRogers1999] +* [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] +-/ + +namespace ComplexityAbstracts.BQPAbstract + +/-! ## Quantum circuits on amplitudes + +A basis string of an `m`-qubit register is a bit string `y : Fin m → Bool`. A state is one complex +amplitude `ψ y` for each basis string. Gates act on amplitudes by the explicit formulas below. +Measuring a state `ψ` of norm one gives the outcome `y` with probability `|ψ y|²`. +-/ + +/-- The state of an `m`-qubit register: one complex amplitude for each basis string. -/ +abbrev State (m : ℕ) := (Fin m → Bool) → ℂ + +/-- Bit `i` of a basis string `y`, written `y_i`. A position past the end reads `false`; the +well-formed gates below never use one. -/ +def bit {m : ℕ} (y : Fin m → Bool) (i : ℕ) : Bool := if h : i < m then y ⟨i, h⟩ else false + +/-- The basis string `y[t ↦ c]`, that is, `y` with bit `t` set to `c`. -/ +def setBit {m : ℕ} (y : Fin m → Bool) (t : ℕ) (c : Bool) : Fin m → Bool := + fun i => if (i : ℕ) = t then c else y i + +/-- The **Hadamard gate** on qubit `t`: +`(H ψ)(y) = 2^{-1/2} Σ_{c ∈ {0,1}} (-1)^{c · y_t} ψ(y[t ↦ c])`. +On qubit `t` it maps `|0⟩ ↦ 2^{-1/2}(|0⟩ + |1⟩)` and `|1⟩ ↦ 2^{-1/2}(|0⟩ - |1⟩)`. -/ +noncomputable def hadamard {m : ℕ} (t : ℕ) (ψ : State m) : State m := fun y => + ((Real.sqrt 2 : ℝ) : ℂ)⁻¹ * ∑ c : Bool, (if c && bit y t then -1 else 1) * ψ (setBit y t c) + +/-- Flip bit `t` of a basis string when every bit of `cs` is one. With no controls this is NOT, +with one control CNOT, and with two controls Toffoli. When `t ∉ cs` the map is its own inverse. -/ +def flip {m : ℕ} (t : ℕ) (cs : List ℕ) (y : Fin m → Bool) : Fin m → Bool := + setBit y t (bit y t ^^ cs.all (bit y)) + +/-- A **classical gate** permutes the basis, `|z⟩ ↦ |flip t cs z⟩`. On amplitudes it is +`ψ ∘ flip t cs`, because `flip t cs` is its own inverse. -/ +def classical {m : ℕ} (t : ℕ) (cs : List ℕ) (ψ : State m) : State m := ψ ∘ flip t cs + +/-- A **gate code** `(h, t, cs)`. The code `(true, t, [])` is the Hadamard gate on qubit `t`, and +`(false, t, cs)` is the classical gate with target `t` and controls `cs`. Uniform machines output +circuits as lists of gate codes. -/ +abbrev GateCode := Bool × ℕ × List ℕ + +/-- A gate code is **well formed** on `m` qubits when its qubits are distinct and below `m`. A +Hadamard code has no controls, and a classical code has at most two. -/ +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 + +/-- The gate that a gate code denotes. -/ +noncomputable def applyGate {m : ℕ} (g : GateCode) (ψ : State m) : State m := + if g.1 then hadamard g.2.1 ψ else classical g.2.1 g.2.2 ψ + +/-- Run a circuit, given as a list of gate codes applied first to last, on the state `ψ`. -/ +noncomputable def run {m : ℕ} (gs : List GateCode) (ψ : State m) : State m := + gs.foldl (fun ψ g => applyGate g ψ) ψ + +/-- The basis state `|z⟩`: amplitude one at `z` and zero elsewhere. -/ +def basis {m : ℕ} (z : Fin m → Bool) : State m := fun y => if y = z then 1 else 0 + +/-- The input word `x` padded with zeros to `m` bits, `x 0^{m - |x|}`. -/ +def pad (m : ℕ) (x : List Bool) : Fin m → Bool := fun i => x.getD i false + +/-- The **acceptance probability** of the circuit `gs` on `m` qubits and input `x`. The circuit +starts in `|x 0^{m - |x|}⟩`, and the whole register is then measured. The circuit accepts when +qubit `0` reads `1`, which has probability `Σ_{y : y_0 = 1} |ψ y|²` for the final state `ψ`. -/ +noncomputable def acceptProb (m : ℕ) (gs : List GateCode) (x : List Bool) : ℝ := + ∑ y : Fin m → Bool, if bit y 0 then ‖run gs (basis (pad m x)) y‖ ^ 2 else 0 + +/-! ## Representation details + +A uniform machine outputs the list of gate codes. The flag bit is a single bit. The target and +controls are written in unary, so every qubit index is bounded by the machine's output length and +is polynomial in the input length. +-/ + +/-- The encoding of a gate code `(h, t, cs)`: the bit `h`, then `t` and the list `cs` in unary. -/ +abbrev encGateCode : GateCode ↪ List Bool := + ComplexityTests.Abstracts.Encoding.encPair ComplexityTests.Abstracts.Encoding.encBool + (ComplexityTests.Abstracts.Encoding.encPair ComplexityTests.Abstracts.Encoding.encUnary + (ComplexityTests.Abstracts.Encoding.encList ComplexityTests.Abstracts.Encoding.encUnary)) + +/-! ## Uniform families and the classes + +The circuit for inputs of length `n` acts on `width n` qubits and has the gate codes `gates n`. A +single polynomial-time machine computes both from `n` written in unary, as in Arora and Barak's +uniform circuit families. Qubit `0` is the output qubit, so the register has at least one qubit, +and the input fits into it, so it has at least `n`. +-/ + +/-- `width` and `gates` form a **polynomial-time uniform circuit family**. Both are computable in +polynomial time from `n` in unary. The register for inputs of length `n` has at least `n` qubits +and at least one, and every gate code of `gates n` is well formed on it. -/ +def Uniform (width : ℕ → ℕ) (gates : ℕ → List GateCode) : Prop := + ComplexityTests.Abstracts.Computation.PolyTime width + ComplexityTests.Abstracts.Encoding.encUnary ComplexityTests.Abstracts.Encoding.encUnary ∧ + ComplexityTests.Abstracts.Computation.PolyTime gates + ComplexityTests.Abstracts.Encoding.encUnary + (ComplexityTests.Abstracts.Encoding.encList encGateCode) ∧ + ∀ n, n ≤ width n ∧ 0 < width n ∧ ∀ g ∈ gates n, WellFormed (width n) g + +/-- **Bounded-error quantum polynomial time** [Bernstein, Vazirani][BernsteinVazirani1997]. A +uniform family decides `A` when it 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`. -/ +def BQP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := + {A | ∃ (width : ℕ → ℕ) (gates : ℕ → List GateCode), Uniform width gates ∧ ∀ a, + (a ∈ A → 2 / 3 ≤ acceptProb (width (enc a).length) (gates (enc a).length) (enc a)) ∧ + (a ∉ A → acceptProb (width (enc a).length) (gates (enc a).length) (enc a) ≤ 1 / 3)} + +/-- The number of binary strings of exactly `n` bits that `V` accepts with the instance `a`. -/ +def acceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card + +/-- **Probabilistic polynomial time with unbounded error.** A problem `A` is in `PP` when one +total polynomial-time verifier `V` and one polynomial `p` exist with the following property: +`a ∈ A` exactly when strictly more than half of the `2^{p(|enc a|)}` strings `r` of length +`p(|enc a|)` give `V (a, r) = true`. -/ +def PP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := + {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), + ComplexityTests.Abstracts.Computation.PolyTimeVerifier enc V ∧ + ∀ a, a ∈ A ↔ 2 ^ p.eval (enc a).length < 2 * acceptCount V a (p.eval (enc a).length)} + +/-! ## Main result -/ + +/-- **BQP ⊆ PP** [Adleman, DeMarrais, Huang][AdlemanDeMarraisHuang1997]: every problem decided +with bounded error by a uniform family of circuits over the Hadamard, NOT, CNOT and Toffoli gates +is decided by a polynomial-time strict-majority vote, for every instance encoding. -/ +theorem BQP_subset_PP {α : Type} (enc : α ↪ List Bool) : BQP enc ⊆ PP enc := by + rintro A ⟨width, gates, ⟨hwidth, hgates, hn⟩, hdec⟩ + have hwf (m : ℕ) (g : GateCode) (h : WellFormed m g) : + Cslib.Quantum.GateCode.WellFormed m g := by + obtain ⟨_ | _, t, cs⟩ := g <;> exact h + exact BQPBridge.BQP_subset_PP enc + ⟨width, gates, ⟨hwidth, hgates, fun n => ⟨(hn n).1, (hn n).2.1, + fun g hg => hwf _ g ((hn n).2.2 g hg)⟩⟩, hdec⟩ + +/-- +info: abstract audit passed for `ComplexityAbstracts.BQPAbstract`: 22 root +declarations +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityAbstracts.BQPAbstract allowing [ + ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation +] + +end ComplexityAbstracts.BQPAbstract diff --git a/abstracts/ComplexityAbstracts/BQPBridge.lean b/abstracts/ComplexityAbstracts/BQPBridge.lean new file mode 100644 index 0000000000..cc20937bb0 --- /dev/null +++ b/abstracts/ComplexityAbstracts/BQPBridge.lean @@ -0,0 +1,251 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract library) + +import ComplexityAbstracts.Check +import ComplexityAbstracts.Encoding +import ComplexityAbstracts.Computation +import Complexity.Computability.Complexity.Classes.BQP.Counting + +/-! +# Bridge for the `BQP ⊆ PP` formal abstract + +`BQPAbstract.lean` restates quantum states, gates, circuit runs and acceptance as explicit formulas +on amplitude functions `(Fin m → Bool) → ℂ`. This module repeats those formulas and proves that +they agree with the library's circuits: + +* a well-formed gate code acts on amplitudes as its formula says + (`ComplexityAbstracts.BQPBridge.ofLp_eval_toPlacedGate`), from the library's action on basis + states (`Cslib.Quantum.GateCode.eval_toPlacedGate_ket`, + `Cslib.Quantum.GateCode.eval_toPlacedGate_hadamard_ket`); +* hence a run of well-formed codes is `Cslib.Quantum.Circuit.run ∘ Cslib.Quantum.Circuit.ofCodes` + (`ComplexityAbstracts.BQPBridge.ofLp_eval_ofCodes`), and the explicit acceptance probability is + `Cslib.Quantum.acceptProb` (`ComplexityAbstracts.BQPBridge.acceptProb_eq`); +* the restated class is `Cslib.Complexity.BQP` (`ComplexityAbstracts.BQPBridge.mem_BQP_iff`), and + the restated `PP` is `Cslib.Complexity.PP` by unfolding, so `Cslib.Complexity.BQP_subset_PP` + gives the headline (`ComplexityAbstracts.BQPBridge.BQP_subset_PP`). +-/ + +namespace ComplexityAbstracts.BQPBridge + +open ComplexityTests.Abstracts Cslib.Quantum Finset + +/-! ### The explicit model, as in the abstract -/ + +/-- The amplitudes of an `m`-qubit state, indexed by basis strings. -/ +abbrev State (m : ℕ) := (Fin m → Bool) → ℂ + +/-- Bit `i` of a basis string, `false` past its end. -/ +def bit {m : ℕ} (y : Fin m → Bool) (i : ℕ) : Bool := if h : i < m then y ⟨i, h⟩ else false + +/-- The basis string `y` with bit `t` set to `c`. -/ +def setBit {m : ℕ} (y : Fin m → Bool) (t : ℕ) (c : Bool) : Fin m → Bool := + fun i => if (i : ℕ) = t then c else y i + +/-- The Hadamard gate on qubit `t`. -/ +noncomputable def hadamard {m : ℕ} (t : ℕ) (ψ : State m) : State m := fun y => + ((Real.sqrt 2 : ℝ) : ℂ)⁻¹ * ∑ c : Bool, (if c && bit y t then -1 else 1) * ψ (setBit y t c) + +/-- Flip bit `t` when every bit of `cs` is one. -/ +def flip {m : ℕ} (t : ℕ) (cs : List ℕ) (y : Fin m → Bool) : Fin m → Bool := + setBit y t (bit y t ^^ cs.all (bit y)) + +/-- The classical gate with target `t` and controls `cs`. -/ +def classical {m : ℕ} (t : ℕ) (cs : List ℕ) (ψ : State m) : State m := ψ ∘ flip t cs + +/-- The gate denoted by a gate code. -/ +noncomputable def applyGate {m : ℕ} (g : GateCode) (ψ : State m) : State m := + if g.1 then hadamard g.2.1 ψ else classical g.2.1 g.2.2 ψ + +/-- Apply gate codes first to last. -/ +noncomputable def run {m : ℕ} (gs : List GateCode) (ψ : State m) : State m := + gs.foldl (fun ψ g => applyGate g ψ) ψ + +/-- The basis state `|z⟩`. -/ +def basis {m : ℕ} (z : Fin m → Bool) : State m := fun y => if y = z then 1 else 0 + +/-- The input word padded with zeros to `m` bits. -/ +def pad (m : ℕ) (x : List Bool) : Fin m → Bool := fun i => x.getD i false + +/-- The probability of reading `1` on qubit `0` after running the codes from `|x 0^{m - |x|}⟩`. -/ +noncomputable def acceptProb (m : ℕ) (gs : List GateCode) (x : List Bool) : ℝ := + ∑ y : Fin m → Bool, if bit y 0 then ‖run gs (basis (pad m x)) y‖ ^ 2 else 0 + +/-! ### Gates on amplitudes -/ + +variable {m : ℕ} + +theorem bit_of_lt (y : Fin m → Bool) {i : ℕ} (h : i < m) : bit y i = y ⟨i, h⟩ := by + simp [bit, h] + +theorem getD_ofFn (y : Fin m → Bool) (i : ℕ) : (List.ofFn y).getD i false = bit y i := by + unfold bit + split_ifs with h <;> simp [List.getD_eq_getElem?_getD, h] + +theorem setBit_eq_update (y : Fin m → Bool) {t : ℕ} (ht : t < m) (c : Bool) : + setBit y t c = Function.update y ⟨t, ht⟩ c := by + funext i + simp only [setBit, Function.update_apply, Fin.ext_iff] + +theorem ofLp_ket (z : Fin m → Bool) : (ket z).ofLp = basis z := by + funext y + rw [ket_apply] + rfl + +/-- A placed gate reads each amplitude through the column of its matrix. -/ +theorem ofLp_eval_apply (pg : PlacedGate m) (ψ : Qubits m) (y : Fin m → Bool) : + (pg.eval ψ).ofLp y = ∑ z, (pg.eval (ket z)).ofLp y * ψ.ofLp z := by + simp only [PlacedGate.eval_ket_apply] + simp [PlacedGate.eval, Matrix.mulVec, dotProduct] + +/-- The Hadamard formula is linear, with matrix entries its values on basis states. -/ +theorem hadamard_apply_eq_sum (t : ℕ) (ψ : State m) (y : Fin m → Bool) : + hadamard t ψ y = ∑ z, hadamard t (basis z) y * ψ z := by + simp only [hadamard, basis, mul_ite, mul_one, mul_zero, sum_mul, mul_sum, ite_mul, zero_mul] + rw [sum_comm] + simp only [sum_ite_eq, mem_univ, ite_true, mul_assoc, one_mul] + +/-- The Hadamard gate code agrees with the Hadamard formula on basis states. -/ +theorem hadamard_basis {t : ℕ} {pg : PlacedGate m} + (hg : GateCode.toPlacedGate? m (true, t, []) = some pg) (ht : t < m) (z y : Fin m → Bool) : + (pg.eval (ket z)).ofLp y = hadamard t (basis z) y := by + rw [GateCode.eval_toPlacedGate_hadamard_ket hg ht z] + simp only [hadamard, basis, bit_of_lt _ ht, setBit_eq_update _ ht, Fintype.sum_bool, + WithLp.ofLp_add, WithLp.ofLp_smul, Pi.add_apply, Pi.smul_apply, ket_apply, smul_eq_mul, + Function.update_eq_iff, Function.eq_update_iff] + by_cases hP : ∀ j ≠ (⟨t, ht⟩ : Fin m), y j = z j + · simp only [iff_true_intro hP, and_true] + cases y ⟨t, ht⟩ <;> cases z ⟨t, ht⟩ <;> simp + · simp [hP] + +/-- A flip of target `t`, not among the controls, is an involution. -/ +theorem flip_flip {t : ℕ} {cs : List ℕ} (ht : t < m) (hcs : t ∉ cs) (y : Fin m → Bool) : + flip t cs (flip t cs y) = y := by + have hbit (v : Bool) (c : ℕ) (hc : c ≠ t) : bit (Function.update y ⟨t, ht⟩ v) c = bit y c := by + unfold bit + split_ifs with h + · exact Function.update_of_ne (fun h' => hc (congrArg Fin.val h')) _ _ + · rfl + have hall (v : Bool) : cs.all (bit (Function.update y ⟨t, ht⟩ v)) = cs.all (bit y) := by + rw [Bool.eq_iff_iff, List.all_eq_true, List.all_eq_true] + exact forall₂_congr fun c hc => by rw [hbit v c fun h => hcs (h ▸ hc)] + simp only [flip, setBit_eq_update _ ht, bit_of_lt _ ht, Function.update_self, hall, + Function.update_idem, Bool.xor_assoc, Bool.xor_self, Bool.xor_false, Function.update_eq_self] + +/-- The classical gate code `(false, t, cs)` maps `|z⟩` to `|flip t cs z⟩`. -/ +theorem classical_basis {t : ℕ} {cs : List ℕ} {pg : PlacedGate m} + (hg : GateCode.toPlacedGate? m (false, t, cs) = some pg) (ht : t < m) (z y : Fin m → Bool) : + (pg.eval (ket z)).ofLp y = if y = flip t cs z then 1 else 0 := by + rw [GateCode.eval_toPlacedGate_ket hg ht z, ket_apply] + simp only [getD_ofFn, flip, setBit_eq_update _ ht, bit_of_lt _ ht] + +/-- **A well-formed gate code acts on amplitudes as its formula says.** -/ +theorem ofLp_eval_toPlacedGate {g : GateCode} {pg : PlacedGate m} + (hwf : GateCode.WellFormed m g) (hg : GateCode.toPlacedGate? m g = some pg) (ψ : Qubits m) : + (pg.eval ψ).ofLp = applyGate g ψ.ofLp := by + funext y + obtain ⟨_ | _, t, cs⟩ := g + · obtain ⟨-, hnd, hlt⟩ := hwf + have ht : t < m := hlt t (List.mem_cons_self ..) + have hcs : t ∉ cs := (List.nodup_cons.mp hnd).1 + have hrow (z : Fin m → Bool) : (pg.eval (ket z)).ofLp y = if z = flip t cs y then 1 else 0 := + (classical_basis hg ht z y).trans (if_congr ⟨fun h => by rw [h, flip_flip ht hcs], + fun h => by rw [h, flip_flip ht hcs]⟩ rfl rfl) + simp only [ofLp_eval_apply, hrow, ite_mul, one_mul, zero_mul, sum_ite_eq', mem_univ, + ite_true] + rfl + · obtain ⟨ht, rfl⟩ := hwf + rw [ofLp_eval_apply] + change _ = hadamard t ψ.ofLp y + rw [hadamard_apply_eq_sum] + exact sum_congr rfl fun z _ => by rw [hadamard_basis hg ht] + +/-- **A run of well-formed gate codes is the library's circuit.** -/ +theorem ofLp_eval_ofCodes {gs : List GateCode} (hwf : ∀ g ∈ gs, GateCode.WellFormed m g) + (ψ : Qubits m) : (Circuit.eval (Circuit.ofCodes m gs) ψ).ofLp = run gs ψ.ofLp := by + induction gs generalizing ψ with + | nil => simp [run] + | cons g gs ih => + obtain ⟨pg, hpg⟩ := Option.isSome_iff_exists.mp + (GateCode.isSome_toPlacedGate?_iff.mpr (hwf g (List.mem_cons_self ..))) + have hcodes : Circuit.ofCodes m (g :: gs) = pg :: Circuit.ofCodes m gs := by + simp [Circuit.ofCodes, hpg] + rw [hcodes, Circuit.eval_cons, ih (fun g' hg' => hwf g' (List.mem_cons_of_mem _ hg')), + ofLp_eval_toPlacedGate (hwf g (List.mem_cons_self ..)) hpg] + rfl + +/-- **The explicit acceptance probability is the library's**, for well-formed gate codes. -/ +theorem acceptProb_eq {gs : List GateCode} (hwf : ∀ g ∈ gs, GateCode.WellFormed m g) + (x : List Bool) : acceptProb m gs x = Cslib.Quantum.acceptProb m gs x := by + have hrun : (Circuit.run (Circuit.ofCodes m gs) (inputState m x)).ofLp = + run gs (basis (pad m x)) := by + rw [Circuit.run, ofLp_eval_ofCodes hwf, ofLp_ket] + rfl + rw [Cslib.Quantum.acceptProb, measureProb, accepting, sum_filter, hrun, acceptProb] + refine sum_congr rfl fun y _ => if_congr ?_ rfl rfl + unfold bit + split_ifs with h <;> simp [h] + +/-! ### The classes -/ + +/-- The encoding of gate codes `(h, t, cs)`: the flag bit, then the target and the controls in +unary. -/ +abbrev encGateCode : GateCode ↪ List Bool := + Encoding.encPair Encoding.encBool + (Encoding.encPair Encoding.encUnary (Encoding.encList Encoding.encUnary)) + +/-- Polynomial-time uniform families of well-formed gate codes. -/ +def Uniform (width : ℕ → ℕ) (gates : ℕ → List GateCode) : Prop := + Computation.PolyTime width Encoding.encUnary Encoding.encUnary ∧ + Computation.PolyTime gates Encoding.encUnary (Encoding.encList encGateCode) ∧ + ∀ n, n ≤ width n ∧ 0 < width n ∧ ∀ g ∈ gates n, GateCode.WellFormed (width n) g + +/-- Bounded-error quantum polynomial time, over the explicit model. -/ +def BQP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := + {A | ∃ (width : ℕ → ℕ) (gates : ℕ → List GateCode), Uniform width gates ∧ ∀ a, + (a ∈ A → 2 / 3 ≤ acceptProb (width (enc a).length) (gates (enc a).length) (enc a)) ∧ + (a ∉ A → acceptProb (width (enc a).length) (gates (enc a).length) (enc a) ≤ 1 / 3)} + +/-- Count the accepted binary strings of exactly `n` bits. -/ +def acceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card + +/-- Unbounded-error probabilistic polynomial time, by a strict majority of certificates. -/ +def PP {α : Type} (enc : α ↪ List Bool) : Set (Set α) := + {A | ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Computation.PolyTimeVerifier enc V ∧ + ∀ a, a ∈ A ↔ 2 ^ p.eval (enc a).length < 2 * acceptCount V a (p.eval (enc a).length)} + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} + +/-- **The explicit class is the library's `BQP`.** -/ +theorem mem_BQP_iff : A ∈ BQP enc ↔ A ∈ Cslib.Complexity.BQP enc := by + constructor + · rintro ⟨width, gates, ⟨hw, hg, hn⟩, hdec⟩ + let F : UniformCircuitFamily := + { width, gates + computableInPolyTime_width := hw + computableInPolyTime_gates := hg + le_width := fun n => (hn n).1 + width_pos := fun n => (hn n).2.1 + wellFormed := fun n => (hn n).2.2 } + refine ⟨F, fun a => ?_⟩ + rw [UniformCircuitFamily.acceptProb, ← acceptProb_eq ((hn _).2.2)] + exact hdec a + · rintro ⟨F, hF⟩ + refine ⟨F.width, F.gates, ⟨F.computableInPolyTime_width, F.computableInPolyTime_gates, + fun n => ⟨F.le_width n, F.width_pos n, F.wellFormed n⟩⟩, fun a => ?_⟩ + rw [acceptProb_eq (F.wellFormed _)] + exact hF a + +/-- The explicit `PP` is the library's, by unfolding. -/ +theorem PP_eq : PP enc = Cslib.Complexity.PP enc := rfl + +/-- **`BQP ⊆ PP`** over the explicit model, from `Cslib.Complexity.BQP_subset_PP`. -/ +theorem BQP_subset_PP (enc : α ↪ List Bool) : BQP enc ⊆ PP enc := fun _ hA => + Cslib.Complexity.BQP_subset_PP (mem_BQP_iff.mp hA) + +end ComplexityAbstracts.BQPBridge diff --git a/abstracts/README.md b/abstracts/README.md index b2e7015dd4..3492213b06 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -40,6 +40,7 @@ former paper/TeX index is retired; Git history retains its sources. | [Immerman–Szelepcsényi: nondeterministic space is closed under complement](ComplexityAbstracts/ImmermanSzelepcsenyiAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/immerman-szelepcsenyi.pdf) | One finite-state native machine per problem, every-prefix work space c₁ s(n) + c₂ for any s with log₂ n ≤ s(n), no constructibility assumed, every branch terminating, arbitrary injective encodings; directed non-reachability on unary-header adjacency matrices as a corollary. | | [Shamir: IP equals PSPACE](ComplexityAbstracts/ShamirAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/shamir.pdf) | All prover strategies are quantified explicitly, with a uniform native clock and specified completeness and soundness. | | [Toda: a counting oracle decides the polynomial hierarchy](ComplexityAbstracts/TodaAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/toda.pdf) | Witness counts and oracle bit answers are explicit; correctness holds for every extension of valid oracle answers. | +| [Adleman–DeMarrais–Huang: BQP is contained in PP](ComplexityAbstracts/BQPAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/bqp-pp.pdf) | Explicit amplitude semantics for the fixed gate set {Hadamard, NOT, CNOT, Toffoli}, acceptance by measuring qubit 0 from the zero-padded input, uniformity in polynomial time from n in unary, and native multi-tape PP; equivalence to textbook BQP over arbitrary elementary gates (universality and Solovay–Kitaev) is a cited, unformalized remark. | | [Barrington: five states capture NC¹](ComplexityAbstracts/BarringtonAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/barrington.pdf) | Nonuniform circuits and permutation programs; no uniform generator or compiler runtime is asserted. | | [Håstad and Razborov–Smolensky: parity resists shallow circuits](ComplexityAbstracts/ConstantDepthAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/constant-depth.pdf) | Explicit finite bounds, gate semantics and depth conventions; nonuniform lower bounds. | | [Formula lower bounds: parity and Andreev](ComplexityAbstracts/FormulaBoundsAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/formula-bounds.pdf) | De Morgan formulas, literal leaves, explicit block indexing and finite quantitative bounds; no general-circuit lower bound. | diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json index 3c3bf467be..fbe07ce288 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -109,6 +109,20 @@ "ComplexityAbstracts.Computation" ] }, + { + "id": "bqp-pp", + "title": "Adleman–DeMarrais–Huang: BQP is contained in PP", + "module": "ComplexityAbstracts.BQPAbstract", + "headline_theorems": [ + "ComplexityAbstracts.BQPAbstract.BQP_subset_PP" + ], + "summary": "Every problem decided with bounded error by a polynomial-time uniform family of quantum circuits is decided by a polynomial-time strict-majority vote over random strings.", + "scope": "Explicit amplitude semantics for the fixed gate set {Hadamard, NOT, CNOT, Toffoli}, acceptance by measuring qubit 0 from the zero-padded input, uniformity in polynomial time from n in unary, and native multi-tape PP; equivalence to textbook BQP over arbitrary elementary gates (universality and Solovay–Kitaev) is a cited, unformalized remark.", + "foundations": [ + "ComplexityAbstracts.Encoding", + "ComplexityAbstracts.Computation" + ] + }, { "id": "barrington", "title": "Barrington: five states capture NC¹", diff --git a/scripts/abstract_to_tex.py b/scripts/abstract_to_tex.py index eb38993838..cb77e66152 100644 --- a/scripts/abstract_to_tex.py +++ b/scripts/abstract_to_tex.py @@ -16,6 +16,7 @@ "ℤ": r"\mathbb{Z}", "ℚ": r"\mathbb{Q}", "ℝ": r"\mathbb{R}", + "ℂ": r"\mathbb{C}", "↪": r"\hookrightarrow", "→": r"\to", "↦": r"\mapsto", @@ -57,6 +58,8 @@ "⌊": r"\lfloor", "⌋": r"\rfloor", "·": r"\cdot", + "±": r"\pm", + "‖": r"\|", "ℓ": r"\ell", "Σ": r"\Sigma", "Δ": r"\Delta", diff --git a/scripts/test_abstract_to_tex.py b/scripts/test_abstract_to_tex.py index 8ec7df3a1a..d4dba7a0b5 100644 --- a/scripts/test_abstract_to_tex.py +++ b/scripts/test_abstract_to_tex.py @@ -329,6 +329,15 @@ def test_floor_delta_omega_eventually_and_cdots_are_pdflatex_safe(self): r"^{\mathsf{f}}", r"\cdots"): self.assertIn(command, rendered) + def test_complex_amplitudes_are_pdflatex_safe(self): + sample = "(Fin m → Bool) → ℂ, ‖ψ y‖ ^ 2, ±1" + for rendered in (abstract_to_tex.escape_tex_code_line(sample), + abstract_to_tex.escape_tex_prose(sample)): + with self.subTest(rendered=rendered): + self.assertTrue(rendered.isascii()) + for command in (r"\mathbb{C}", r"\|", r"\pm"): + self.assertIn(command, rendered) + def test_named_axiom_audits_are_stripped(self): sample = ( "/-! # Title\n\nIntro.\n-/\n\nnamespace Foo\n\n" From 0ecdb90af5977bf0019e7abb456c667c936be408 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 19:51:55 -0400 Subject: [PATCH 4/5] =?UTF-8?q?doc(readme):=20list=20the=20BQP=20=E2=8A=86?= =?UTF-8?q?=20PP=20abstract=20among=20the=20selected=20results?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The README hygiene check (#1958) requires every catalogue entry in the root README. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 83dcc46615..d3db31ac41 100644 --- a/README.md +++ b/README.md @@ -65,6 +65,7 @@ the selection is not an exhaustive API reference. * [Immerman–Szelepcsényi: nondeterministic space is closed under complement](abstracts/ComplexityAbstracts/ImmermanSzelepcsenyiAbstract.lean): Nondeterministic space at least logarithmic is closed under complement; in particular NL equals coNL. * [Shamir: IP equals PSPACE](abstracts/ComplexityAbstracts/ShamirAbstract.lean): Interaction and randomness give a polynomial-time verifier the power of polynomial space. * [Toda: a counting oracle decides the polynomial hierarchy](abstracts/ComplexityAbstracts/TodaAbstract.lean): Every problem in the polynomial hierarchy is decidable in polynomial time with an exact counting oracle. +* [Adleman–DeMarrais–Huang: BQP is contained in PP](abstracts/ComplexityAbstracts/BQPAbstract.lean): Every problem decided with bounded error by a polynomial-time uniform family of quantum circuits is decided by a polynomial-time strict-majority vote over random strings. * [Barrington: five states capture NC¹](abstracts/ComplexityAbstracts/BarringtonAbstract.lean): Polynomial-length permutation programs on five states capture logarithmic-depth polynomial-size Boolean circuits. * [Håstad and Razborov–Smolensky: parity resists shallow circuits](abstracts/ComplexityAbstracts/ConstantDepthAbstract.lean): At fixed depth, parity requires more than polynomially many gates, including over an odd-prime modular basis. * [Braverman: polylogarithmic independence fools AC⁰](abstracts/ComplexityAbstracts/BravermanAbstract.lean): k-wise independence with k = (log(m/ε))^O(d²) fools every depth-d circuit of NOT and unbounded fan-in AND/OR gates with size and fan-in at most m, to within error ε. From 7139252b7c6dd93b7337d1eef71b117a9be5462a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 20:01:03 -0400 Subject: [PATCH 5/5] fix(abstracts): unfold onesAt in the BQP bridge after #2099 #2099 defines `accepting` as `onesAt m [0]`; the bridge's rewrite chain unfolds it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- abstracts/ComplexityAbstracts/BQPBridge.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/abstracts/ComplexityAbstracts/BQPBridge.lean b/abstracts/ComplexityAbstracts/BQPBridge.lean index cc20937bb0..a56272727b 100644 --- a/abstracts/ComplexityAbstracts/BQPBridge.lean +++ b/abstracts/ComplexityAbstracts/BQPBridge.lean @@ -185,7 +185,7 @@ theorem acceptProb_eq {gs : List GateCode} (hwf : ∀ g ∈ gs, GateCode.WellFor run gs (basis (pad m x)) := by rw [Circuit.run, ofLp_eval_ofCodes hwf, ofLp_ket] rfl - rw [Cslib.Quantum.acceptProb, measureProb, accepting, sum_filter, hrun, acceptProb] + rw [Cslib.Quantum.acceptProb, measureProb, accepting, onesAt, sum_filter, hrun, acceptProb] refine sum_congr rfl fun y _ => if_congr ?_ rfl rfl unfold bit split_ifs with h <;> simp [h]