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/4] feat(Classes/BQP): define BQP over Hadamard and Toffoli circuits (#896 M2) Define BQP by polynomial-time uniform families of quantum circuits over the Hadamard, NOT, CNOT and Toffoli gates, accepting by measuring qubit 0, with bounded error 2/3 vs 1/3 (Samuel's 2026-10-30 decision on #896). Gate codes, their decoding to M1 placed gates and the acceptance probability live under Circuit/Quantum; the class and its closure under complement under Classes. Tests cover exact deciders, interference and a family that decides nothing. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../Computability/Circuit/Quantum/Code.lean | 323 ++++++++++++++++++ .../Circuit/Quantum/Uniform.lean | 116 +++++++ .../Computability/Complexity/Classes/BQP.lean | 91 +++++ .../Foundations/Quantum/Measurement.lean | 6 + ComplexityTests/BQP.lean | 169 +++++++++ references.bib | 30 ++ 7 files changed, 738 insertions(+) create mode 100644 Complexity/Computability/Circuit/Quantum/Code.lean create mode 100644 Complexity/Computability/Circuit/Quantum/Uniform.lean create mode 100644 Complexity/Computability/Complexity/Classes/BQP.lean create mode 100644 ComplexityTests/BQP.lean diff --git a/Complexity.lean b/Complexity.lean index e6f116c6e..7accc0251 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -937,6 +937,8 @@ public import Complexity.Computability.Circuit.Pi public import Complexity.Computability.Circuit.Pointwise public import Complexity.Computability.Circuit.Program public import Complexity.Computability.Circuit.Quantum.Basic +public import Complexity.Computability.Circuit.Quantum.Code +public import Complexity.Computability.Circuit.Quantum.Uniform public import Complexity.Computability.Circuit.Rational public import Complexity.Computability.Circuit.Rational.Affine public import Complexity.Computability.Circuit.Rational.BlockDivision @@ -1042,6 +1044,7 @@ public import Complexity.Computability.Complexity.Classes.BPP.KarpLipton public import Complexity.Computability.Complexity.Classes.BPP.Reduction public import Complexity.Computability.Complexity.Classes.BPP.WorstCaseHardness public import Complexity.Computability.Complexity.Classes.BPPpath +public import Complexity.Computability.Complexity.Classes.BQP public import Complexity.Computability.Complexity.Classes.BooleanHierarchy public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Closure public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Kadin diff --git a/Complexity/Computability/Circuit/Quantum/Code.lean b/Complexity/Computability/Circuit/Quantum/Code.lean new file mode 100644 index 000000000..0ee18bbd6 --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/Code.lean @@ -0,0 +1,323 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Quantum.Basic + +/-! +# Quantum circuits over Hadamard and Toffoli gates, written as data + +This file fixes the gate set of the class `BQP` (`Cslib.Complexity.BQP`): the Hadamard gate and the +classical reversible gates NOT, CNOT and Toffoli of +`Complexity/Computability/Circuit/Quantum/Basic.lean`. Their matrix entries lie in +`{0, ±1, ±1/√2}`. + +A gate is written as a triple `(h, t, cs) : Bool × ℕ × List ℕ` (`Cslib.Quantum.GateCode`): +`(true, t, [])` is the Hadamard gate on qubit `t`, and `(false, t, cs)` with at most two control +qubits `cs` flips qubit `t` when every qubit of `cs` is one, that is NOT, CNOT or Toffoli. A code +is *well formed* on `m` qubits when its qubits are distinct and below `m` +(`Cslib.Quantum.GateCode.WellFormed`); it then denotes a placed gate +(`Cslib.Quantum.GateCode.toPlacedGate?`), and a list of codes denotes a circuit +(`Cslib.Quantum.Circuit.ofCodes`). Codes are what a polynomial-time machine outputs in the +definition of uniform circuit families. + +A run starts in the basis state `|x 0^{m - n}⟩` holding the input word `x` of length `n` on the +first qubits (`Cslib.Quantum.inputState`), and accepts when the final measurement finds qubit `0` +in state `1` (`Cslib.Quantum.accepting`, `Cslib.Quantum.acceptProb`), as in +[Arora, Barak][AroraBarak09], Chapter 10. + +Classical reversible gates permute basis states, updating the bit of their target +(`Cslib.Quantum.GateCode.eval_toPlacedGate_ket`). Appending a NOT gate on qubit `0` exchanges +acceptance and rejection (`Cslib.Quantum.acceptProb_append_not`). + +## Main definitions + +* `Cslib.Quantum.GateCode`, `Cslib.Quantum.GateCode.WellFormed`, + `Cslib.Quantum.GateCode.toPlacedGate?`: gate codes and the gates they denote. +* `Cslib.Quantum.Circuit.ofCodes`: the circuit denoted by a list of gate codes. +* `Cslib.Quantum.inputState`, `Cslib.Quantum.accepting`, `Cslib.Quantum.acceptProb`: the input + basis state, the accepting outcomes and the acceptance probability. + +## Main results + +* `Cslib.Quantum.splitEquiv_symm_update`: placing a classical gate that changes one bit. +* `Cslib.Quantum.GateCode.eval_toPlacedGate_ket`: a classical gate code updates its target bit. +* `Cslib.Quantum.acceptProb_nonneg`, `Cslib.Quantum.acceptProb_le_one`. +* `Cslib.Quantum.acceptProb_append_not`: a final NOT on qubit `0` complements the acceptance + probability. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Finset + +variable {m k : ℕ} + +/-- Placing a bit string that differs from `x ∘ A` only at position `i` changes `x` only at the +qubit `A i`. -/ +theorem splitEquiv_symm_update (A : Fin k ↪ Fin m) (x : Fin m → Bool) (i : Fin k) (b : Bool) : + (splitEquiv A).symm (Function.update (x ∘ A) i b, (splitEquiv A x).2) = + Function.update x (A i) b := by + funext j + by_cases hj : ∃ i', A i' = j + · obtain ⟨i', rfl⟩ := hj + rw [splitEquiv_symm_apply_wire] + simp only [Function.update_apply, A.injective.eq_iff, Function.comp_apply] + · rw [splitEquiv_symm_apply_of_not _ _ _ _ hj, splitEquiv_apply_snd, + Function.update_of_ne fun h => hj ⟨i, h.symm⟩] + +/-- A classical reversible gate that changes only its bit `i`, to `f z` on input `z`, maps `|x⟩` to +the basis state that changes only the qubit `A i`, to `f (x ∘ A)`. -/ +theorem PlacedGate.eval_ofPerm_ket_of_update (σ : Equiv.Perm (Fin k → Bool)) (A : Fin k ↪ Fin m) + (i : Fin k) (f : (Fin k → Bool) → Bool) (hσ : ∀ z, σ z = Function.update z i (f z)) + (x : Fin m → Bool) : + (PlacedGate.mk k (Gate.ofPerm σ) A).eval (ket x) = + ket (Function.update x (A i) (f (x ∘ A))) := by + rw [eval_ofPerm_ket, hσ, splitEquiv_symm_update] + +/-! ### Gate codes -/ + +/-- A **gate code** `(h, t, cs)`: `(true, t, [])` is the Hadamard gate on qubit `t`, and +`(false, t, cs)` with at most two controls `cs` flips qubit `t` when every qubit in `cs` is one +(the NOT, CNOT and Toffoli gates). -/ +abbrev GateCode := Bool × ℕ × List ℕ + +namespace GateCode + +/-- The placed gate denoted by a gate code on `m` qubits, or `none` when the code is not well +formed: its qubits must be distinct and below `m`. -/ +noncomputable def toPlacedGate? (m : ℕ) : GateCode → Option (PlacedGate m) + | (true, t, []) => + if h : t < m then some ⟨1, Gate.hadamard, ⟨![⟨t, h⟩], fun i j _ => Subsingleton.elim i j⟩⟩ + else none + | (false, t, []) => + if h : t < m then some ⟨1, Gate.not, ⟨![⟨t, h⟩], fun i j _ => Subsingleton.elim i j⟩⟩ + else none + | (false, t, [c]) => + if h : c < m ∧ t < m ∧ c ≠ t then + some ⟨2, Gate.cnot, ⟨![⟨c, h.1⟩, ⟨t, h.2.1⟩], by + intro i j hij + fin_cases i <;> fin_cases j <;> first | rfl | (simp [Fin.ext_iff] at hij; omega)⟩⟩ + else none + | (false, t, [c₁, c₂]) => + if h : c₁ < m ∧ c₂ < m ∧ t < m ∧ c₁ ≠ c₂ ∧ c₁ ≠ t ∧ c₂ ≠ t then + some ⟨3, Gate.toffoli, ⟨![⟨c₁, h.1⟩, ⟨c₂, h.2.1⟩, ⟨t, h.2.2.1⟩], by + intro i j hij + fin_cases i <;> fin_cases j <;> first | rfl | (simp [Fin.ext_iff] at hij; omega)⟩⟩ + else none + | _ => none + +/-- A gate code is **well formed** on `m` qubits: a Hadamard gate without controls, or a classical +gate with at most two controls, on distinct qubits below `m`. -/ +def WellFormed (m : ℕ) : GateCode → Prop + | (true, t, cs) => t < m ∧ cs = [] + | (false, t, cs) => cs.length ≤ 2 ∧ (t :: cs).Nodup ∧ ∀ i ∈ t :: cs, i < m + +instance (m : ℕ) : DecidablePred (WellFormed m) + | (true, _, _) => inferInstanceAs (Decidable (_ ∧ _)) + | (false, _, _) => inferInstanceAs (Decidable (_ ∧ _)) + +/-- **Exactly the well-formed codes denote gates.** -/ +theorem isSome_toPlacedGate?_iff {g : GateCode} : + (toPlacedGate? m g).isSome ↔ WellFormed m g := by + match g with + | (true, t, []) => simp [WellFormed, toPlacedGate?] + | (true, t, _ :: _) => simp [WellFormed, toPlacedGate?] + | (false, t, []) => simp [WellFormed, toPlacedGate?] + | (false, t, [c]) => + simp only [WellFormed, toPlacedGate?] + split_ifs with h <;> simp only [Option.isSome_some, Option.isSome_none] <;> + simp only [List.length_singleton, List.nodup_cons, List.not_mem_nil, not_false_eq_true, + List.nodup_nil, and_true, List.mem_cons, forall_eq_or_imp, true_iff, false_iff, + Bool.false_eq_true] <;> grind + | (false, t, [c₁, c₂]) => + simp only [WellFormed, toPlacedGate?] + split_ifs with h <;> simp only [Option.isSome_some, Option.isSome_none] <;> + simp only [List.length_cons, List.length_nil, List.nodup_cons, List.mem_cons, + List.not_mem_nil, List.nodup_nil, forall_eq_or_imp, true_iff, false_iff, + Bool.false_eq_true] <;> grind + | (false, t, _ :: _ :: _ :: _) => simp [WellFormed, toPlacedGate?] + +/-- **A classical gate code updates its target bit**: the well-formed code `(false, t, cs)` maps +`|x⟩` to the basis state that changes only qubit `t`, flipping it when every control is one. -/ +theorem eval_toPlacedGate_ket {t : ℕ} {cs : List ℕ} {g : PlacedGate m} + (hg : toPlacedGate? m (false, t, cs) = some g) (ht : t < m) (x : Fin m → Bool) : + g.eval (ket x) = ket (Function.update x ⟨t, ht⟩ + (x ⟨t, ht⟩ ^^ cs.all fun c => (List.ofFn x).getD c false)) := by + have hread (i : Fin m) : (List.ofFn x).getD i false = x i := by + simp [List.getD_eq_getElem?_getD] + match cs, hg with + | [], hg => + simp only [toPlacedGate?, ht, ↓reduceDIte, Option.some.injEq] at hg + subst hg + refine (PlacedGate.eval_ofPerm_ket_of_update _ _ 0 (fun z => !z 0) (fun z => ?_) x).trans ?_ + · funext i + rw [Subsingleton.elim i 0, Function.update_self] + rfl + · simp only [List.all_nil, Bool.xor_true] + rfl + | [c], hg => + simp only [toPlacedGate?] at hg + split_ifs at hg with h + simp only [Option.some.injEq] at hg + subst hg + refine (PlacedGate.eval_ofPerm_ket_of_update _ _ 1 (fun z => z 1 ^^ z 0) (fun _ => rfl) + x).trans ?_ + rw [List.all_cons, List.all_nil, Bool.and_true, + show (List.ofFn x).getD c false = x ⟨c, h.1⟩ from hread ⟨c, h.1⟩] + rfl + | [c₁, c₂], hg => + simp only [toPlacedGate?] at hg + split_ifs at hg with h + simp only [Option.some.injEq] at hg + subst hg + refine (PlacedGate.eval_ofPerm_ket_of_update _ _ 2 (fun z => z 2 ^^ (z 0 && z 1)) + (fun _ => rfl) x).trans ?_ + rw [List.all_cons, List.all_cons, List.all_nil, Bool.and_true, + show (List.ofFn x).getD c₁ false = x ⟨c₁, h.1⟩ from hread ⟨c₁, h.1⟩, + show (List.ofFn x).getD c₂ false = x ⟨c₂, h.2.1⟩ from hread ⟨c₂, h.2.1⟩] + rfl + | _ :: _ :: _ :: _, hg => simp [toPlacedGate?] at hg + +/-- **The Hadamard gate code branches on its target**: the well-formed code `(true, t, [])` maps +`|x⟩` to `∑_c (-1)^{x_t c} / √2 · |x[t ↦ c]⟩`. -/ +theorem eval_toPlacedGate_hadamard_ket {t : ℕ} {g : PlacedGate m} + (hg : toPlacedGate? m (true, t, []) = some g) (ht : t < m) (x : Fin m → Bool) : + g.eval (ket x) = ∑ c : Bool, ((if x ⟨t, ht⟩ && c then -1 else 1) * + (((Real.sqrt 2)⁻¹ : ℝ) : ℂ)) • ket (Function.update x ⟨t, ht⟩ c) := by + simp only [toPlacedGate?, ht, ↓reduceDIte, Option.some.injEq] at hg + subst hg + have hupd (y : Fin m → Bool) (c : Bool) : y = Function.update x ⟨t, ht⟩ c ↔ + y ⟨t, ht⟩ = c ∧ ∀ j ≠ ⟨t, ht⟩, y j = x j := by + constructor + · rintro rfl + exact ⟨Function.update_self .., fun j hj => Function.update_of_ne hj ..⟩ + · rintro ⟨h₁, h₂⟩ + funext j + by_cases hj : j = ⟨t, ht⟩ + · rw [hj, h₁, Function.update_self] + · rw [h₂ j hj, Function.update_of_ne hj] + ext y + rw [PlacedGate.eval_ket_apply, PlacedGate.matrix_apply, Fintype.sum_bool] + simp only [WithLp.ofLp_add, WithLp.ofLp_smul, Pi.add_apply, Pi.smul_apply, ket_apply, + smul_eq_mul, mul_ite, mul_one, mul_zero, hupd] + have hcond : (∀ j, (¬∃ i, (⟨![⟨t, ht⟩], fun i j _ => Subsingleton.elim i j⟩ : Fin 1 ↪ Fin m) i = + j) → y j = x j) ↔ ∀ j ≠ ⟨t, ht⟩, y j = x j := by + refine forall_congr' fun j => ⟨fun h hj => h ?_, fun h hj => h ?_⟩ + · rintro ⟨i, rfl⟩ + exact hj (by rw [Subsingleton.elim i 0]; rfl) + · rintro rfl + exact hj ⟨0, rfl⟩ + by_cases hagree : ∀ j ≠ ⟨t, ht⟩, y j = x j + · rw [ite_eq_left_of_eq_true _ _ (eq_true (hcond.mpr hagree)), Gate.hadamard_apply] + have hw (i : Fin 1) : + (⟨![⟨t, ht⟩], fun i j _ => Subsingleton.elim i j⟩ : Fin 1 ↪ Fin m) i = ⟨t, ht⟩ := by + rw [Subsingleton.elim i 0] + rfl + simp only [iff_true_intro hagree, and_true, Function.comp_apply, hw] + cases y ⟨t, ht⟩ <;> cases x ⟨t, ht⟩ <;> simp + · rw [ite_eq_right_of_eq_false _ _ (eq_false (mt hcond.mp hagree))] + simp only [iff_false_intro hagree, and_false, ite_false, add_zero] + +end GateCode + +/-- The circuit on `m` qubits denoted by a list of gate codes, applied first to last. Codes that are +not well formed are skipped. -/ +noncomputable def Circuit.ofCodes (m : ℕ) (gs : List GateCode) : Circuit m := + gs.filterMap (GateCode.toPlacedGate? m) + +@[simp] theorem Circuit.ofCodes_nil : Circuit.ofCodes m [] = [] := rfl + +theorem Circuit.ofCodes_append (gs hs : List GateCode) : + Circuit.ofCodes m (gs ++ hs) = Circuit.ofCodes m gs ++ Circuit.ofCodes m hs := + List.filterMap_append + +/-! ### Input, acceptance and acceptance probability -/ + +/-- The basis state `|x 0^{m - n}⟩` of an `m`-qubit register holding the input word `x` on its +first qubits (truncated when `x` is longer than `m`). -/ +def inputState (m : ℕ) (x : List Bool) : Fin m → Bool := fun i => x.getD i false + +/-- The accepting outcomes: qubit `0` reads `1`. -/ +def accepting (m : ℕ) : Finset (Fin m → Bool) := + univ.filter fun y => ∃ h : 0 < m, y ⟨0, h⟩ = true + +/-- The **acceptance probability** of the circuit with gate codes `gs` on `m` qubits on input `x`: +started in `|x 0^{m - n}⟩`, the final measurement finds qubit `0` in state `1`. -/ +noncomputable def acceptProb (m : ℕ) (gs : List GateCode) (x : List Bool) : ℝ := + measureProb (Circuit.run (Circuit.ofCodes m gs) (inputState m x)) (accepting m) + +theorem acceptProb_nonneg (m : ℕ) (gs : List GateCode) (x : List Bool) : + 0 ≤ acceptProb m gs x := + measureProb_nonneg _ _ + +theorem acceptProb_le_one (m : ℕ) (gs : List GateCode) (x : List Bool) : + acceptProb m gs x ≤ 1 := by + have h := measureProb_le_measureProb_univ + (Circuit.run (Circuit.ofCodes m gs) (inputState m x)) (accepting m) + rwa [measureProb_univ, Circuit.norm_run, one_pow] at h + +theorem mem_accepting (hm : 0 < m) {y : Fin m → Bool} : + y ∈ accepting m ↔ y ⟨0, hm⟩ = true := by + simp [accepting, hm] + +/-- The probability of the rejecting outcomes is one minus the acceptance probability. -/ +private theorem measureProb_compl_accepting (ψ : Qubits m) (hψ : ‖ψ‖ = 1) : + measureProb ψ (accepting m)ᶜ = 1 - measureProb ψ (accepting m) := by + have h := measureProb_univ ψ + rw [hψ, one_pow, ← union_compl (accepting m), measureProb, + sum_union disjoint_compl_right] at h + rw [measureProb, measureProb] + linarith + +/-- **A final NOT on qubit `0` exchanges acceptance and rejection.** -/ +theorem acceptProb_append_not (hm : 0 < m) (gs : List GateCode) (x : List Bool) : + acceptProb m (gs ++ [(false, 0, [])]) x = 1 - acceptProb m gs x := by + obtain ⟨g, hg⟩ : ∃ g, GateCode.toPlacedGate? m (false, 0, []) = some g := + Option.isSome_iff_exists.mp (GateCode.isSome_toPlacedGate?_iff.mpr + (by simp [GateCode.WellFormed, hm])) + set ψ := Circuit.run (Circuit.ofCodes m gs) (inputState m x) + let flip : (Fin m → Bool) → Fin m → Bool := fun y => Function.update y ⟨0, hm⟩ (!y ⟨0, hm⟩) + have hflip : Function.Involutive flip := by + intro y + funext j + by_cases hj : j = ⟨0, hm⟩ <;> simp [flip, hj] + have hket (z : Fin m → Bool) : g.eval (ket z) = ket (flip z) := by + rw [GateCode.eval_toPlacedGate_ket hg hm z] + simp only [List.all_nil, Bool.xor_true] + rfl + -- the NOT gate reads the amplitude of the flipped outcome + have happly (y : Fin m → Bool) : (g.eval ψ).ofLp y = ψ.ofLp (flip y) := by + have hrow (z : Fin m → Bool) : + (g.matrix : Matrix _ _ ℂ) y z = if z = flip y then 1 else 0 := by + rw [← PlacedGate.eval_ket_apply, hket, ket_apply] + refine if_congr ⟨fun h => ?_, fun h => ?_⟩ rfl rfl + · rw [h, hflip] + · rw [h, hflip] + simp only [PlacedGate.eval, unitaryEquiv_apply, Matrix.mulVec, dotProduct, hrow, ite_mul, + one_mul, zero_mul, sum_ite_eq', mem_univ, ite_true] + have hrun : Circuit.run (Circuit.ofCodes m (gs ++ [(false, 0, [])])) (inputState m x) = + g.eval ψ := by + simp only [Circuit.run, Circuit.ofCodes_append, Circuit.eval_append, ψ] + simp [Circuit.ofCodes, hg] + rw [acceptProb, hrun, acceptProb, ← measureProb_compl_accepting ψ (Circuit.norm_run _ _)] + simp only [measureProb, happly] + refine sum_nbij' flip flip (fun y hy => ?_) (fun y hy => ?_) (fun y _ => hflip y) + (fun y _ => hflip y) (fun y _ => rfl) + · rw [mem_accepting hm] at hy + simp [mem_accepting hm, flip, hy] + · rw [mem_compl, mem_accepting hm] at hy + simpa [mem_accepting hm, flip] using hy + +end Cslib.Quantum diff --git a/Complexity/Computability/Circuit/Quantum/Uniform.lean b/Complexity/Computability/Circuit/Quantum/Uniform.lean new file mode 100644 index 000000000..b612a5435 --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/Uniform.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Quantum.Code +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List + +/-! +# Polynomial-time uniform families of quantum circuits + +A uniform family of quantum circuits (`Cslib.Quantum.UniformCircuitFamily`) gives, for inputs of +length `n`, an `m`-qubit register with `m = width n ≥ n` and the gate codes `gates n` of a circuit +over the Hadamard, NOT, CNOT and Toffoli gates +(`Complexity/Computability/Circuit/Quantum/Code.lean`). +Both are computed from `n`, written in unary, by a polynomial-time machine. This follows the +library's convention for uniform Boolean circuits +(`Cslib.Complexity.CircuitValue.exists_uniformCircuits`) and [Arora, Barak][AroraBarak09], +Chapter 10: a polynomial-time machine that, given `n` in unary, outputs the descriptions of the +gates. Wires and the register width are written in unary, so they are +polynomially bounded. On an input word `x` the family runs its circuit for `n = |x|` from +`|x 0^{m - n}⟩` and accepts when the final measurement finds qubit `0` in state `1` +(`Cslib.Quantum.UniformCircuitFamily.acceptProb`). + +Appending a NOT gate on qubit `0` gives a family with complementary acceptance probability +(`Cslib.Quantum.UniformCircuitFamily.appendNot`). + +## Main definitions + +* `Cslib.Quantum.encGateCode`: the encoding of gate codes. +* `Cslib.Quantum.UniformCircuitFamily`: polynomial-time uniform families of circuits. +* `Cslib.Quantum.UniformCircuitFamily.acceptProb`: the acceptance probability on an input word. +* `Cslib.Quantum.UniformCircuitFamily.appendNot`: the family with a final NOT on qubit `0`. + +## Main results + +* `Cslib.Quantum.UniformCircuitFamily.acceptProb_appendNot`: the acceptance probability of + `appendNot` is one minus that of the family. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Turing.MultiTapeTM + +/-- The encoding of gate codes `(h, t, cs)`: the Hadamard flag, then the target and the list of +controls in unary. -/ +abbrev encGateCode : GateCode ↪ List Bool := encPair encBool (encPair encUnary (encList encUnary)) + +/-- A **polynomial-time uniform family of quantum circuits** over the Hadamard, NOT, CNOT and +Toffoli gates. On inputs of length `n` it uses a register of `width n` qubits, at least `n` and at +least one, and the well-formed gate codes `gates n`. The width and the gate codes are computed from +`n` in unary in polynomial time. -/ +structure UniformCircuitFamily where + /-- The number of qubits used on inputs of length `n`. -/ + width : ℕ → ℕ + /-- The gate codes of the circuit used on inputs of length `n`, applied first to last. -/ + gates : ℕ → List GateCode + computableInPolyTime_width : ComputableInPolyTime width encUnary encUnary + computableInPolyTime_gates : ComputableInPolyTime gates encUnary (encList encGateCode) + le_width : ∀ n, n ≤ width n + width_pos : ∀ n, 0 < width n + wellFormed : ∀ n, ∀ g ∈ gates n, g.WellFormed (width n) + +namespace UniformCircuitFamily + +/-- The **acceptance probability** of the family on the input word `x`: its circuit for inputs of +length `|x|`, started in `|x 0^{m - |x|}⟩`, ends with qubit `0` measured in state `1`. -/ +noncomputable def acceptProb (F : UniformCircuitFamily) (x : List Bool) : ℝ := + Quantum.acceptProb (F.width x.length) (F.gates x.length) x + +theorem acceptProb_nonneg (F : UniformCircuitFamily) (x : List Bool) : 0 ≤ F.acceptProb x := + Quantum.acceptProb_nonneg _ _ _ + +theorem acceptProb_le_one (F : UniformCircuitFamily) (x : List Bool) : F.acceptProb x ≤ 1 := + Quantum.acceptProb_le_one _ _ _ + +/-- The family with a final NOT gate on qubit `0`. -/ +def appendNot (F : UniformCircuitFamily) : UniformCircuitFamily where + width := F.width + gates n := F.gates n ++ [(false, 0, [])] + computableInPolyTime_width := F.computableInPolyTime_width + computableInPolyTime_gates := by + have := F.computableInPolyTime_gates + fun_prop + le_width := F.le_width + width_pos := F.width_pos + wellFormed n g hg := by + rcases List.mem_append.mp hg with hg | hg + · exact F.wellFormed n g hg + · rw [List.mem_singleton.mp hg] + simp [GateCode.WellFormed, F.width_pos n] + +/-- **A final NOT on qubit `0` complements the acceptance probability.** -/ +@[simp] theorem acceptProb_appendNot (F : UniformCircuitFamily) (x : List Bool) : + F.appendNot.acceptProb x = 1 - F.acceptProb x := + acceptProb_append_not (F.width_pos _) _ _ + +end UniformCircuitFamily + +end Cslib.Quantum diff --git a/Complexity/Computability/Complexity/Classes/BQP.lean b/Complexity/Computability/Complexity/Classes/BQP.lean new file mode 100644 index 000000000..3ef377f94 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/BQP.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Quantum.Uniform + +/-! +# The class BQP + +`BQP` is the class of problems decided with bounded error by polynomial-time uniform families of +quantum circuits [Bernstein, Vazirani][BernsteinVazirani1997], in the circuit formulation of +[Arora, Barak][AroraBarak09], Chapter 10: `A ∈ BQP enc` when a family +`F : Cslib.Quantum.UniformCircuitFamily` accepts the encoding of every member of `A` with +probability at least `2 / 3`, and the encoding of every other instance with probability at most +`1 / 3`. + +## Gate set + +The circuits use the Hadamard gate and the classical reversible gates NOT, CNOT and Toffoli +(`Cslib.Quantum.GateCode`), a fixed finite gate set whose matrix entries lie in +`{0, ±1, ±1/√2}`. Arora and Barak instead allow any elementary operation, a unitary acting on at +most three qubits, whose description a polynomial-time machine outputs. The two definitions give +the same class. Toffoli and Hadamard gates are universal for quantum computation +[Shi][Shi2003], [Aharonov][Aharonov2003]; with the Solovay–Kitaev approximation theorem, circuits +over them simulate circuits over arbitrary elementary operations with polynomial overhead and small +error. This equivalence is cited, not formalized here. A fixed finite gate set matters: +Adleman, DeMarrais and Huang show that arbitrary complex amplitudes would put uncountably many +languages into `BQP` [Adleman, DeMarrais, Huang][AdlemanDeMarraisHuang1997]. + +Acceptance is the measurement of qubit `0`, after a single measurement of the whole register in the +computational basis at the end; Arora and Barak note that intermediate measurements and mixed +states add no power. + +## Main definitions + +* `Cslib.Complexity.BQP`. + +## Main results + +* `Cslib.Complexity.compl_mem_BQP`: `BQP` is closed under complement. + +## References + +* [E. Bernstein, U. Vazirani, *Quantum complexity theory*][BernsteinVazirani1997] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +* [Y. Shi, *Both Toffoli and Controlled-NOT need little help to do universal quantum + computation*][Shi2003] +* [D. Aharonov, *A simple proof that Toffoli and Hadamard are quantum universal*][Aharonov2003] +* [L. Adleman, J. DeMarrais, M.-D. Huang, *Quantum computability*][AdlemanDeMarraisHuang1997] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Quantum + +variable {α : Type} + +/-- The problems decided with bounded error by polynomial-time uniform families of quantum +circuits over the Hadamard, NOT, CNOT and Toffoli gates, with respect to the encoding `enc` of +instances: members are accepted with probability at least `2 / 3`, and other instances with +probability at most `1 / 3`. -/ +def BQP (enc : α ↪ List Bool) : Set (Set α) := + {A | ∃ F : UniformCircuitFamily, ∀ a, + (a ∈ A → 2 / 3 ≤ F.acceptProb (enc a)) ∧ (a ∉ A → F.acceptProb (enc a) ≤ 1 / 3)} + +variable {enc : α ↪ List Bool} {A : Set α} + +theorem mem_BQP : A ∈ BQP enc ↔ ∃ F : UniformCircuitFamily, ∀ a, + (a ∈ A → 2 / 3 ≤ F.acceptProb (enc a)) ∧ (a ∉ A → F.acceptProb (enc a) ≤ 1 / 3) := + Iff.rfl + +/-- **`BQP` is closed under complement**: a final NOT gate on qubit `0` exchanges acceptance and +rejection. -/ +theorem compl_mem_BQP (hA : A ∈ BQP enc) : Aᶜ ∈ BQP enc := by + obtain ⟨F, hF⟩ := hA + refine ⟨F.appendNot, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ + · have := (hF a).2 ha + rw [UniformCircuitFamily.acceptProb_appendNot] + linarith + · have := (hF a).1 (Set.notMem_compl_iff.mp ha) + rw [UniformCircuitFamily.acceptProb_appendNot] + linarith + +end Cslib.Complexity diff --git a/Complexity/Foundations/Quantum/Measurement.lean b/Complexity/Foundations/Quantum/Measurement.lean index 63b40ca6c..b13c06033 100644 --- a/Complexity/Foundations/Quantum/Measurement.lean +++ b/Complexity/Foundations/Quantum/Measurement.lean @@ -34,6 +34,7 @@ query index (`Complexity/Computability/QueryComplexity/Quantum/Search.lean`). ## Main results * `Cslib.Quantum.measureProb_univ`: the outcome probabilities sum to `‖ψ‖²`. +* `Cslib.Quantum.measureProb_ket`: a basis state is measured with certainty. * `Cslib.Quantum.measure_toOuterMeasure_apply`: the measurement probabilities are `measureProb`. ## References @@ -70,6 +71,11 @@ theorem measureProb_nonneg (ψ : EuclideanSpace ℂ ι) (S : Finset ι) : 0 ≤ theorem measureProb_univ [Fintype ι] (ψ : EuclideanSpace ℂ ι) : measureProb ψ univ = ‖ψ‖ ^ 2 := (EuclideanSpace.norm_sq_eq ψ).symm +/-- Measuring a basis state `|x⟩` gives outcome `x` with certainty. -/ +theorem measureProb_ket [DecidableEq ι] (x : ι) (S : Finset ι) : + measureProb (ket x) S = if x ∈ S then 1 else 0 := by + simp [measureProb, apply_ite] + theorem measureProb_le_measureProb_univ [Fintype ι] (ψ : EuclideanSpace ℂ ι) (S : Finset ι) : measureProb ψ S ≤ measureProb ψ univ := sum_le_sum_of_subset_of_nonneg (subset_univ S) fun _ _ _ => by positivity diff --git a/ComplexityTests/BQP.lean b/ComplexityTests/BQP.lean new file mode 100644 index 000000000..6a838bba7 --- /dev/null +++ b/ComplexityTests/BQP.lean @@ -0,0 +1,169 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.Classes.BQP + +/-! `BQP`: uniform families that decide a language exactly, interference, closure under +complement, and a family whose acceptance probability `1 / 2` decides nothing. -/ + +namespace ComplexityTests.BQP + +open Cslib Cslib.Quantum Cslib.Complexity Turing.MultiTapeTM + +/-! ### Gate codes -/ + +-- A Toffoli gate with controls `0, 1` and target `2` is well formed on three qubits, but not on +-- two, nor with a repeated qubit, nor with three controls; Hadamard gates take no controls. +example : GateCode.WellFormed 3 (false, 2, [0, 1]) := by decide +example : ¬GateCode.WellFormed 2 (false, 2, [0, 1]) := by decide +example : ¬GateCode.WellFormed 3 (false, 1, [1]) := by decide +example : ¬GateCode.WellFormed 5 (false, 0, [1, 2, 3]) := by decide +example : GateCode.WellFormed 1 (true, 0, []) := by decide +example : ¬GateCode.WellFormed 2 (true, 0, [1]) := by decide + +-- The Toffoli code maps `|110⟩` to `|111⟩`. +example : ∃ g, GateCode.toPlacedGate? 3 (false, 2, [0, 1]) = some g ∧ + g.eval (ket ![true, true, false]) = ket ![true, true, true] := by + obtain ⟨g, hg⟩ := Option.isSome_iff_exists.mp + (GateCode.isSome_toPlacedGate?_iff.mpr (by decide : GateCode.WellFormed 3 (false, 2, [0, 1]))) + refine ⟨g, hg, ?_⟩ + rw [GateCode.eval_toPlacedGate_ket hg (by decide)] + congr 1 + funext i + fin_cases i <;> rfl + +/-! ### A family that reads the first input bit -/ + +/-- The family with one qubit more than the input and no gates: it measures the first input bit. -/ +def readFirst : UniformCircuitFamily where + width n := n + 1 + gates _ := [] + computableInPolyTime_width := by fun_prop + computableInPolyTime_gates := ComputableInPolyTime.const _ + le_width n := Nat.le_succ n + width_pos n := Nat.succ_pos n + wellFormed _ _ h := by simp at h + +/-- With no gates, the input basis state is measured, so the first input bit is read exactly. -/ +theorem acceptProb_readFirst (x : List Bool) : + readFirst.acceptProb x = if x.headD false then 1 else 0 := by + change measureProb (Circuit.run (Circuit.ofCodes (x.length + 1) []) (inputState _ x)) + (accepting _) = _ + simp only [Circuit.ofCodes_nil, Circuit.run, Circuit.eval_nil, measureProb_ket, + mem_accepting (Nat.succ_pos _), inputState] + cases x <;> rfl + +/-- The words whose first bit is one. -/ +def FirstBit : Set (List Bool) := {x | x.headD false = true} + +/-- Deciding the first bit, exactly: a member and a nonmember of `BQP`. -/ +theorem firstBit_mem_BQP : FirstBit ∈ BQP encBits := by + refine ⟨readFirst, fun x => ⟨fun hx => ?_, fun hx => ?_⟩⟩ + · rw [encBits_apply, acceptProb_readFirst] + simp only [show x.headD false = true from hx, ite_true] + norm_num + · rw [encBits_apply, acceptProb_readFirst] + simp only [show x.headD false = false from Bool.eq_false_iff.mpr hx, Bool.false_eq_true, + ite_false] + norm_num + +example : FirstBitᶜ ∈ BQP encBits := compl_mem_BQP firstBit_mem_BQP + +-- The bounds are not vacuous: `readFirst` accepts `[true]` with probability one, so it does not +-- witness that the complement of `FirstBit` is in `BQP`. +example : ¬(readFirst.acceptProb (encBits [true]) ≤ 1 / 3) := by + rw [encBits_apply, acceptProb_readFirst] + norm_num + +/-! ### Interference -/ + +/-- Two Hadamard gates on qubit `0`: they cancel. -/ +def hadamardTwice : UniformCircuitFamily where + width n := n + 1 + gates _ := [(true, 0, []), (true, 0, [])] + computableInPolyTime_width := by fun_prop + computableInPolyTime_gates := ComputableInPolyTime.const _ + le_width n := Nat.le_succ n + width_pos n := Nat.succ_pos n + wellFormed n g hg := by + simp only [List.mem_cons, List.not_mem_nil, or_false, or_self] at hg + subst hg + exact ⟨Nat.succ_pos n, rfl⟩ + +-- `HH = I`: the two gates interfere, and the family reads the first bit like `readFirst`. +example (x : List Bool) : hadamardTwice.acceptProb x = readFirst.acceptProb x := by + have hrun (m : ℕ) (hm : 0 < m) (z : Fin m → Bool) : + Circuit.run (Circuit.ofCodes m [(true, 0, []), (true, 0, [])]) z = ket z := by + simp only [Circuit.ofCodes, List.filterMap_cons, List.filterMap_nil, GateCode.toPlacedGate?, + hm, ↓reduceDIte, Circuit.run, Circuit.eval_cons, Circuit.eval_nil, PlacedGate.eval, + ← unitaryEquiv_mul, PlacedGate.matrix, ← map_mul, Gate.hadamard_mul_self, map_one, + unitaryEquiv_one] + change measureProb (Circuit.run (Circuit.ofCodes (x.length + 1) [(true, 0, []), (true, 0, [])]) + (inputState _ x)) (accepting _) = + measureProb (Circuit.run (Circuit.ofCodes (x.length + 1) []) (inputState _ x)) (accepting _) + rw [hrun _ (Nat.succ_pos _)] + simp only [Circuit.ofCodes_nil, Circuit.run, Circuit.eval_nil] + +/-! ### A family that decides nothing -/ + +/-- One Hadamard gate on qubit `0`. -/ +def hadamardOnce : UniformCircuitFamily where + width n := n + 1 + gates _ := [(true, 0, [])] + computableInPolyTime_width := by fun_prop + computableInPolyTime_gates := ComputableInPolyTime.const _ + le_width n := Nat.le_succ n + width_pos n := Nat.succ_pos n + wellFormed n g hg := by + rw [List.mem_singleton.mp hg] + exact ⟨Nat.succ_pos n, rfl⟩ + +/-- A Hadamard gate on qubit `0` makes it read `1` with probability `1 / 2`, whatever the input. -/ +theorem acceptProb_hadamardOnce (x : List Bool) : hadamardOnce.acceptProb x = 1 / 2 := by + set m := x.length + 1 + have hm : 0 < m := Nat.succ_pos _ + obtain ⟨g, hg⟩ : ∃ g, GateCode.toPlacedGate? m (true, 0, []) = some g := + Option.isSome_iff_exists.mp (GateCode.isSome_toPlacedGate?_iff.mpr + (⟨hm, rfl⟩ : GateCode.WellFormed m (true, 0, []))) + set z := inputState m x + have hrun : Circuit.run (Circuit.ofCodes m [(true, 0, [])]) z = g.eval (ket z) := by + simp [Circuit.ofCodes, hg, Circuit.run] + have hnorm (c : ℂ) (hc : ‖c‖ = 1) : ‖c * (((Real.sqrt 2)⁻¹ : ℝ) : ℂ)‖ ^ 2 = 1 / 2 := by + rw [norm_mul, hc, one_mul, Complex.norm_real, Real.norm_eq_abs, abs_inv, + abs_of_nonneg (Real.sqrt_nonneg 2), inv_pow, Real.sq_sqrt (by norm_num)] + norm_num + -- only the outcome `z[0 ↦ 1]` is accepting and reachable + have hentry (y : Fin m → Bool) (hy : y ∈ accepting m) : + ‖(g.eval (ket z)).ofLp y‖ ^ 2 = if y = Function.update z ⟨0, hm⟩ true then 1 / 2 else 0 := by + rw [mem_accepting hm] at hy + have hne : y ≠ Function.update z ⟨0, hm⟩ false := fun h => by + simp [h] at hy + rw [GateCode.eval_toPlacedGate_hadamard_ket hg hm, Fintype.sum_bool] + simp only [WithLp.ofLp_add, WithLp.ofLp_smul, Pi.add_apply, Pi.smul_apply, ket_apply, + smul_eq_mul, mul_ite, mul_one, mul_zero, hne, ite_false, add_zero] + split_ifs <;> first | exact hnorm _ (by simp) | simp + have hmem : Function.update z ⟨0, hm⟩ true ∈ accepting m := by + rw [mem_accepting hm, Function.update_self] + simp only [UniformCircuitFamily.acceptProb, acceptProb, hadamardOnce] + change measureProb (Circuit.run (Circuit.ofCodes m [(true, 0, [])]) z) (accepting m) = 1 / 2 + rw [hrun, measureProb, Finset.sum_congr rfl hentry, Finset.sum_ite_eq' _ _ _] + simp only [hmem, ite_true] + +/-- Acceptance probability `1 / 2` is neither at least `2 / 3` nor at most `1 / 3`, so +`hadamardOnce` decides no set of words with bounded error. -/ +example (A : Set (List Bool)) : ¬∀ x, + (x ∈ A → 2 / 3 ≤ hadamardOnce.acceptProb (encBits x)) ∧ + (x ∉ A → hadamardOnce.acceptProb (encBits x) ≤ 1 / 3) := by + intro h + by_cases hx : ([] : List Bool) ∈ A + · have := (h []).1 hx + rw [acceptProb_hadamardOnce] at this + norm_num at this + · have := (h []).2 hx + rw [acceptProb_hadamardOnce] at this + norm_num at this + +end ComplexityTests.BQP diff --git a/references.bib b/references.bib index 248ed73df..de1189a35 100644 --- a/references.bib +++ b/references.bib @@ -39,6 +39,17 @@ @inproceedings{Adleman1978 doi = {10.1109/SFCS.1978.37} } +@article{AdlemanDeMarraisHuang1997, + author = {Adleman, Leonard M. and DeMarrais, Jonathan and Huang, Ming-Deh A.}, + title = {Quantum Computability}, + journal = {SIAM Journal on Computing}, + volume = {26}, + number = {5}, + pages = {1524--1540}, + year = {1997}, + doi = {10.1137/S0097539795293639} +} + @article{AFvMV2006, author = {Antunes, Lu{\'i}s and Fortnow, Lance and van Melkebeek, Dieter and Vinodchandran, N. V.}, @@ -49,6 +60,14 @@ @article{AFvMV2006 year = {2006} } +@misc{Aharonov2003, + author = {Aharonov, Dorit}, + title = {A Simple Proof that {T}offoli and {H}adamard are Quantum Universal}, + year = {2003}, + eprint = {quant-ph/0301040}, + archivePrefix = {arXiv} +} + @article{Ajtai1983, author = {Ajtai, Mikl{\'o}s}, title = {{$\Sigma^1_1$}-Formulae on Finite Structures}, @@ -615,6 +634,17 @@ @article{BermanHartmanis1977 doi = {10.1137/0206023} } +@article{BernsteinVazirani1997, + author = {Bernstein, Ethan and Vazirani, Umesh}, + title = {Quantum Complexity Theory}, + journal = {SIAM Journal on Computing}, + volume = {26}, + number = {5}, + pages = {1411--1473}, + year = {1997}, + doi = {10.1137/S0097539796300921} +} + @article{Bird2011, author = {Bird, Richard S.}, title = {A Simple Division-Free Algorithm for Computing Determinants}, From 5b21c57baaf3eff4a6cd4f4fdf51bea7c7efb257 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 00:28:39 -0400 Subject: [PATCH 2/4] feat(Classes/BQP): error reduction for BQP by reversible majority vote (#896 M2) A problem is in BQP exactly when, for every polynomial q, some uniform family errs with probability at most 2^{-q(n)}. The amplified family runs 2r copies of the circuit on disjoint blocks, counts their answers with a reversible thermometer counter of CNOT/Toffoli gates, and swaps the strict majority into qubit 0. Copies on disjoint blocks act independently, so the acceptance probability is exactly that of a strict majority of 2r independent trials; a weighted exponential-moment bound gives (8/9)^r. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 5 + .../Circuit/Quantum/Classical.lean | 296 ++++++++ .../Circuit/Quantum/Counter.lean | 227 +++++++ .../Circuit/Quantum/Parallel.lean | 341 ++++++++++ .../Complexity/Classes/BQP/Amplification.lean | 642 ++++++++++++++++++ .../Combinatorics/MajorityVote/Weighted.lean | 109 +++ ComplexityTests/BQPAmplification.lean | 55 ++ 7 files changed, 1675 insertions(+) create mode 100644 Complexity/Computability/Circuit/Quantum/Classical.lean create mode 100644 Complexity/Computability/Circuit/Quantum/Counter.lean create mode 100644 Complexity/Computability/Circuit/Quantum/Parallel.lean create mode 100644 Complexity/Computability/Complexity/Classes/BQP/Amplification.lean create mode 100644 Complexity/Foundations/Combinatorics/MajorityVote/Weighted.lean create mode 100644 ComplexityTests/BQPAmplification.lean diff --git a/Complexity.lean b/Complexity.lean index 7accc0251..1c966dc5d 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -937,7 +937,10 @@ 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.Classical public import Complexity.Computability.Circuit.Quantum.Code +public import Complexity.Computability.Circuit.Quantum.Counter +public import Complexity.Computability.Circuit.Quantum.Parallel public import Complexity.Computability.Circuit.Quantum.Uniform public import Complexity.Computability.Circuit.Rational public import Complexity.Computability.Circuit.Rational.Affine @@ -1045,6 +1048,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.Amplification public import Complexity.Computability.Complexity.Classes.BooleanHierarchy public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Closure public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Kadin @@ -2594,6 +2598,7 @@ public import Complexity.Foundations.Combinatorics.LineCode.Menu.Collision public import Complexity.Foundations.Combinatorics.LineCode.Menu.Counting public import Complexity.Foundations.Combinatorics.MajorityTree public import Complexity.Foundations.Combinatorics.MajorityVote +public import Complexity.Foundations.Combinatorics.MajorityVote.Weighted public import Complexity.Foundations.Combinatorics.Multigraph public import Complexity.Foundations.Combinatorics.PacketPacking public import Complexity.Foundations.Combinatorics.PartialLabelScores diff --git a/Complexity/Computability/Circuit/Quantum/Classical.lean b/Complexity/Computability/Circuit/Quantum/Classical.lean new file mode 100644 index 000000000..3937b2bd2 --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/Classical.lean @@ -0,0 +1,296 @@ +/- +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 + +/-! +# Classical gate codes on basis states + +The classical gate codes NOT, CNOT and Toffoli of +`Complexity/Computability/Circuit/Quantum/Code.lean` permute the computational basis: the code +`(false, t, cs)` flips bit `t` when every bit of `cs` is one +(`Cslib.Quantum.GateCode.classicalStep`). A list of classical codes therefore maps the basis +state `|x⟩` to the basis state of the composed permutation +(`Cslib.Quantum.Circuit.eval_ofCodes_ket`), and it acts on any state by reading amplitudes back +through the inverse permutation (`Cslib.Quantum.Circuit.eval_ofCodes_apply`). Measuring after a +classical circuit is measuring before it and then applying the permutation to the outcome +(`Cslib.Quantum.Circuit.measureProb_eval_ofCodes`). + +Bits of a basis string are read by their number (`Cslib.Quantum.readBit`), as in gate codes. + +## Main definitions + +* `Cslib.Quantum.readBit`: bit `c` of a basis string, `false` past its end. +* `Cslib.Quantum.GateCode.classicalStep`: the permutation of a classical gate code. +* `Cslib.Quantum.GateCode.IsClassical`: a list of well-formed classical gate codes. +* `Cslib.Quantum.GateCode.classicalRun`, `Cslib.Quantum.GateCode.classicalUnrun`: the composed + permutation of a list of classical codes and its inverse. + +## Main results + +* `Cslib.Quantum.GateCode.readBit_classicalStep`: a classical code changes only its target. +* `Cslib.Quantum.Circuit.eval_ofCodes_ket`, `Cslib.Quantum.Circuit.eval_ofCodes_apply`: classical + circuits permute basis states. +* `Cslib.Quantum.Circuit.measureProb_eval_ofCodes`: measuring after a classical circuit. +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Finset + +variable {m : ℕ} + +/-- Bit number `c` of a basis string, and `false` past its end. -/ +def readBit (x : Fin m → Bool) (c : ℕ) : Bool := (List.ofFn x).getD c false + +theorem readBit_of_lt (x : Fin m → Bool) {c : ℕ} (h : c < m) : readBit x c = x ⟨c, h⟩ := by + simp [readBit, List.getD_eq_getElem?_getD, h] + +theorem readBit_of_le (x : Fin m → Bool) {c : ℕ} (h : m ≤ c) : readBit x c = false := by + simp [readBit, List.getD_eq_getElem?_getD, h] + +@[simp] theorem readBit_fin (x : Fin m → Bool) (i : Fin m) : readBit x i = x i := + readBit_of_lt x i.2 + +/-- Basis strings are equal when they have the same bits. -/ +theorem funext_readBit {x y : Fin m → Bool} (h : ∀ c, readBit x c = readBit y c) : x = y := + funext fun i => by simpa using h i + +namespace GateCode + +/-- The permutation of basis strings of the classical gate code `(false, t, cs)`: bit `t` flips when +every bit of `cs` is one. It is the identity when `t` is out of range. -/ +def classicalStep (g : GateCode) (x : Fin m → Bool) : Fin m → Bool := + if h : g.2.1 < m then Function.update x ⟨g.2.1, h⟩ (x ⟨g.2.1, h⟩ ^^ g.2.2.all (readBit x)) + else x + +/-- **A classical code changes only its target bit**, flipping it when all its controls are one. -/ +theorem readBit_classicalStep (g : GateCode) (x : Fin m → Bool) (c : ℕ) : + readBit (classicalStep g x) c = + (readBit x c ^^ (decide (c = g.2.1 ∧ g.2.1 < m) && g.2.2.all (readBit x))) := by + unfold classicalStep + split_ifs with h + · by_cases hc : c < m + · rw [readBit_of_lt _ hc, readBit_of_lt _ hc] + by_cases hct : c = g.2.1 + · subst hct + simp [h] + · rw [Function.update_of_ne (fun h' => hct (congrArg Fin.val h'))] + simp [hct] + · rw [readBit_of_le _ (not_lt.mp hc), readBit_of_le _ (not_lt.mp hc)] + have : c ≠ g.2.1 := fun h' => hc (h' ▸ h) + simp [this] + · simp [h] + +/-- Bits other than the target of a classical code read the same after it acts. -/ +theorem all_readBit_classicalStep {g : GateCode} (x : Fin m → Bool) + (cs : List ℕ) (hcs : g.2.1 ∉ cs) : + cs.all (readBit (classicalStep g x)) = cs.all (readBit x) := by + induction cs with + | nil => rfl + | cons c cs ih => + rw [List.all_cons, List.all_cons, ih (fun h => hcs (List.mem_cons_of_mem _ h)), + readBit_classicalStep] + have : c ≠ g.2.1 := fun h => hcs (h ▸ List.mem_cons_self ..) + simp [this] + +/-- **A classical code is an involution** when its target is not one of its controls. -/ +theorem classicalStep_classicalStep {g : GateCode} (hg : g.2.1 ∉ g.2.2) (x : Fin m → Bool) : + classicalStep g (classicalStep g x) = x := by + refine funext_readBit fun c => ?_ + rw [readBit_classicalStep, all_readBit_classicalStep x _ hg, readBit_classicalStep, + Bool.xor_assoc, Bool.xor_self, Bool.xor_false] + +/-- A list of **classical gate codes**, well formed on `m` qubits: NOT, CNOT and Toffoli gates. -/ +def IsClassical (m : ℕ) (gs : List GateCode) : Prop := + ∀ g ∈ gs, g.1 = false ∧ WellFormed m g + +theorem IsClassical.cons {g : GateCode} {gs : List GateCode} : + IsClassical m (g :: gs) ↔ (g.1 = false ∧ WellFormed m g) ∧ IsClassical m gs := + List.forall_mem_cons + +theorem IsClassical.append {gs hs : List GateCode} : + IsClassical m (gs ++ hs) ↔ IsClassical m gs ∧ IsClassical m hs := + List.forall_mem_append + +theorem IsClassical.flatMap {β : Type*} {l : List β} {f : β → List GateCode} + (h : ∀ b ∈ l, IsClassical m (f b)) : IsClassical m (l.flatMap f) := by + intro g hg + obtain ⟨b, hb, hg⟩ := List.mem_flatMap.mp hg + exact h b hb g hg + +/-- The target of a well-formed classical code is not one of its controls. -/ +theorem target_notMem_of_wellFormed {g : GateCode} (h₁ : g.1 = false) (h₂ : WellFormed m g) : + g.2.1 ∉ g.2.2 := by + obtain ⟨b, t, cs⟩ := g + subst h₁ + exact (List.nodup_cons.mp h₂.2.1).1 + +/-- The composed permutation of a list of classical codes, applied first to last. -/ +def classicalRun (gs : List GateCode) (x : Fin m → Bool) : Fin m → Bool := + gs.foldl (fun y g => classicalStep g y) x + +/-- The inverse of `classicalRun`: the permutations applied last to first. -/ +def classicalUnrun (gs : List GateCode) (y : Fin m → Bool) : Fin m → Bool := + gs.foldr (fun g y => classicalStep g y) y + +@[simp] theorem classicalRun_nil (x : Fin m → Bool) : classicalRun [] x = x := rfl + +@[simp] theorem classicalRun_cons (g : GateCode) (gs : List GateCode) (x : Fin m → Bool) : + classicalRun (g :: gs) x = classicalRun gs (classicalStep g x) := rfl + +theorem classicalRun_append (gs hs : List GateCode) (x : Fin m → Bool) : + classicalRun (gs ++ hs) x = classicalRun hs (classicalRun gs x) := + List.foldl_append + +@[simp] theorem classicalUnrun_nil (y : Fin m → Bool) : classicalUnrun [] y = y := rfl + +@[simp] theorem classicalUnrun_cons (g : GateCode) (gs : List GateCode) (y : Fin m → Bool) : + classicalUnrun (g :: gs) y = classicalStep g (classicalUnrun gs y) := rfl + +theorem classicalUnrun_classicalRun {gs : List GateCode} (h : IsClassical m gs) + (x : Fin m → Bool) : classicalUnrun gs (classicalRun gs x) = x := by + induction gs generalizing x with + | nil => rfl + | cons g gs ih => + obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h + rw [classicalRun_cons, classicalUnrun_cons, ih h, + classicalStep_classicalStep (target_notMem_of_wellFormed h₁ h₂)] + +theorem classicalRun_classicalUnrun {gs : List GateCode} (h : IsClassical m gs) + (y : Fin m → Bool) : classicalRun gs (classicalUnrun gs y) = y := by + induction gs generalizing y with + | nil => rfl + | cons g gs ih => + obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h + rw [classicalUnrun_cons, classicalRun_cons, + classicalStep_classicalStep (target_notMem_of_wellFormed h₁ h₂), ih h] + +theorem classicalRun_flatMap {β : Type*} (l : List β) (f : β → List GateCode) + (x : Fin m → Bool) : + classicalRun (l.flatMap f) x = l.foldl (fun y b => classicalRun (f b) y) x := + List.foldl_flatMap + +/-- **Classical codes that never read a written bit** add to each bit the controls' values on the +initial string, one for each code writing that bit. -/ +theorem readBit_classicalRun_of_forall_notMem {gs : List GateCode} (h : IsClassical m gs) + (hread : ∀ g ∈ gs, ∀ g' ∈ gs, g.2.1 ∉ g'.2.2) (x : Fin m → Bool) (p : ℕ) : + readBit (classicalRun gs x) p = + gs.foldl (fun b g => b ^^ (decide (p = g.2.1) && g.2.2.all (readBit x))) (readBit x p) := by + induction gs generalizing x with + | nil => rfl + | cons g gs ih => + obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h + have ht : g.2.1 < m := by + obtain ⟨b, t, cs⟩ := g + subst h₁ + exact h₂.2.2 t (List.mem_cons_self ..) + rw [classicalRun_cons, ih h (fun g₁ hg₁ g₂ hg₂ => hread g₁ (List.mem_cons_of_mem _ hg₁) g₂ + (List.mem_cons_of_mem _ hg₂)), List.foldl_cons, readBit_classicalStep] + simp only [ht, and_true] + refine List.foldl_ext _ _ _ fun b g' hg' => ?_ + rw [all_readBit_classicalStep x _ (hread g (List.mem_cons_self ..) g' + (List.mem_cons_of_mem _ hg'))] + +/-- An exclusive or over a range in which only the term `i₀` can be nonzero. -/ +theorem foldl_xor_range (T i₀ : ℕ) (f : ℕ → Bool) (b : Bool) (hf : ∀ i < T, i ≠ i₀ → f i = false) : + (List.range T).foldl (fun b i => b ^^ f i) b = (b ^^ (decide (i₀ < T) && f i₀)) := by + induction T with + | zero => simp + | succ T ih => + rw [List.range_succ, List.foldl_append, ih fun i hi hne => hf i (by omega) hne] + simp only [List.foldl_cons, List.foldl_nil] + by_cases hT : T = i₀ + · subst hT + simp + · rw [hf T (by omega) hT] + by_cases hlt : i₀ < T + · simp [hlt, show i₀ < T + 1 by omega] + · simp [hlt, show ¬i₀ < T + 1 by omega] + +/-- A well-formed classical code denotes a gate that maps `|x⟩` to `|classicalStep g x⟩`. -/ +theorem exists_toPlacedGate?_eval_ket {g : GateCode} (h₁ : g.1 = false) (h₂ : WellFormed m g) : + ∃ pg, toPlacedGate? m g = some pg ∧ ∀ x, pg.eval (ket x) = ket (classicalStep g x) := by + obtain ⟨pg, hpg⟩ := Option.isSome_iff_exists.mp (isSome_toPlacedGate?_iff.mpr h₂) + obtain ⟨b, t, cs⟩ := g + subst h₁ + have ht : t < m := h₂.2.2 t (List.mem_cons_self ..) + refine ⟨pg, hpg, fun x => ?_⟩ + rw [eval_toPlacedGate_ket hpg ht] + simp only [classicalStep, ht, ↓reduceDIte] + rfl + +/-- A well-formed classical code reads each amplitude at the permuted basis string. -/ +theorem exists_toPlacedGate?_eval_apply {g : GateCode} (h₁ : g.1 = false) (h₂ : WellFormed m g) : + ∃ pg, toPlacedGate? m g = some pg ∧ + ∀ (ψ : Qubits m) y, (pg.eval ψ).ofLp y = ψ.ofLp (classicalStep g y) := by + obtain ⟨pg, hpg, hket⟩ := exists_toPlacedGate?_eval_ket h₁ h₂ + refine ⟨pg, hpg, fun ψ y => ?_⟩ + have hinv := classicalStep_classicalStep (m := m) (target_notMem_of_wellFormed h₁ h₂) + have hrow (z : Fin m → Bool) : + (pg.matrix : Matrix _ _ ℂ) y z = if z = classicalStep g 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, hinv] + · rw [h, hinv] + simp only [PlacedGate.eval, unitaryEquiv_apply, Matrix.mulVec, dotProduct, hrow, ite_mul, + one_mul, zero_mul, sum_ite_eq', mem_univ, ite_true] + +end GateCode + +open GateCode + +namespace Circuit + +/-- **A classical circuit permutes basis states.** -/ +theorem eval_ofCodes_ket {gs : List GateCode} (h : IsClassical m gs) (x : Fin m → Bool) : + eval (ofCodes m gs) (ket x) = ket (classicalRun gs x) := by + induction gs generalizing x with + | nil => simp + | cons g gs ih => + obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h + obtain ⟨pg, hpg, hket⟩ := exists_toPlacedGate?_eval_ket h₁ h₂ + simp only [ofCodes, List.filterMap_cons, hpg, eval_cons, hket, classicalRun_cons] + exact ih h _ + +/-- A classical circuit started in `|x⟩` ends in `|classicalRun gs x⟩`. -/ +theorem run_ofCodes {gs : List GateCode} (h : IsClassical m gs) (x : Fin m → Bool) : + run (ofCodes m gs) x = ket (classicalRun gs x) := + eval_ofCodes_ket h x + +/-- **A classical circuit reads amplitudes through the inverse permutation.** -/ +theorem eval_ofCodes_apply {gs : List GateCode} (h : IsClassical m gs) (ψ : Qubits m) + (y : Fin m → Bool) : (eval (ofCodes m gs) ψ).ofLp y = ψ.ofLp (classicalUnrun gs y) := by + induction gs generalizing ψ with + | nil => simp + | cons g gs ih => + obtain ⟨⟨h₁, h₂⟩, h⟩ := IsClassical.cons.mp h + obtain ⟨pg, hpg, happly⟩ := exists_toPlacedGate?_eval_apply h₁ h₂ + simp only [ofCodes, List.filterMap_cons, hpg, eval_cons, classicalUnrun_cons] + rw [← happly] + exact ih h _ + +/-- **Measuring after a classical circuit** is measuring before it and permuting the outcome. -/ +theorem measureProb_eval_ofCodes {gs : List GateCode} (h : IsClassical m gs) (ψ : Qubits m) + (S : Finset (Fin m → Bool)) : + measureProb (eval (ofCodes m gs) ψ) S = + ∑ x, if classicalRun gs x ∈ S then ‖ψ.ofLp x‖ ^ 2 else 0 := by + rw [measureProb, ← sum_filter] + simp only [eval_ofCodes_apply h] + refine sum_nbij' (classicalUnrun gs) (classicalRun gs) (fun y hy => ?_) (fun x hx => ?_) + (fun y _ => classicalRun_classicalUnrun h y) (fun x _ => classicalUnrun_classicalRun h x) + (fun y _ => rfl) + · simpa [classicalRun_classicalUnrun h] using hy + · simpa using (mem_filter.mp hx).2 + +end Circuit + +end Cslib.Quantum diff --git a/Complexity/Computability/Circuit/Quantum/Counter.lean b/Complexity/Computability/Circuit/Quantum/Counter.lean new file mode 100644 index 000000000..6248614ae --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/Counter.lean @@ -0,0 +1,227 @@ +/- +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.Classical + +/-! +# A reversible threshold counter + +A classical circuit of CNOT and Toffoli gates that counts, in unary, how many of `k` input bits +are one, up to a threshold `T` (`Cslib.Quantum.Counter.codes`). Its ancillas start at zero: qubit +`base` is set to one, and stage `s` has `T` fresh qubits, its *levels* +(`Cslib.Quantum.Counter.level`). After stage `s`, level `i` reads whether more than `i` of the +first `s` input bits are one. Stage `s + 1` reads the next input bit `b` and sets each new level +to the old level `i - 1` when `b` is one and to the old level `i` otherwise, with three gates: the +multiplexer `t ⊕ (b ∧ u) ⊕ (b ∧ t)` of the old levels `t` and `u`. No gate reads a qubit written in +the same stage, so each stage is computed from the previous one +(`Cslib.Quantum.GateCode.readBit_classicalRun_of_forall_notMem`). + +The last level of the last stage is the threshold function of the input bits +(`Cslib.Quantum.Counter.readBit_classicalRun_codes`); with `k = 2 r` inputs and `T = r + 1` levels +it is their strict majority. This is the reversible majority vote used to amplify the success +probability of quantum circuits. + +## Main definitions + +* `Cslib.Quantum.Counter.level`, `Cslib.Quantum.Counter.stage`, `Cslib.Quantum.Counter.codes`. +* `Cslib.Quantum.Counter.count`: the number of input bits that are one. + +## Main results + +* `Cslib.Quantum.Counter.isClassical_codes`: the counter is a classical circuit. +* `Cslib.Quantum.Counter.readBit_classicalRun_codes`: it computes the threshold function and + leaves the qubits below `base` unchanged. +-/ + +@[expose] public section + +namespace Cslib.Quantum.Counter + +open Finset GateCode + +variable {N : ℕ} + +/-- The qubit of level `i` of stage `s`: after stage `s` it reads whether more than `i` of the +first `s` input bits are one. -/ +def level (base T s i : ℕ) : ℕ := base + 1 + s * T + i + +/-- The qubit of level `i - 1` of stage `s`, where level `-1` is the qubit `base`, set to one. -/ +def below (base T s i : ℕ) : ℕ := if i = 0 then base else level base T s (i - 1) + +/-- Stage `s + 1` of the counter, reading the input bit at `b`: level `i` becomes level `i - 1` of +stage `s` when the bit is one, and level `i` of stage `s` otherwise. -/ +def stage (base T b s : ℕ) : List GateCode := + (List.range T).flatMap fun i => + [(false, level base T (s + 1) i, [level base T s i]), + (false, level base T (s + 1) i, [b, below base T s i]), + (false, level base T (s + 1) i, [b, level base T s i])] + +/-- The counter for the input bits at `src 0, …, src (k - 1)`, with `T` levels and ancillas from +`base` on: set qubit `base` to one, then run the stages. -/ +def codes (base T : ℕ) (src : ℕ → ℕ) (k : ℕ) : List GateCode := + (false, base, []) :: (List.range k).flatMap fun s => stage base T (src s) s + +/-- The number of input bits that are one among the first `s`. -/ +def count (x : Fin N → Bool) (src : ℕ → ℕ) (s : ℕ) : ℕ := + ((range s).filter fun j => readBit x (src j) = true).card + +theorem count_succ (x : Fin N → Bool) (src : ℕ → ℕ) (s : ℕ) : + count x src (s + 1) = count x src s + if readBit x (src s) = true then 1 else 0 := by + unfold count + rw [range_add_one, filter_insert] + split_ifs with h + · rw [card_insert_of_notMem (fun h' => by simpa using (mem_filter.mp h').1)] + · rw [Nat.add_zero] + +private theorem level_lt {base T s i : ℕ} (hi : i < T) : + level base T s i < base + 1 + (s + 1) * T := by + unfold level + rw [Nat.add_mul, Nat.one_mul] + omega + +theorem isClassical_stage {base T b s : ℕ} (hb : b < base) (hN : base + 1 + (s + 2) * T ≤ N) : + IsClassical N (stage base T b s) := by + refine IsClassical.flatMap fun i hi => ?_ + have hi : i < T := List.mem_range.mp hi + have h₁ := level_lt (base := base) (s := s + 1) hi + have h₀ : base + 1 + s * T + i < base + 1 + (s + 1) * T * 1 := by + rw [Nat.mul_one, Nat.add_mul, Nat.one_mul] + omega + rw [show s + 2 = s + 1 + 1 by rfl, Nat.add_mul (s + 1), Nat.one_mul] at hN + rw [Nat.add_mul, Nat.one_mul] at h₁ + rw [Nat.mul_one, Nat.add_mul, Nat.one_mul] at h₀ + have hl : base + 1 + (s + 1) * T + i = base + 1 + s * T + T + i := by + rw [Nat.add_mul, Nat.one_mul] + omega + simp only [IsClassical, List.mem_cons, List.not_mem_nil, or_false, forall_eq_or_imp, + forall_eq, WellFormed, List.length_cons, List.length_nil, List.nodup_cons, List.mem_cons, + List.not_mem_nil, List.nodup_nil, level, below, hl] + split_ifs with h0 <;> refine ⟨⟨trivial, ?_⟩, ⟨trivial, ?_⟩, ⟨trivial, ?_⟩⟩ <;> simp <;> omega + +theorem isClassical_codes {base T k : ℕ} {src : ℕ → ℕ} (hsrc : ∀ s < k, src s < base) + (hN : base + 1 + (k + 1) * T ≤ N) : IsClassical N (codes base T src k) := by + refine IsClassical.cons.mpr ⟨⟨rfl, ?_⟩, IsClassical.flatMap fun s hs => ?_⟩ + · have : base < N := by omega + simp [WellFormed, this] + · have hs : s < k := List.mem_range.mp hs + refine isClassical_stage (hsrc s hs) (le_trans ?_ hN) + have : (s + 2) * T ≤ (k + 1) * T := Nat.mul_le_mul_right T (by omega) + omega + +/-- The bits after `s` stages: unchanged below `base`, one at `base`, the threshold values on the +levels of stage `s`, and zero from the levels of stage `s + 1` on. -/ +private def Invariant (base T : ℕ) (src : ℕ → ℕ) (x y : Fin N → Bool) (s : ℕ) : Prop := + (∀ p < base, readBit y p = readBit x p) ∧ readBit y base = true ∧ + (∀ i < T, readBit y (level base T s i) = decide (i < count x src s)) ∧ + ∀ p, base + 1 + (s + 1) * T ≤ p → readBit y p = false + +private theorem invariant_zero {base T : ℕ} {src : ℕ → ℕ} (hN : base < N) (x : Fin N → Bool) + (hx : ∀ p, base ≤ p → readBit x p = false) : + Invariant base T src x (classicalStep (false, base, []) x) 0 := by + have hstep (p : ℕ) : readBit (classicalStep (false, base, []) x) p = + (readBit x p ^^ decide (p = base)) := by + rw [readBit_classicalStep] + simp [hN] + refine ⟨fun p hp => ?_, ?_, fun i hi => ?_, fun p hp => ?_⟩ + · rw [hstep] + simp [show p ≠ base by omega] + · rw [hstep, hx base le_rfl] + simp + · rw [hstep, hx _ (by unfold level; omega)] + simp only [count, level, Nat.zero_mul, Nat.add_zero, range_zero, filter_empty, card_empty, + Nat.not_lt_zero, decide_false, Bool.false_xor, decide_eq_false_iff_not] + omega + · rw [hstep, hx _ (by omega)] + simp only [Nat.zero_add, Nat.one_mul] at hp + simp [show p ≠ base by omega] + +private theorem invariant_succ {base T s : ℕ} {src : ℕ → ℕ} (hsrc : src s < base) + (hN : base + 1 + (s + 2) * T ≤ N) {x y : Fin N → Bool} (hy : Invariant base T src x y s) : + Invariant base T src x (classicalRun (stage base T (src s) s) y) (s + 1) := by + obtain ⟨hlow, hbase, hlev, hhigh⟩ := hy + have hcl := isClassical_stage (N := N) hsrc hN + rw [show s + 2 = s + 1 + 1 by rfl, Nat.add_mul (s + 1), Nat.one_mul, Nat.add_mul, + Nat.one_mul] at hN + -- the stage reads no bit it writes + have hread : ∀ g ∈ stage base T (src s) s, ∀ g' ∈ stage base T (src s) s, g.2.1 ∉ g'.2.2 := by + intro g hg g' hg' + simp only [stage, List.mem_flatMap, List.mem_range, List.mem_cons, List.not_mem_nil, + or_false] at hg hg' + obtain ⟨i, hi, rfl | rfl | rfl⟩ := hg <;> obtain ⟨i', hi', rfl | rfl | rfl⟩ := hg' <;> + simp only [level, below, List.mem_cons, List.not_mem_nil, or_false, Nat.add_mul, + Nat.one_mul] <;> (try split_ifs) <;> omega + -- each bit, as a sum over the levels of the stage + have hfold (p : ℕ) : readBit (classicalRun (stage base T (src s) s) y) p = + (List.range T).foldl (fun b i => b ^^ (decide (p = level base T (s + 1) i) && + (readBit y (level base T s i) ^^ (readBit y (src s) && readBit y (below base T s i)) ^^ + (readBit y (src s) && readBit y (level base T s i))))) (readBit y p) := by + rw [readBit_classicalRun_of_forall_notMem hcl hread, stage, List.foldl_flatMap] + refine List.foldl_ext _ _ _ fun b i _ => ?_ + simp only [List.foldl_cons, List.foldl_nil, List.all_cons, List.all_nil, Bool.and_true] + cases decide (p = level base T (s + 1) i) <;> simp + -- bits that the stage does not write + have hkeep (p : ℕ) (hp : ∀ i < T, p ≠ level base T (s + 1) i) : + readBit (classicalRun (stage base T (src s) s) y) p = readBit y p := by + rw [hfold, foldl_xor_range T T _ _ fun i hi _ => by simp [hp i hi]] + simp + have hlev_ge (i : ℕ) : base + 1 + s * T + T ≤ level base T (s + 1) i := by + unfold level + rw [Nat.add_mul, Nat.one_mul] + omega + refine ⟨fun p hp => ?_, ?_, fun i₀ hi₀ => ?_, fun p hp => ?_⟩ + · rw [hkeep p fun i _ => by have := hlev_ge i; omega, hlow p hp] + · rw [hkeep base fun i _ => by have := hlev_ge i; omega, hbase] + · have hne (i : ℕ) (hne : i ≠ i₀) : level base T (s + 1) i₀ ≠ level base T (s + 1) i := by + unfold level + omega + have hbelow : readBit y (below base T s i₀) = decide (i₀ ≤ count x src s) := by + unfold below + split_ifs with h0 + · subst h0 + simp [hbase] + · rw [hlev _ (by omega)] + exact decide_eq_decide.mpr (by omega) + rw [hfold, foldl_xor_range T i₀ _ _ fun i _ h => by simp [hne i h], + hhigh _ (by have := hlev_ge i₀; rw [Nat.add_mul, Nat.one_mul]; omega), + hlev i₀ hi₀, hlow _ hsrc, hbelow, count_succ] + simp only [hi₀, decide_true, Bool.true_and, Bool.false_xor] + cases hb : readBit x (src s) + · simp + · by_cases h1 : i₀ < count x src s <;> by_cases h2 : i₀ ≤ count x src s <;> + simp [h1, h2] + · have hp' : base + 1 + s * T + T + T ≤ p := by + simp only [Nat.add_mul, Nat.one_mul] at hp + omega + rw [hkeep p fun i hi => by unfold level; simp only [Nat.add_mul, Nat.one_mul]; omega, + hhigh p (by simp only [Nat.add_mul, Nat.one_mul]; omega)] + +/-- **The counter computes the threshold function**: started with zero ancillas from `base` on, it +leaves the qubits below `base` unchanged, and level `i` of stage `k` reads whether more than `i` of +the `k` input bits are one. -/ +theorem readBit_classicalRun_codes {base T k : ℕ} {src : ℕ → ℕ} (hsrc : ∀ s < k, src s < base) + (hN : base + 1 + (k + 1) * T ≤ N) (x : Fin N → Bool) + (hx : ∀ p, base ≤ p → readBit x p = false) : + (∀ p < base, readBit (classicalRun (codes base T src k) x) p = readBit x p) ∧ + ∀ i < T, readBit (classicalRun (codes base T src k) x) (level base T k i) = + decide (i < count x src k) := by + suffices h : ∀ s ≤ k, Invariant base T src x + (classicalRun ((List.range s).flatMap fun s => stage base T (src s) s) + (classicalStep (false, base, []) x)) s by + obtain ⟨h₁, -, h₃, -⟩ := h k le_rfl + exact ⟨h₁, h₃⟩ + intro s hs + induction s with + | zero => exact invariant_zero (by omega) x hx + | succ s ih => + rw [List.range_succ, List.flatMap_append, List.flatMap_singleton, classicalRun_append] + refine invariant_succ (hsrc s (by omega)) (le_trans ?_ hN) (ih (by omega)) + have : (s + 2) * T ≤ (k + 1) * T := Nat.mul_le_mul_right T (by omega) + omega + +end Cslib.Quantum.Counter diff --git a/Complexity/Computability/Circuit/Quantum/Parallel.lean b/Complexity/Computability/Circuit/Quantum/Parallel.lean new file mode 100644 index 000000000..41df21c32 --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/Parallel.lean @@ -0,0 +1,341 @@ +/- +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 + +/-! +# Circuits on parts of a larger register + +A circuit on `m` qubits runs on the qubits `e : Fin m ↪ Fin N` of a larger register +(`Cslib.Quantum.Circuit.mapWires`). Its entries are those of the small circuit on the qubits `e`, +provided the basis strings agree off `e` (`Cslib.Quantum.Circuit.matrix_mapWires`). Copies of one +circuit on pairwise disjoint sets of qubits act independently: an entry of the whole is the product +of the entries of the copies (`Cslib.Quantum.Circuit.matrix_flatMap_mapWires`). This is the tensor +product structure behind running independent copies of a quantum computation in parallel. + +For gate codes, shifting every qubit number by `o` (`Cslib.Quantum.GateCode.shift`) places the +circuit on the block of qubits `o, …, o + m - 1` (`Cslib.Quantum.Circuit.ofCodes_map_shift`). + +## Main definitions + +* `Cslib.Quantum.AgreeOff`: two basis strings agree off the range of an embedding. +* `Cslib.Quantum.glue`: a basis string with part of it replaced. +* `Cslib.Quantum.PlacedGate.mapWires`, `Cslib.Quantum.Circuit.mapWires`: running on a part of a + larger register. +* `Cslib.Quantum.GateCode.shift`, `Cslib.Quantum.blockEmb`: shifted gate codes and blocks of qubits. + +## Main results + +* `Cslib.Quantum.sum_agreeOff`: summing over the basis strings that agree with `x` off `e`. +* `Cslib.Quantum.Circuit.matrix_mapWires`: the entries of a circuit on part of a register. +* `Cslib.Quantum.Circuit.matrix_flatMap_mapWires`: copies on disjoint parts act independently. +* `Cslib.Quantum.Circuit.ofCodes_map_shift`: shifted gate codes denote a circuit on a block. +* `Cslib.Quantum.GateCode.WellFormed.shift`: shifted gate codes are well formed on a larger + register. +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Finset + +variable {ι : Type*} {m N : ℕ} + +/-! ### Agreeing off part of a register -/ + + +/-- The basis strings `y` and `x` **agree off** the qubits `e`. -/ +def AgreeOff (e : ι ↪ Fin N) (y x : Fin N → Bool) : Prop := + ∀ j, (∀ i, e i ≠ j) → y j = x j + +instance [Fintype ι] (e : ι ↪ Fin N) (y x : Fin N → Bool) : Decidable (AgreeOff e y x) := by + unfold AgreeOff; infer_instance + +theorem AgreeOff.refl (e : ι ↪ Fin N) (x : Fin N → Bool) : AgreeOff e x x := fun _ _ => rfl + +theorem AgreeOff.symm {e : ι ↪ Fin N} {y x : Fin N → Bool} (h : AgreeOff e y x) : + AgreeOff e x y := fun j hj => (h j hj).symm + +theorem AgreeOff.trans {e : ι ↪ Fin N} {z y x : Fin N → Bool} (h₁ : AgreeOff e z y) + (h₂ : AgreeOff e y x) : AgreeOff e z x := fun j hj => (h₁ j hj).trans (h₂ j hj) + +section Glue + +variable [Fintype ι] + +/-- The basis string `x` with the bits `z` on the qubits `e`. -/ +noncomputable def glue (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) : Fin N → Bool := + fun j => if h : ∃ i, e i = j then z h.choose else x j + +@[simp] theorem glue_apply_emb (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) (i : ι) : + glue e z x (e i) = z i := by + have h : ∃ i', e i' = e i := ⟨i, rfl⟩ + rw [glue, dite_eq_left h, e.injective h.choose_spec] + +theorem glue_of_not (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) {j : Fin N} + (hj : ∀ i, e i ≠ j) : glue e z x j = x j := by + rw [glue, dite_eq_right (by simpa using hj)] + +@[simp] theorem glue_comp (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) : + glue e z x ∘ e = z := + funext fun i => glue_apply_emb e z x i + +theorem agreeOff_glue (e : ι ↪ Fin N) (z : ι → Bool) (x : Fin N → Bool) : + AgreeOff e (glue e z x) x := fun _ hj => glue_of_not e z x hj + +theorem glue_comp_of_agreeOff {e : ι ↪ Fin N} {y x : Fin N → Bool} (h : AgreeOff e y x) : + glue e (y ∘ e) x = y := by + funext j + by_cases hj : ∃ i, e i = j + · obtain ⟨i, rfl⟩ := hj + simp + · push Not at hj + rw [glue_of_not e _ x hj, h j hj] + +/-- **Summing over the basis strings that agree with `x` off `e`** is summing over their bits on +`e`. -/ +theorem sum_agreeOff [DecidableEq ι] {R : Type*} [AddCommMonoid R] (e : ι ↪ Fin N) + (x : Fin N → Bool) (H : (Fin N → Bool) → R) : + ∑ y, (if AgreeOff e y x then H y else 0) = ∑ z : ι → Bool, H (glue e z x) := by + rw [← sum_filter] + refine sum_nbij' (· ∘ e) (glue e · x) (fun _ _ => mem_univ _) + (fun z _ => mem_filter.mpr ⟨mem_univ _, agreeOff_glue e z x⟩) + (fun y hy => glue_comp_of_agreeOff (mem_filter.mp hy).2) (fun z _ => glue_comp e z x) + (fun y hy => by rw [glue_comp_of_agreeOff (mem_filter.mp hy).2]) + +/-- Summing a function of the bits on `e` over the basis strings that agree with `x` off `e`. -/ +theorem sum_agreeOff_comp [DecidableEq ι] {R : Type*} [AddCommMonoid R] + (e : ι ↪ Fin N) (x : Fin N → Bool) (F : (ι → Bool) → R) : + ∑ y, (if AgreeOff e y x then F (y ∘ e) else 0) = ∑ z, F z := by + rw [sum_agreeOff e x fun y => F (y ∘ e)] + simp + +end Glue + +/-! ### Circuits on part of a register -/ + +/-- The placed gate `g` on the qubits `e` of a larger register. -/ +def PlacedGate.mapWires (e : Fin m ↪ Fin N) (g : PlacedGate m) : PlacedGate N := + ⟨g.arity, g.gate, g.wires.trans e⟩ + +/-- **The entries of a gate on part of a register** are those of the gate on the qubits `e`, when +the basis strings agree off `e`. -/ +theorem PlacedGate.matrix_mapWires (e : Fin m ↪ Fin N) (g : PlacedGate m) (y x : Fin N → Bool) : + ((g.mapWires e).matrix : Matrix _ _ ℂ) y x = + if AgreeOff e y x then (g.matrix : Matrix _ _ ℂ) (y ∘ e) (x ∘ e) else 0 := by + rw [matrix_apply, matrix_apply] + have hiff : (∀ j, (¬∃ i, (g.mapWires e).wires i = j) → y j = x j) ↔ + AgreeOff e y x ∧ ∀ j, (¬∃ i, g.wires i = j) → (y ∘ e) j = (x ∘ e) j := by + constructor + · intro h + refine ⟨fun j hj => h j ?_, fun j hj => h (e j) ?_⟩ + · rintro ⟨i, rfl⟩ + exact hj _ rfl + · rintro ⟨i, hi⟩ + exact hj ⟨i, e.injective hi⟩ + · rintro ⟨h₁, h₂⟩ j hj + by_cases hj' : ∃ j', e j' = j + · obtain ⟨j', rfl⟩ := hj' + exact h₂ j' fun ⟨i, hi⟩ => hj ⟨i, by rw [← hi]; rfl⟩ + · exact h₁ j fun i hi => hj' ⟨i, hi⟩ + rw [if_congr hiff rfl rfl, ite_and] + rfl + +/-- A circuit maps the basis state `|x⟩` to its column `x`. -/ +theorem Circuit.eval_ket_apply (C : Circuit m) (x y : Fin m → Bool) : + (Circuit.eval C (ket x)).ofLp y = (Circuit.matrix C : Matrix _ _ ℂ) y x := by + simp [Circuit.eval, Matrix.mulVec, dotProduct] + +/-- A circuit on `m` qubits with a list of gate codes; the codes of a concatenation of lists. -/ +theorem Circuit.ofCodes_flatMap {β : Type*} (l : List β) (f : β → List GateCode) : + Circuit.ofCodes m (l.flatMap f) = l.flatMap fun b => Circuit.ofCodes m (f b) := by + induction l with + | nil => rfl + | cons b l ih => rw [List.flatMap_cons, List.flatMap_cons, Circuit.ofCodes_append, ih] + +/-- The circuit `C` on the qubits `e` of a larger register. -/ +def Circuit.mapWires (e : Fin m ↪ Fin N) (C : Circuit m) : Circuit N := + C.map (PlacedGate.mapWires e) + +@[simp] theorem Circuit.mapWires_nil (e : Fin m ↪ Fin N) : Circuit.mapWires e [] = [] := rfl + +@[simp] theorem Circuit.mapWires_cons (e : Fin m ↪ Fin N) (g : PlacedGate m) (C : Circuit m) : + Circuit.mapWires e (g :: C) = g.mapWires e :: Circuit.mapWires e C := rfl + +/-- **The entries of a circuit on part of a register** are those of the circuit on the qubits `e`, +when the basis strings agree off `e`. -/ +theorem Circuit.matrix_mapWires (e : Fin m ↪ Fin N) (C : Circuit m) (y x : Fin N → Bool) : + (Circuit.matrix (Circuit.mapWires e C) : Matrix _ _ ℂ) y x = + if AgreeOff e y x then (Circuit.matrix C : Matrix _ _ ℂ) (y ∘ e) (x ∘ e) else 0 := by + induction C generalizing y x with + | nil => + simp only [mapWires_nil, matrix_nil, OneMemClass.coe_one, Matrix.one_apply] + by_cases hyx : y = x + · subst hyx + simp [AgreeOff.refl] + · rw [ite_eq_right hyx] + split_ifs with h h' + · exact absurd (by rw [← glue_comp_of_agreeOff h, h', glue_comp_of_agreeOff + (AgreeOff.refl e x)]) hyx + · rfl + · rfl + | cons g C ih => + simp only [mapWires_cons, matrix_cons, Submonoid.coe_mul, Matrix.mul_apply, ih, + PlacedGate.matrix_mapWires, ite_mul, zero_mul, mul_ite, mul_zero] + split_ifs with hyx + · have hiff (z : Fin N → Bool) : AgreeOff e y z ↔ AgreeOff e z x := + ⟨fun h => h.symm.trans hyx, fun h => hyx.trans h.symm⟩ + simp only [hiff, ← ite_and, and_self] + exact sum_agreeOff_comp e x fun w => (Circuit.matrix C : Matrix _ _ ℂ) (y ∘ e) w * + (g.matrix : Matrix _ _ ℂ) w (x ∘ e) + · refine sum_eq_zero fun z _ => ?_ + split_ifs with h₁ h₂ <;> first | rfl | exact absurd (h₂.trans h₁) hyx + +/-- **Copies of a circuit on disjoint parts of a register act independently**: an entry of the +whole is the product of the entries of the copies, when the basis strings agree off all parts. -/ +theorem Circuit.matrix_flatMap_mapWires (C : Circuit m) (L : List (Fin m ↪ Fin N)) + (hL : L.Pairwise fun e e' => ∀ i i', e i ≠ e' i') (y x : Fin N → Bool) : + (Circuit.matrix (L.flatMap (Circuit.mapWires · C)) : Matrix _ _ ℂ) y x = + if ∀ j, (∀ e ∈ L, ∀ i, e i ≠ j) → y j = x j then + (L.map fun e : Fin m ↪ Fin N => (Circuit.matrix C : Matrix _ _ ℂ) (y ∘ ⇑e) (x ∘ ⇑e)).prod + else 0 := by + induction L generalizing y x with + | nil => + simp only [List.flatMap_nil, matrix_nil, OneMemClass.coe_one, Matrix.one_apply, + List.not_mem_nil, IsEmpty.forall_iff, implies_true, forall_const, List.map_nil, + List.prod_nil, funext_iff] + | cons e L ih => + obtain ⟨he, hL⟩ := List.pairwise_cons.mp hL + rw [List.flatMap_cons, matrix_append, Submonoid.coe_mul, Matrix.mul_apply] + simp only [ih hL, matrix_mapWires, ite_mul, zero_mul, mul_ite, mul_zero, ← ite_and] + -- the only intermediate basis string is `y` on `e` and `x` elsewhere + set z₀ : Fin N → Bool := fun j => if ∃ i, e i = j then y j else x j + have hdisj (e' : Fin m ↪ Fin N) (he' : e' ∈ L) (i i' : Fin m) : e' i ≠ e i' := + fun h => he e' he' i' i h.symm + rw [sum_eq_single z₀] + · have hz₀e : z₀ ∘ e = y ∘ e := funext fun i => ite_eq_left ⟨i, rfl⟩ + have hz₀x : AgreeOff e z₀ x := fun j hj => ite_eq_right (by simpa using hj) + have hz₀L (e' : Fin m ↪ Fin N) (he' : e' ∈ L) : z₀ ∘ e' = x ∘ e' := + funext fun i => ite_eq_right fun ⟨i', hi'⟩ => hdisj e' he' i i' hi'.symm + have hcond : (∀ j, (∀ e' ∈ L, ∀ i, e' i ≠ j) → y j = z₀ j) ↔ + ∀ j, (∀ e' ∈ e :: L, ∀ i, e' i ≠ j) → y j = x j := by + constructor + · intro h j hj + have := h j fun e' he' => hj e' (List.mem_cons_of_mem _ he') + rwa [show z₀ j = x j from + ite_eq_right (by simpa using fun i => hj e (List.mem_cons_self ..) i)] at this + · intro h j hj + by_cases hj' : ∃ i, e i = j + · exact (ite_eq_left hj').symm + · rw [show z₀ j = x j from ite_eq_right hj'] + refine h j fun e' he' => ?_ + rcases List.mem_cons.mp he' with rfl | he' + · simpa using hj' + · exact hj e' he' + simp only [hz₀x, true_and, hcond, hz₀e, List.map_cons, List.prod_cons] + split_ifs + · rw [List.map_congr_left fun e' he' => by rw [hz₀L e' he'], mul_comm] + · rfl + · intro z _ hz + refine ite_eq_right fun ⟨h₁, h₂⟩ => hz (funext fun j => ?_) + by_cases hj : ∃ i, e i = j + · rw [show z₀ j = y j from ite_eq_left hj] + obtain ⟨i, rfl⟩ := hj + exact (h₂ (e i) fun e' he' i' => hdisj e' he' i' i).symm + · rw [show z₀ j = x j from ite_eq_right hj] + exact h₁ j (by simpa using hj) + · exact fun h => absurd (mem_univ _) h + +/-! ### Shifted gate codes -/ + +/-- The gate code `g` with every qubit number increased by `o`. -/ +def GateCode.shift (o : ℕ) (g : GateCode) : GateCode := (g.1, g.2.1 + o, g.2.2.map (· + o)) + +/-- The block of qubits `o, …, o + m - 1` of an `N`-qubit register. -/ +def blockEmb (o : ℕ) (h : o + m ≤ N) : Fin m ↪ Fin N := + ⟨fun i => ⟨i + o, by omega⟩, fun i j hij => Fin.ext (by simpa using congrArg Fin.val hij)⟩ + +@[simp] theorem blockEmb_apply_val (o : ℕ) (h : o + m ≤ N) (i : Fin m) : + (blockEmb o h i : ℕ) = i + o := rfl + +/-- **A shifted well-formed gate code denotes the gate on the shifted block.** -/ +theorem GateCode.toPlacedGate?_shift {o : ℕ} (h : o + m ≤ N) {g : GateCode} + (hg : WellFormed m g) : + toPlacedGate? N (g.shift o) = (toPlacedGate? m g).map (PlacedGate.mapWires (blockEmb o h)) := by + have key {k : ℕ} (U : Gate k) (A : Fin k ↪ Fin m) (A' : Fin k ↪ Fin N) + (hA : ∀ i, (A' i : ℕ) = A i + o) : + (⟨k, U, A'⟩ : PlacedGate N) = PlacedGate.mapWires (blockEmb o h) ⟨k, U, A⟩ := by + simp only [PlacedGate.mapWires, PlacedGate.mk.injEq, heq_eq_eq, true_and] + exact Function.Embedding.ext fun i => Fin.ext (hA i) + match g, hg with + | (true, t, []), hg => + have ht : t < m := hg.1 + simp only [shift, toPlacedGate?, ht, ↓reduceDIte, show t + o < N by omega, Option.map_some, + List.map_nil, Option.some.injEq] + exact key _ _ _ fun i => by fin_cases i; rfl + | (true, t, _ :: _), hg => exact absurd hg.2 (List.cons_ne_nil _ _) + | (false, t, []), hg => + have ht : t < m := hg.2.2 t (List.mem_cons_self ..) + simp only [shift, toPlacedGate?, ht, ↓reduceDIte, show t + o < N by omega, Option.map_some, + List.map_nil, Option.some.injEq] + exact key _ _ _ fun i => by fin_cases i; rfl + | (false, t, [c]), hg => + obtain ⟨-, hnd, hlt⟩ := hg + have ht : t < m := hlt t (by simp) + have hc : c < m := hlt c (by simp) + have hct : c ≠ t := by simp at hnd; omega + simp only [shift, toPlacedGate?, List.map_cons, List.map_nil, + dite_eq_left (show c < m ∧ t < m ∧ c ≠ t from ⟨hc, ht, hct⟩), + dite_eq_left (show c + o < N ∧ t + o < N ∧ c + o ≠ t + o by omega), Option.map_some, + Option.some.injEq] + exact key _ _ _ fun i => by fin_cases i <;> rfl + | (false, t, [c₁, c₂]), hg => + obtain ⟨-, hnd, hlt⟩ := hg + have ht : t < m := hlt t (by simp) + have hc₁ : c₁ < m := hlt c₁ (by simp) + have hc₂ : c₂ < m := hlt c₂ (by simp) + simp only [List.nodup_cons, List.mem_cons, List.not_mem_nil, or_false, List.nodup_nil, + not_false_eq_true, and_true] at hnd + simp only [shift, toPlacedGate?, List.map_cons, List.map_nil, + dite_eq_left (show c₁ < m ∧ c₂ < m ∧ t < m ∧ c₁ ≠ c₂ ∧ c₁ ≠ t ∧ c₂ ≠ t by omega), + dite_eq_left (show c₁ + o < N ∧ c₂ + o < N ∧ t + o < N ∧ c₁ + o ≠ c₂ + o ∧ c₁ + o ≠ t + o ∧ + c₂ + o ≠ t + o by omega), Option.map_some, Option.some.injEq] + exact key _ _ _ fun i => by fin_cases i <;> rfl + | (false, t, _ :: _ :: _ :: _), hg => exact absurd hg.1 (by simp) + +/-- A well-formed gate code, shifted by `o`, is well formed on a register of at least `o + m` +qubits. -/ +theorem GateCode.WellFormed.shift {o : ℕ} (h : o + m ≤ N) {g : GateCode} (hg : WellFormed m g) : + WellFormed N (g.shift o) := by + obtain ⟨_ | _, t, cs⟩ := g + · obtain ⟨hlen, hnd, hlt⟩ := hg + refine ⟨by simpa [GateCode.shift] using hlen, ?_, ?_⟩ + · simpa [GateCode.shift, List.map_cons] using + hnd.map (f := (· + o)) (fun a b hab => by simpa using hab) + · intro i hi + simp only [List.mem_cons, List.mem_map] at hi + rcases hi with rfl | ⟨c, hc, rfl⟩ + · have := hlt t (List.mem_cons_self ..) + omega + · have := hlt c (List.mem_cons_of_mem _ hc) + omega + · obtain ⟨ht, rfl⟩ := hg + exact ⟨show t + o < N by omega, rfl⟩ + +/-- **Shifted gate codes denote the circuit on a block**: shifting a well-formed circuit's qubit +numbers by `o` runs it on the qubits `o, …, o + m - 1`. -/ +theorem Circuit.ofCodes_map_shift {o : ℕ} (h : o + m ≤ N) {gs : List GateCode} + (hgs : ∀ g ∈ gs, GateCode.WellFormed m g) : + Circuit.ofCodes N (gs.map (GateCode.shift o)) = + (Circuit.ofCodes m gs).mapWires (blockEmb o h) := by + simp only [ofCodes, mapWires, List.filterMap_map, List.map_filterMap] + exact List.filterMap_congr fun g hg => GateCode.toPlacedGate?_shift h (hgs g hg) + +end Cslib.Quantum diff --git a/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean b/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean new file mode 100644 index 000000000..804d03a26 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean @@ -0,0 +1,642 @@ +/- +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.Counter +public import Complexity.Computability.Circuit.Quantum.Parallel +import Complexity.Foundations.Combinatorics.MajorityVote.Weighted +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat + +/-! +# Error reduction for `BQP` + +The error `1 / 3` in the definition of `BQP` (`Cslib.Complexity.BQP`) can be made exponentially +small: `A ∈ BQP enc` exactly when for every polynomial `q` some uniform family accepts members with +probability at least `1 - 2^{-q(n)}` and other instances with probability at most `2^{-q(n)}`, where +`n` is the length of the encoded instance (`Cslib.Complexity.mem_BQP_iff_forall_errorExponent`). + +This is the majority-vote error reduction of `BPP` +(`Cslib.Complexity.mem_BPP_iff_forall_decidesWithErrorExponent`), carried out inside a quantum +circuit, since acceptance is the measurement of a single qubit at the end. The amplified family +(`Cslib.Quantum.UniformCircuitFamily.amplify`) runs `2 r` copies of the circuit side by side and +takes a reversible majority vote of their answers. On inputs of length `n` its register holds the +input, `2 r` blocks of the original width `w`, and the ancillas of a threshold counter: + +1. CNOT gates copy the input into each block (`Cslib.Quantum.Amplify.copyCodes`); +2. each block runs the original circuit, with its qubit numbers shifted + (`Cslib.Quantum.Amplify.copiesCodes`); +3. a reversible counter computes whether more than `r` of the blocks' first qubits are one + (`Cslib.Quantum.Counter.codes`); +4. three CNOT gates swap that answer into qubit `0` (`Cslib.Quantum.Amplify.swapCodes`). + +The copies act on disjoint blocks, so their measurement outcomes are independent +(`Cslib.Quantum.Circuit.matrix_flatMap_mapWires`), and the classical steps permute the outcomes. The +acceptance probability of the amplified family is therefore the probability that a strict majority +of `2 r` independent trials succeed, each with the original acceptance probability +(`Cslib.Quantum.UniformCircuitFamily.acceptProb_amplify`). The exponential-moment bound +`Cslib.sum_prod_le_of_card_filter_le` makes the error at most `(8 / 9) ^ r`, and `r = 6 q` gives +`2^{-q}`. + +## Main definitions + +* `Cslib.Quantum.Amplify.codes`, `Cslib.Quantum.Amplify.width`: the amplified circuit. +* `Cslib.Quantum.UniformCircuitFamily.amplify`: the amplified family. + +## Main results + +* `Cslib.Quantum.UniformCircuitFamily.acceptProb_amplify`: the acceptance probability of the + amplified family is that of a strict majority of independent copies. +* `Cslib.Complexity.mem_BQP_iff_forall_errorExponent`: error reduction for `BQP`. + +The argument is the standard one; no source locator is claimed for it. `BQP` itself follows +[Bernstein, Vazirani][BernsteinVazirani1997] and [Arora, Barak][AroraBarak09] (see +`Cslib.Complexity.BQP`). + +## References + +* [E. Bernstein, U. Vazirani, *Quantum complexity theory*][BernsteinVazirani1997] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Finset GateCode Turing.MultiTapeTM + +namespace Amplify + +/-- CNOT gates copying the first `n` qubits into the blocks `1, …, k` of width `w`. -/ +def copyCodes (n w k : ℕ) : List GateCode := + (List.range k).flatMap fun j => (List.range n).map fun i => (false, i + (j + 1) * w, [i]) + +/-- The circuit `gs` on each of the blocks `1, …, k` of width `w`. -/ +def copiesCodes (w k : ℕ) (gs : List GateCode) : List GateCode := + (List.range k).flatMap fun j => gs.map (shift ((j + 1) * w)) + +/-- Three CNOT gates swapping qubit `a` into qubit `0`. -/ +def swapCodes (a : ℕ) : List GateCode := [(false, 0, [a]), (false, a, [0]), (false, 0, [a])] + +/-- The first ancilla of the counter, after the input block and `2 r` copies of width `w`. -/ +def base (w r : ℕ) : ℕ := (2 * r + 1) * w + +/-- The register width of the amplified circuit: the blocks and the counter's ancillas. -/ +def width (w r : ℕ) : ℕ := base w r + 1 + (2 * r + 1) * (r + 1) + +/-- The counter's qubit that reads whether more than `r` of the `2 r` copies accept. -/ +def answer (w r : ℕ) : ℕ := Counter.level (base w r) (r + 1) (2 * r) r + +/-- **The amplified circuit**: copy the input of length `n` into `2 r` blocks of width `w`, run +the circuit `gs` on each, count the blocks whose first qubit is one, and swap the strict majority +into qubit `0`. -/ +def codes (n w r : ℕ) (gs : List GateCode) : List GateCode := + copyCodes n w (2 * r) ++ (copiesCodes w (2 * r) gs ++ + (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++ swapCodes (answer w r))) + +variable {n w r : ℕ} + +theorem base_eq (w r : ℕ) : base w r = 2 * r * w + w := by + unfold base + rw [Nat.add_mul, Nat.one_mul] + +theorem block_lt {j i : ℕ} (hj : j < 2 * r) (hi : i < w) : + i + (j + 1) * w < base w r := by + have := Nat.mul_le_mul_right w (show j + 1 ≤ 2 * r by omega) + rw [base_eq] + omega + +theorem base_lt_width : base w r < width w r := by + unfold width + omega + +theorem answer_lt_width : answer w r < width w r := by + unfold answer width Counter.level + have : 2 * r * (r + 1) + r < (2 * r + 1) * (r + 1) := by + rw [Nat.add_mul (2 * r), Nat.one_mul] + omega + omega + +theorem base_le_answer : base w r ≤ answer w r := by + unfold answer Counter.level + omega + +/-- The blocks `1, …, 2 r` of the amplified register. -/ +def blocks (w r : ℕ) : Fin (2 * r) × Fin w ↪ Fin (width w r) where + toFun p := ⟨p.2 + (p.1 + 1) * w, (block_lt p.1.2 p.2.2).trans base_lt_width⟩ + inj' p p' h := by + have h' : (p.2 : ℕ) + (p.1 + 1) * w = p'.2 + (p'.1 + 1) * w := congrArg Fin.val h + have hw : 0 < w := Nat.lt_of_le_of_lt (Nat.zero_le _) p.2.2 + have hmod := congrArg (· % w) h' + have hdiv := congrArg (· / w) h' + simp only [Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt p.2.2, + Nat.mod_eq_of_lt p'.2.2] at hmod + simp only [Nat.add_mul_div_right _ _ hw, Nat.div_eq_of_lt p.2.2, + Nat.div_eq_of_lt p'.2.2] at hdiv + exact Prod.ext (Fin.ext (by omega)) (Fin.ext hmod) + +@[simp] theorem blocks_apply_val (p : Fin (2 * r) × Fin w) : + (blocks w r p : ℕ) = p.2 + (p.1 + 1) * w := rfl + +theorem block_le_width {j : ℕ} (hj : j < 2 * r) : (j + 1) * w + w ≤ width w r := by + have := Nat.mul_le_mul_right w (show j + 1 ≤ 2 * r by omega) + have : base w r < width w r := base_lt_width + rw [base_eq] at this + omega + +/-- Block `j` of the amplified register. -/ +def block (j : Fin (2 * r)) : Fin w ↪ Fin (width w r) := + blockEmb ((j + 1) * w) (block_le_width j.2) + +theorem block_apply (j : Fin (2 * r)) (i : Fin w) : block j i = blocks w r (j, i) := rfl + +/-! ### The classical steps -/ + +theorem isClassical_copyCodes (hn : n ≤ w) (hw : 0 < w) : + IsClassical (width w r) (copyCodes n w (2 * r)) := by + refine IsClassical.flatMap fun j hj => fun g hg => ?_ + obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hg + have hj : j < 2 * r := List.mem_range.mp hj + have hi : i < n := List.mem_range.mp hi + have hlt := (block_lt (r := r) hj (show i < w by omega)).trans base_lt_width + have : 0 < (j + 1) * w := Nat.mul_pos (by omega) hw + refine ⟨rfl, by simp, ?_, ?_⟩ + · simp only [List.nodup_cons, List.mem_cons, List.not_mem_nil, or_false, List.nodup_nil, + not_false_eq_true, and_true] + omega + · simp only [List.mem_cons, List.not_mem_nil, or_false, forall_eq_or_imp, forall_eq] + omega + +/-- **The copy step puts the input in every block**, and leaves the other qubits unchanged. -/ +theorem readBit_classicalRun_copyCodes (hn : n ≤ w) (hw : 0 < w) (X : Fin (width w r) → Bool) + (hX : ∀ p, n ≤ p → readBit X p = false) (p : ℕ) : + readBit (classicalRun (copyCodes n w (2 * r)) X) p = + if ∃ j < 2 * r, ∃ i < w, p = i + (j + 1) * w then readBit X (p % w) else readBit X p := by + have hread : ∀ g ∈ copyCodes n w (2 * r), ∀ g' ∈ copyCodes n w (2 * r), g.2.1 ∉ g'.2.2 := by + intro g hg g' hg' + simp only [copyCodes, List.mem_flatMap, List.mem_map, List.mem_range] at hg hg' + obtain ⟨j, hj, i, hi, rfl⟩ := hg + obtain ⟨j', hj', i', hi', rfl⟩ := hg' + have : w ≤ (j + 1) * w := Nat.le_mul_of_pos_left w (by omega) + simp only [List.mem_cons, List.not_mem_nil, or_false] + omega + rw [readBit_classicalRun_of_forall_notMem (isClassical_copyCodes hn hw) hread, copyCodes, + List.foldl_flatMap] + -- each block contributes the exclusive or of its copies of the input bits + have hinner (b : Bool) (j : ℕ) : + ((List.range n).map fun i => ((false, i + (j + 1) * w, [i]) : GateCode)).foldl + (fun b g => b ^^ (decide (p = g.2.1) && g.2.2.all (readBit X))) b = + (b ^^ (decide (∃ i < n, p = i + (j + 1) * w) && readBit X (p % w))) := by + rw [List.foldl_map] + by_cases hp : ∃ i < n, p = i + (j + 1) * w + · obtain ⟨i₀, hi₀, rfl⟩ := hp + rw [foldl_xor_range n i₀ _ _ fun i _ hne => by simp [Ne.symm hne]] + simp [hi₀, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (show i₀ < w by omega)] + · have hp' : ∀ i < n, p ≠ i + (j + 1) * w := fun i hi h => hp ⟨i, hi, h⟩ + rw [foldl_xor_range n n _ _ fun i hi _ => by simp [hp' i hi]] + simp [hp] + simp only [hinner] + by_cases hp : ∃ j < 2 * r, ∃ i < w, p = i + (j + 1) * w + · obtain ⟨j₀, hj₀, i₀, hi₀, rfl⟩ := hp + rw [ite_eq_left ⟨j₀, hj₀, i₀, hi₀, rfl⟩, foldl_xor_range (2 * r) j₀ _ _ fun j _ hne => ?_] + · have hw' : w ≤ (j₀ + 1) * w := Nat.le_mul_of_pos_left w (by omega) + rw [hX _ (by omega), Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt hi₀] + by_cases hi : i₀ < n + · simp [hj₀, hi] + · simp [hj₀, hi, hX i₀ (by omega)] + · simp only [Bool.and_eq_false_iff, decide_eq_false_iff_not] + left + rintro ⟨i, hi, h⟩ + have hmod := congrArg (· / w) h + simp only [Nat.add_mul_div_right _ _ hw, Nat.div_eq_of_lt hi₀, + Nat.div_eq_of_lt (show i < w by omega)] at hmod + omega + · rw [ite_eq_right hp, foldl_xor_range (2 * r) (2 * r) _ _ fun j hj _ => ?_] + · simp + · simp only [Bool.and_eq_false_iff, decide_eq_false_iff_not] + exact Or.inl fun ⟨i, hi, h⟩ => hp ⟨j, hj, i, by omega, h⟩ + +theorem isClassical_swapCodes {N a : ℕ} (ha : 0 < a) (hN : a < N) : + IsClassical N (swapCodes a) := by + have h₀ : WellFormed N ((false, 0, [a]) : GateCode) := + ⟨by simp, by simp; omega, by simp; omega⟩ + have h₁ : WellFormed N ((false, a, [0]) : GateCode) := + ⟨by simp, by simp; omega, by simp; omega⟩ + intro g hg + simp only [swapCodes, List.mem_cons, List.not_mem_nil, or_false] at hg + rcases hg with rfl | rfl | rfl + · exact ⟨rfl, h₀⟩ + · exact ⟨rfl, h₁⟩ + · exact ⟨rfl, h₀⟩ + +/-- **The swap moves qubit `a` into qubit `0`.** -/ +theorem readBit_classicalRun_swapCodes {N a : ℕ} (ha : 0 < a) (hN : a < N) (X : Fin N → Bool) : + readBit (classicalRun (swapCodes a) X) 0 = readBit X a := by + simp only [swapCodes, classicalRun_cons, classicalRun_nil, readBit_classicalStep, + List.all_cons, List.all_nil, Bool.and_true] + have h0 : (0 : ℕ) < N := by omega + simp [h0, hN, show a ≠ 0 by omega, show (0 : ℕ) ≠ a by omega] + +theorem isClassical_counter_swap (hw : 0 < w) : + IsClassical (width w r) (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++ + swapCodes (answer w r)) := by + refine IsClassical.append.mpr ⟨Counter.isClassical_codes (fun s hs => ?_) le_rfl, + isClassical_swapCodes ?_ answer_lt_width⟩ + · have := block_lt (r := r) hs hw + omega + · have : 0 < base w r := Nat.mul_pos (by omega) hw + have := base_le_answer (w := w) (r := r) + omega + +/-- **The classical steps accept by strict majority**: on a register whose qubits from the counter +on are zero, the counter and the swap leave in qubit `0` whether more than `r` of the blocks' first +qubits are one. -/ +theorem readBit_classicalRun_counter_swap (hw : 0 < w) (Y : Fin (width w r) → Bool) + (hY : ∀ p, base w r ≤ p → readBit Y p = false) : + readBit (classicalRun (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++ + swapCodes (answer w r)) Y) 0 = + decide (r < Counter.count Y (fun s => (s + 1) * w) (2 * r)) := by + rw [classicalRun_append, readBit_classicalRun_swapCodes _ answer_lt_width] + · exact (Counter.readBit_classicalRun_codes (fun s hs => by + have := block_lt (r := r) hs hw; omega) le_rfl Y hY).2 r (by omega) + · have : 0 < base w r := Nat.mul_pos (by omega) hw + have := base_le_answer (w := w) (r := r) + omega + +/-! ### The parallel copies -/ + +theorem ofCodes_copiesCodes {gs : List GateCode} (hgs : ∀ g ∈ gs, WellFormed w g) : + Circuit.ofCodes (width w r) (copiesCodes w (2 * r) gs) = + ((List.finRange (2 * r)).map block).flatMap (Circuit.mapWires · (Circuit.ofCodes w gs)) := by + rw [copiesCodes, Circuit.ofCodes_flatMap, ← List.map_coe_finRange_eq_range, List.flatMap_map, + List.flatMap_map] + congr 1 + funext j + exact Circuit.ofCodes_map_shift _ hgs + +theorem pairwise_block : + ((List.finRange (2 * r)).map (block (w := w))).Pairwise fun e e' => ∀ i i', e i ≠ e' i' := by + rw [List.pairwise_map] + refine (List.nodup_finRange _).imp fun {j j'} hjj' i i' h => hjj' ?_ + rw [block_apply, block_apply] at h + exact congrArg Prod.fst ((blocks w r).injective h) + +end Amplify + +/-! ### Acceptance probability of the amplified circuit -/ + +/-- Grouping a sum over tuples by a function of their entries. -/ +private theorem sum_mul_prod_fiberwise {α κ R : Type*} [Fintype α] [Fintype κ] [DecidableEq κ] + [CommSemiring R] {k : ℕ} (φ : α → κ) (f : α → R) (G : (Fin k → κ) → R) : + ∑ y : Fin k → α, G (fun j => φ (y j)) * ∏ j, f (y j) = + ∑ b : Fin k → κ, G b * ∏ j, ∑ z ∈ univ.filter (fun z => φ z = b j), f z := by + simp_rw [prod_univ_sum, mul_sum] + rw [← sum_fiberwise univ (fun y : Fin k → α => fun j => φ (y j))] + refine sum_congr rfl fun b _ => ?_ + have hset : Fintype.piFinset (fun j => univ.filter fun z => φ z = b j) = + univ.filter fun y : Fin k → α => (fun j => φ (y j)) = b := by + ext y + simp [Fintype.mem_piFinset, funext_iff] + rw [hset] + refine sum_congr rfl fun y hy => ?_ + rw [(mem_filter.mp hy).2] + +open Amplify in +/-- **The acceptance probability of the amplified circuit** is the probability that more than `r` +of `2 r` independent runs of the original circuit accept. -/ +theorem acceptProb_amplify_codes {n w r : ℕ} {gs : List GateCode} (hw : 0 < w) (hn : n ≤ w) + (hgs : ∀ g ∈ gs, WellFormed w g) (x : List Bool) (hx : x.length = n) : + acceptProb (width w r) (codes n w r gs) x = + ∑ b : Fin (2 * r) → Bool with r < (univ.filter fun j => b j = true).card, + ∏ j, if b j then acceptProb w gs x else 1 - acceptProb w gs x := by + set N := width w r + set C := Circuit.ofCodes w gs + set a : (Fin w → Bool) → ℂ := fun z => (Circuit.run C (inputState w x)).ofLp z + set X := classicalRun (copyCodes n w (2 * r)) (inputState N x) with hXdef + have hgetD (p : ℕ) (hp : n ≤ p) : x.getD p false = false := by + rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)] + rfl + have hX₀ (p : ℕ) : readBit (inputState N x) p = x.getD p false := by + by_cases hp : p < N + · rw [readBit_of_lt _ hp] + rfl + · rw [readBit_of_le _ (not_lt.mp hp), hgetD] + have := (base_lt_width (w := w) (r := r)) + have : w ≤ base w r := by unfold base; exact Nat.le_mul_of_pos_left w (by omega) + omega + have hXbit (p : ℕ) := readBit_classicalRun_copyCodes (r := r) hn hw (inputState N x) + (fun p hp => by rw [hX₀, hgetD p hp]) p + -- the copy step puts the input in every block and keeps zeros from the counter on + have hXblock (j : Fin (2 * r)) : X ∘ block j = inputState w x := by + funext i + have h := hXbit (i + (j + 1) * w) + rw [ite_eq_left ⟨j, j.2, i, i.2, rfl⟩, Nat.add_mul_mod_self_right, + Nat.mod_eq_of_lt i.2, hX₀] at h + rw [Function.comp_apply, show X (block j i) = readBit X (block j i) from + (readBit_fin _ _).symm, block_apply, blocks_apply_val, h] + rfl + have hXhigh (p : ℕ) (hp : base w r ≤ p) : readBit X p = false := by + rw [hXbit, ite_eq_right, hX₀, hgetD] + · have : w ≤ base w r := by unfold base; exact Nat.le_mul_of_pos_left w (by omega) + omega + · rintro ⟨j, hj, i, hi, rfl⟩ + exact absurd hp (not_le.mpr (block_lt hj hi)) + -- the amplitudes of the copies are products + have hamp (Y : Fin N → Bool) : + (Circuit.eval (Circuit.ofCodes N (copiesCodes w (2 * r) gs)) (ket X)).ofLp Y = + if AgreeOff (blocks w r) Y X then ∏ j, a (Y ∘ block j) else 0 := by + rw [Circuit.eval_ket_apply, ofCodes_copiesCodes hgs, + Circuit.matrix_flatMap_mapWires _ _ pairwise_block] + have hcond : (∀ p, (∀ e ∈ (List.finRange (2 * r)).map block, ∀ i, e i ≠ p) → Y p = X p) ↔ + AgreeOff (blocks w r) Y X := by + simp only [List.mem_map, List.mem_finRange, true_and, forall_exists_index, + forall_apply_eq_imp_iff, AgreeOff, Prod.forall, block_apply] + rw [if_congr hcond rfl rfl, List.map_map, ← Fin.prod_univ_def] + refine if_congr Iff.rfl (prod_congr rfl fun j _ => ?_) rfl + simp only [Function.comp_apply, hXblock, a, Circuit.run, Circuit.eval_ket_apply] + rfl + -- the acceptance probability as a sum over the blocks' outcomes + unfold acceptProb + rw [codes, Circuit.ofCodes_append, Circuit.ofCodes_append, Circuit.run, Circuit.eval_append, + Circuit.eval_append, Circuit.eval_ofCodes_ket (isClassical_copyCodes hn hw), + Circuit.measureProb_eval_ofCodes (isClassical_counter_swap hw), ← hXdef] + simp only [hamp] + have hterm (Y : Fin N → Bool) : + (if classicalRun (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++ + swapCodes (answer w r)) Y ∈ accepting N then + ‖(if AgreeOff (blocks w r) Y X then ∏ j, a (Y ∘ block j) else 0)‖ ^ 2 else 0) = + if AgreeOff (blocks w r) Y X then + (if r < (univ.filter fun j : Fin (2 * r) => (Y ∘ blocks w r) (j, ⟨0, hw⟩) = true).card + then (1 : ℝ) else 0) * ∏ j, ‖a (fun i => (Y ∘ blocks w r) (j, i))‖ ^ 2 + else 0 := by + by_cases hY : AgreeOff (blocks w r) Y X + · have hYhigh (p : ℕ) (hp : base w r ≤ p) : readBit Y p = false := by + rw [← hXhigh p hp] + by_cases hpN : p < N + · rw [readBit_of_lt _ hpN, readBit_of_lt _ hpN] + refine hY _ fun q h => ?_ + have := congrArg Fin.val h + simp only [blocks_apply_val] at this + exact absurd hp (not_le.mpr (this ▸ block_lt q.1.2 q.2.2)) + · rw [readBit_of_le _ (not_lt.mp hpN), readBit_of_le _ (not_lt.mp hpN)] + have hbit (j : Fin (2 * r)) : readBit Y ((j + 1) * w) = (Y ∘ blocks w r) (j, ⟨0, hw⟩) := by + rw [Function.comp_apply, ← readBit_fin Y (blocks w r (j, ⟨0, hw⟩)), blocks_apply_val] + simp only [Nat.zero_add] + have hcount : Counter.count Y (fun s => (s + 1) * w) (2 * r) = + (univ.filter fun j : Fin (2 * r) => (Y ∘ blocks w r) (j, ⟨0, hw⟩) = true).card := by + unfold Counter.count + rw [← card_map Fin.valEmbedding] + congr 1 + ext s + simp only [mem_filter, mem_range, mem_map, mem_univ, true_and, Fin.valEmbedding_apply, + Function.comp_apply] + constructor + · rintro ⟨hs, h⟩ + exact ⟨⟨s, hs⟩, (hbit ⟨s, hs⟩).symm.trans h, rfl⟩ + · rintro ⟨j, h, rfl⟩ + exact ⟨j.2, (hbit j).trans h⟩ + have hacc : (classicalRun (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++ + swapCodes (answer w r)) Y ∈ accepting N) ↔ + r < (univ.filter fun j : Fin (2 * r) => (Y ∘ blocks w r) (j, ⟨0, hw⟩) = true).card := by + have h0 : 0 < N := by have := base_lt_width (w := w) (r := r); omega + rw [mem_accepting h0, ← readBit_fin (classicalRun _ Y) (⟨0, h0⟩ : Fin N)] + change readBit _ 0 = true ↔ _ + rw [readBit_classicalRun_counter_swap hw Y hYhigh, hcount, decide_eq_true_iff] + simp only [hY, ite_true, hacc, norm_prod, ← prod_pow] + split_ifs <;> simp [block_apply, Function.comp_def] + · simp [hY] + simp only [hterm] + rw [sum_agreeOff_comp (blocks w r) X fun z => + (if r < (univ.filter fun j : Fin (2 * r) => z (j, ⟨0, hw⟩) = true).card then (1 : ℝ) else 0) * + ∏ j, ‖a (fun i => z (j, i))‖ ^ 2] + rw [Fintype.sum_equiv (Equiv.curry (Fin (2 * r)) (Fin w) Bool) (fun z => + (if r < (univ.filter fun j => z (j, ⟨0, hw⟩) = true).card then (1 : ℝ) else 0) * + ∏ j, ‖a (fun i => z (j, i))‖ ^ 2) (fun y => + (if r < (univ.filter fun j => y j ⟨0, hw⟩ = true).card then (1 : ℝ) else 0) * + ∏ j, ‖a (y j)‖ ^ 2) fun z => rfl] + refine (sum_mul_prod_fiberwise (fun z : Fin w → Bool => z ⟨0, hw⟩) (fun z => ‖a z‖ ^ 2) + fun b => if r < (univ.filter fun j => b j = true).card then (1 : ℝ) else 0).trans ?_ + -- the outcome probabilities of one copy + have hone : ∑ z, ‖a z‖ ^ 2 = 1 := by + rw [← measureProb, measureProb_univ, Circuit.norm_run, one_pow] + have htrue : ∑ z ∈ univ.filter (fun z : Fin w → Bool => z ⟨0, hw⟩ = true), ‖a z‖ ^ 2 = + acceptProb w gs x := by + unfold acceptProb measureProb + congr 1 + ext z + simp [mem_accepting hw] + have hfalse : ∑ z ∈ univ.filter (fun z : Fin w → Bool => z ⟨0, hw⟩ = false), ‖a z‖ ^ 2 = + 1 - acceptProb w gs x := by + rw [← hone, ← htrue, ← sum_filter_add_sum_filter_not univ (fun z : Fin w → Bool => + z ⟨0, hw⟩ = true)] + simp + rw [sum_filter] + refine sum_congr rfl fun b _ => ?_ + rw [ite_mul, one_mul, zero_mul] + refine if_congr Iff.rfl (prod_congr rfl fun j _ => ?_) rfl + cases b j + · exact hfalse + · exact htrue + +namespace Amplify + +/-! ### The amplified circuit is constructed in polynomial time -/ + +variable {γ : Type} {enc : γ ↪ List Bool} + +theorem computableInPolyTime_copyCodes {n w k : γ → ℕ} + (hn : ComputableInPolyTime n enc encUnary) (hw : ComputableInPolyTime w enc encUnary) + (hk : ComputableInPolyTime k enc encUnary) : + ComputableInPolyTime (fun c => copyCodes (n c) (w c) (k c)) enc (encList encGateCode) := by + unfold copyCodes + fun_prop + +theorem computableInPolyTime_copiesCodes {w k : γ → ℕ} {gs : γ → List GateCode} + (hw : ComputableInPolyTime w enc encUnary) (hk : ComputableInPolyTime k enc encUnary) + (hgs : ComputableInPolyTime gs enc (encList encGateCode)) : + ComputableInPolyTime (fun c => copiesCodes (w c) (k c) (gs c)) enc (encList encGateCode) := by + have hshift (o : ℕ) : shift o = fun g => (g.1, g.2.1 + o, g.2.2.map (· + o)) := rfl + simp only [copiesCodes, hshift] + fun_prop + +theorem computableInPolyTime_stage {base T b s : γ → ℕ} + (hbase : ComputableInPolyTime base enc encUnary) (hT : ComputableInPolyTime T enc encUnary) + (hb : ComputableInPolyTime b enc encUnary) (hs : ComputableInPolyTime s enc encUnary) : + ComputableInPolyTime (fun c => Counter.stage (base c) (T c) (b c) (s c)) enc + (encList encGateCode) := by + simp only [Counter.stage, Counter.level, Counter.below] + fun_prop + +theorem computableInPolyTime_counter {w r : γ → ℕ} + (hw : ComputableInPolyTime w enc encUnary) (hr : ComputableInPolyTime r enc encUnary) : + ComputableInPolyTime (fun c => Counter.codes (base (w c) (r c)) (r c + 1) + (fun s => (s + 1) * w c) (2 * r c)) enc (encList encGateCode) := by + have hstage := computableInPolyTime_stage (enc := encPair enc encUnary) + (base := fun p => base (w p.1) (r p.1)) (T := fun p => r p.1 + 1) + (b := fun p => (p.2 + 1) * w p.1) (s := fun p => p.2) + (by unfold base; fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) + have hbase : ComputableInPolyTime (fun c => base (w c) (r c)) enc encUnary := by + unfold base + fun_prop + unfold Counter.codes + fun_prop + +theorem computableInPolyTime_codes {n w r : γ → ℕ} {gs : γ → List GateCode} + (hn : ComputableInPolyTime n enc encUnary) (hw : ComputableInPolyTime w enc encUnary) + (hr : ComputableInPolyTime r enc encUnary) + (hgs : ComputableInPolyTime gs enc (encList encGateCode)) : + ComputableInPolyTime (fun c => codes (n c) (w c) (r c) (gs c)) enc (encList encGateCode) := by + have h₁ := computableInPolyTime_copyCodes hn hw (k := fun c => 2 * r c) (by fun_prop) + have h₂ := computableInPolyTime_copiesCodes hw (k := fun c => 2 * r c) (by fun_prop) hgs + have h₃ := computableInPolyTime_counter hw hr + have h₄ : ComputableInPolyTime (fun c => swapCodes (answer (w c) (r c))) enc + (encList encGateCode) := by + simp only [swapCodes, answer, Counter.level, base] + fun_prop + unfold codes + fun_prop + +end Amplify + +namespace UniformCircuitFamily + +open Amplify + +/-- **The amplified family**: on inputs of length `n`, `2 r(n)` copies of the family's circuit run +side by side, and a reversible majority vote of their answers is measured. -/ +def amplify (F : UniformCircuitFamily) (r : ℕ → ℕ) + (hr : ComputableInPolyTime r encUnary encUnary) : UniformCircuitFamily where + width n := Amplify.width (F.width n) (r n) + gates n := codes n (F.width n) (r n) (F.gates n) + computableInPolyTime_width := by + have := F.computableInPolyTime_width + simp only [Amplify.width, base] + fun_prop + computableInPolyTime_gates := + computableInPolyTime_codes (by fun_prop) F.computableInPolyTime_width hr + F.computableInPolyTime_gates + le_width n := by + have := F.le_width n + have : F.width n ≤ base (F.width n) (r n) := Nat.le_mul_of_pos_left _ (by omega) + have := base_lt_width (w := F.width n) (r := r n) + omega + width_pos n := Nat.lt_of_le_of_lt (Nat.zero_le _) base_lt_width + wellFormed n g hg := by + have hw := F.width_pos n + rcases List.mem_append.mp hg with hg | hg + · exact (isClassical_copyCodes (F.le_width n) hw g hg).2 + rcases List.mem_append.mp hg with hg | hg + · obtain ⟨j, hj, hg⟩ := List.mem_flatMap.mp hg + obtain ⟨g, hg', rfl⟩ := List.mem_map.mp hg + exact (F.wellFormed n g hg').shift (block_le_width (List.mem_range.mp hj)) + · exact (isClassical_counter_swap hw g hg).2 + +/-- **The acceptance probability of the amplified family** is the probability that more than +`r(n)` of `2 r(n)` independent runs of the family accept, on inputs of length `n`. -/ +theorem acceptProb_amplify (F : UniformCircuitFamily) {r : ℕ → ℕ} + (hr : ComputableInPolyTime r encUnary encUnary) (x : List Bool) : + (F.amplify r hr).acceptProb x = + ∑ b : Fin (2 * r x.length) → Bool with r x.length < (univ.filter fun j => b j = true).card, + ∏ j, if b j then F.acceptProb x else 1 - F.acceptProb x := + acceptProb_amplify_codes (F.width_pos _) (F.le_width _) (F.wellFormed _) x rfl + +/-- The trials of the majority vote: success with probability `p`. -/ +private theorem sum_bernoulli (p : ℝ) : ∑ c : Bool, (if c then p else 1 - p) = 1 := by + simp + +/-- **Amplifying acceptance**: a family accepting with probability at least `2 / 3` gives a family +accepting with probability at least `1 - (8 / 9) ^ r(n)`. -/ +theorem one_sub_le_acceptProb_amplify (F : UniformCircuitFamily) {r : ℕ → ℕ} + (hr : ComputableInPolyTime r encUnary encUnary) {x : List Bool} + (hx : 2 / 3 ≤ F.acceptProb x) : + 1 - (8 / 9) ^ r x.length ≤ (F.amplify r hr).acceptProb x := by + set p := F.acceptProb x + set R := r x.length + have hq : ∀ c : Bool, 0 ≤ if c then p else 1 - p := fun c => by + have := F.acceptProb_le_one x + cases c <;> simp <;> linarith + have hbad := sum_prod_le_of_card_filter_le (fun c : Bool => if c then p else 1 - p) hq + (sum_bernoulli p) {true} (by simpa using (by linarith : (2 : ℝ) ≤ 3 * p)) R + simp only [mem_singleton] at hbad + have htotal := (Fintype.sum_pow (fun c : Bool => if c then p else 1 - p) (2 * R)).symm + rw [sum_bernoulli, one_pow, ← sum_filter_add_sum_filter_not univ + (fun b : Fin (2 * R) → Bool => R < (univ.filter fun j => b j = true).card)] at htotal + simp only [not_lt] at htotal + rw [acceptProb_amplify] + linarith + +/-- **Amplifying rejection**: a family accepting with probability at most `1 / 3` gives a family +accepting with probability at most `(8 / 9) ^ r(n)`. -/ +theorem acceptProb_amplify_le (F : UniformCircuitFamily) {r : ℕ → ℕ} + (hr : ComputableInPolyTime r encUnary encUnary) {x : List Bool} + (hx : F.acceptProb x ≤ 1 / 3) : + (F.amplify r hr).acceptProb x ≤ (8 / 9) ^ r x.length := by + set p := F.acceptProb x + have hq : ∀ c : Bool, 0 ≤ if c then p else 1 - p := fun c => by + have := F.acceptProb_nonneg x + cases c <;> simp <;> linarith + have hbad := sum_prod_le_of_card_filter_le (fun c : Bool => if c then p else 1 - p) hq + (sum_bernoulli p) {false} (by simpa using (by linarith : (2 : ℝ) ≤ 3 * (1 - p))) (r x.length) + simp only [mem_singleton] at hbad + rw [acceptProb_amplify] + refine le_trans (sum_le_sum_of_subset_of_nonneg (fun b hb => ?_) + fun b _ _ => prod_nonneg fun j _ => hq _) hbad + rw [mem_filter] at hb ⊢ + refine ⟨mem_univ _, ?_⟩ + have := card_filter_add_card_filter_not (s := (univ : Finset (Fin (2 * r x.length)))) + (fun j => b j = true) + have e : (univ.filter fun j => ¬b j = true) = univ.filter fun j => b j = false := by + ext j + simp + rw [e, card_univ, Fintype.card_fin] at this + omega + +end UniformCircuitFamily + +end Cslib.Quantum + +namespace Cslib.Complexity + +open Quantum Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} + +/-- `(8 / 9) ^ (6 m) ≤ 2 ^ (-m)`, since `2 * 8 ^ 6 < 9 ^ 6`. -/ +private theorem eight_ninths_pow_le (m : ℕ) : ((8 : ℝ) / 9) ^ (6 * m) ≤ ((2 : ℝ) ^ m)⁻¹ := by + rw [pow_mul, ← inv_pow] + exact pow_le_pow_left₀ (by positivity) (by norm_num) m + +/-- **Error reduction for `BQP`**: a problem is in `BQP` exactly when, for every polynomial `q`, +some polynomial-time uniform family accepts the encodings of members with probability at least +`1 - 2^{-q(n)}` and those of other instances with probability at most `2^{-q(n)}`, where `n` is the +length of the encoding. -/ +theorem mem_BQP_iff_forall_errorExponent {A : Set α} : + A ∈ BQP enc ↔ ∀ q : Polynomial ℕ, ∃ F : UniformCircuitFamily, ∀ a, + (a ∈ A → 1 - ((2 : ℝ) ^ q.eval (enc a).length)⁻¹ ≤ F.acceptProb (enc a)) ∧ + (a ∉ A → F.acceptProb (enc a) ≤ ((2 : ℝ) ^ q.eval (enc a).length)⁻¹) := by + constructor + · rintro ⟨F, hF⟩ q + have hr : ComputableInPolyTime (fun n => 6 * q.eval n) encUnary encUnary := by fun_prop + refine ⟨F.amplify _ hr, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ + · exact le_trans (by linarith [eight_ninths_pow_le (q.eval (enc a).length)]) + (F.one_sub_le_acceptProb_amplify hr ((hF a).1 ha)) + · exact (F.acceptProb_amplify_le hr ((hF a).2 ha)).trans (eight_ninths_pow_le _) + · intro h + obtain ⟨F, hF⟩ := h (Polynomial.C 2) + refine ⟨F, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ + · have := (hF a).1 ha + simp only [Polynomial.eval_C] at this + norm_num at this ⊢ + linarith + · have := (hF a).2 ha + simp only [Polynomial.eval_C] at this + norm_num at this ⊢ + linarith + +end Cslib.Complexity diff --git a/Complexity/Foundations/Combinatorics/MajorityVote/Weighted.lean b/Complexity/Foundations/Combinatorics/MajorityVote/Weighted.lean new file mode 100644 index 000000000..b81adc03e --- /dev/null +++ b/Complexity/Foundations/Combinatorics/MajorityVote/Weighted.lean @@ -0,0 +1,109 @@ +/- +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.Init +public import Mathlib.Algebra.BigOperators.Fin +public import Mathlib.Basic.Real.Basic +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Algebra.Order.BigOperators.Ring.Finset +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Majority votes over independent trials + +Repeat a trial `2 r` times independently, where each trial has outcome `ω ∈ Ω` with probability +`q ω` and is *good* with probability at least `2 / 3`. Then at most half of the trials are good with +probability at most `(8 / 9) ^ r` (`Cslib.sum_prod_le_of_card_filter_le`). This is the weighted form +of `Cslib.card_filter_card_filter_le_le`, where `q` is uniform, with the same exponential-moment +proof: weight the bad outcomes by `2`, so that the expected weight of a tuple is at most +`(4 / 3) ^ (2 r)` while a tuple with at most `r` good entries has weight at least `2 ^ r`. + +## Main results + +* `Cslib.sum_prod_le_of_card_filter_le`: the bound. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, Section 7.4][AroraBarak09] +-/ + +@[expose] public section + +namespace Cslib + +open Finset + +variable {Ω : Type*} [Fintype Ω] [DecidableEq Ω] + +/-- The weight of an outcome in the exponential-moment bound: `1` when good, `2` when bad. -/ +private def voteWeight (G : Finset Ω) (a : Ω) : ℝ := if a ∈ G then 1 else 2 + +omit [Fintype Ω] in +private theorem voteWeight_nonneg (G : Finset Ω) (a : Ω) : 0 ≤ voteWeight G a := by + unfold voteWeight + split_ifs <;> norm_num + +omit [Fintype Ω] in +/-- A tuple with at most `r` of its `2 r` entries good has weight at least `2 ^ r`. -/ +private theorem two_pow_le_prod_voteWeight (G : Finset Ω) {r : ℕ} (ω : Fin (2 * r) → Ω) + (hω : (univ.filter fun i => ω i ∈ G).card ≤ r) : (2 : ℝ) ^ r ≤ ∏ i, voteWeight G (ω i) := by + simp only [voteWeight] + rw [prod_ite, prod_const_one, prod_const, one_mul] + refine pow_le_pow_right₀ (by norm_num) ?_ + have := card_filter_add_card_filter_not (s := (univ : Finset (Fin (2 * r)))) + (fun i => ω i ∈ G) + rw [card_univ, Fintype.card_fin] at this + omega + +/-- The expected weight of one trial is at most `4 / 3`. -/ +private theorem sum_mul_voteWeight_le (q : Ω → ℝ) (hsum : ∑ ω, q ω = 1) (G : Finset Ω) + (hG : 2 ≤ 3 * ∑ ω ∈ G, q ω) : ∑ a, q a * voteWeight G a ≤ 4 / 3 := by + have hsplit : ∑ a, q a * voteWeight G a = 2 - ∑ a ∈ G, q a := by + simp only [voteWeight, mul_ite, mul_one] + rw [sum_ite, filter_mem_eq_inter, univ_inter, ← sum_mul, mul_comm] + have h := sum_filter_add_sum_filter_not (univ : Finset Ω) (fun a => a ∈ G) q + rw [filter_mem_eq_inter, univ_inter, hsum] at h + linarith + linarith + +/-- **Majority votes over independent trials.** If each trial is good with probability at least +`2 / 3`, then at most half of `2 r` independent trials are good with probability at most +`(8 / 9) ^ r`. -/ +theorem sum_prod_le_of_card_filter_le (q : Ω → ℝ) (hq : ∀ ω, 0 ≤ q ω) (hsum : ∑ ω, q ω = 1) + (G : Finset Ω) (hG : 2 ≤ 3 * ∑ ω ∈ G, q ω) (r : ℕ) : + ∑ ω : Fin (2 * r) → Ω with (univ.filter fun i => ω i ∈ G).card ≤ r, ∏ i, q (ω i) ≤ + (8 / 9) ^ r := by + have hmean₀ : 0 ≤ ∑ a, q a * voteWeight G a := + sum_nonneg fun a _ => mul_nonneg (hq a) (voteWeight_nonneg G a) + have h2r : (0 : ℝ) < 2 ^ r := by positivity + rw [← mul_le_mul_iff_of_pos_left h2r] + calc 2 ^ r * ∑ ω : Fin (2 * r) → Ω with (univ.filter fun i => ω i ∈ G).card ≤ r, + ∏ i, q (ω i) + ≤ ∑ ω : Fin (2 * r) → Ω with (univ.filter fun i => ω i ∈ G).card ≤ r, + ∏ i, (q (ω i) * voteWeight G (ω i)) := by + rw [mul_sum] + refine sum_le_sum fun ω hω => ?_ + rw [prod_mul_distrib, mul_comm] + exact mul_le_mul_of_nonneg_left (two_pow_le_prod_voteWeight G ω (mem_filter.mp hω).2) + (prod_nonneg fun i _ => hq _) + _ ≤ ∑ ω : Fin (2 * r) → Ω, ∏ i, (q (ω i) * voteWeight G (ω i)) := + sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun ω _ _ => + prod_nonneg fun i _ => mul_nonneg (hq _) (voteWeight_nonneg G _) + _ = (∑ a, q a * voteWeight G a) ^ (2 * r) := + (Fintype.sum_pow (fun a => q a * voteWeight G a) (2 * r)).symm + _ ≤ (4 / 3) ^ (2 * r) := pow_le_pow_left₀ hmean₀ (sum_mul_voteWeight_le q hsum G hG) _ + _ = 2 ^ r * (8 / 9) ^ r := by + rw [pow_mul, ← mul_pow] + norm_num + +end Cslib diff --git a/ComplexityTests/BQPAmplification.lean b/ComplexityTests/BQPAmplification.lean new file mode 100644 index 000000000..11fafe503 --- /dev/null +++ b/ComplexityTests/BQPAmplification.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.Amplification +import ComplexityTests.BQP + +/-! Error reduction for `BQP`: the reversible counter on a concrete register, the exact +acceptance probability of a majority vote over two fair coins, and exponentially small error for a +language in `BQP`. -/ + +namespace ComplexityTests.BQPAmplification + +open Cslib Cslib.Quantum Cslib.Complexity Finset Turing.MultiTapeTM +open ComplexityTests.BQP + +/-! ### The counter -/ + +-- Two input bits at qubits `0, 1`, one of them set; two levels from `base = 2` on, on `9` qubits. +-- After both stages, level `0` (more than zero inputs set) is one and level `1` is zero. +example : readBit (GateCode.classicalRun (Counter.codes 2 2 id 2) + (fun i : Fin 9 => decide (i = 0))) (Counter.level 2 2 2 0) = true := by decide +example : readBit (GateCode.classicalRun (Counter.codes 2 2 id 2) + (fun i : Fin 9 => decide (i = 0))) (Counter.level 2 2 2 1) = false := by decide +-- With both inputs set, level `1` is one. +example : readBit (GateCode.classicalRun (Counter.codes 2 2 id 2) + (fun i : Fin 9 => decide (i.val < 2))) (Counter.level 2 2 2 1) = true := by decide + +/-! ### A majority of two fair coins -/ + +/-- Both of two fair coins land heads with probability `1 / 4`: amplifying the family that +measures `H|0⟩` by a strict majority of two copies. -/ +theorem acceptProb_amplify_hadamardOnce (x : List Bool) : + (hadamardOnce.amplify (fun _ => 1) (ComputableInPolyTime.const _)).acceptProb x = 1 / 4 := by + rw [UniformCircuitFamily.acceptProb_amplify, acceptProb_hadamardOnce] + have hhalf (c : Bool) : (if c = true then (1 / 2 : ℝ) else 1 - 1 / 2) = 1 / 2 := by + cases c <;> norm_num + simp only [hhalf, prod_const, card_univ, Fintype.card_fin, sum_const, nsmul_eq_mul] + have hcard : (univ.filter fun b : Fin (2 * 1) → Bool => + 1 < (univ.filter fun j => b j = true).card).card = 1 := by decide + rw [hcard] + norm_num + +/-! ### Exponentially small error -/ + +-- The words starting with one are accepted with probability at least `1 - 2^{-q(n)}`, and the +-- others with probability at most `2^{-q(n)}`, for every polynomial `q`. +example (q : Polynomial ℕ) : ∃ F : UniformCircuitFamily, ∀ x, + (x ∈ FirstBit → 1 - ((2 : ℝ) ^ q.eval (encBits x).length)⁻¹ ≤ F.acceptProb (encBits x)) ∧ + (x ∉ FirstBit → F.acceptProb (encBits x) ≤ ((2 : ℝ) ^ q.eval (encBits x).length)⁻¹) := + mem_BQP_iff_forall_errorExponent.mp firstBit_mem_BQP q + +end ComplexityTests.BQPAmplification From bcbbeb9d321666769dff0f70d8b0a507ca311052 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 00:31:36 -0400 Subject: [PATCH 3/4] refactor(Circuit/Quantum): move the swap codes beside the classical gate codes The three-CNOT swap into qubit 0 is reused by the reversible compilation of Boolean circuits, so it belongs with the classical gate-code API rather than inside the amplification construction. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Circuit/Quantum/Classical.lean | 28 +++++++++++++++++++ .../Complexity/Classes/BQP/Amplification.lean | 26 +---------------- 2 files changed, 29 insertions(+), 25 deletions(-) diff --git a/Complexity/Computability/Circuit/Quantum/Classical.lean b/Complexity/Computability/Circuit/Quantum/Classical.lean index 3937b2bd2..73e2bbcad 100644 --- a/Complexity/Computability/Circuit/Quantum/Classical.lean +++ b/Complexity/Computability/Circuit/Quantum/Classical.lean @@ -31,6 +31,7 @@ Bits of a basis string are read by their number (`Cslib.Quantum.readBit`), as in * `Cslib.Quantum.GateCode.IsClassical`: a list of well-formed classical gate codes. * `Cslib.Quantum.GateCode.classicalRun`, `Cslib.Quantum.GateCode.classicalUnrun`: the composed permutation of a list of classical codes and its inverse. +* `Cslib.Quantum.GateCode.swapCodes`: three CNOT gates moving a qubit into qubit `0`. ## Main results @@ -244,6 +245,33 @@ theorem exists_toPlacedGate?_eval_apply {g : GateCode} (h₁ : g.1 = false) (h simp only [PlacedGate.eval, unitaryEquiv_apply, Matrix.mulVec, dotProduct, hrow, ite_mul, one_mul, zero_mul, sum_ite_eq', mem_univ, ite_true] + +/-! ### Swapping a qubit into qubit `0` -/ + +/-- Three CNOT gates swapping qubit `a` into qubit `0`. -/ +def swapCodes (a : ℕ) : List GateCode := [(false, 0, [a]), (false, a, [0]), (false, 0, [a])] + +theorem isClassical_swapCodes {N a : ℕ} (ha : 0 < a) (hN : a < N) : + IsClassical N (swapCodes a) := by + have h₀ : WellFormed N ((false, 0, [a]) : GateCode) := + ⟨by simp, by simp; omega, by simp; omega⟩ + have h₁ : WellFormed N ((false, a, [0]) : GateCode) := + ⟨by simp, by simp; omega, by simp; omega⟩ + intro g hg + simp only [swapCodes, List.mem_cons, List.not_mem_nil, or_false] at hg + rcases hg with rfl | rfl | rfl + · exact ⟨rfl, h₀⟩ + · exact ⟨rfl, h₁⟩ + · exact ⟨rfl, h₀⟩ + +/-- **The swap moves qubit `a` into qubit `0`.** -/ +theorem readBit_classicalRun_swapCodes {N a : ℕ} (ha : 0 < a) (hN : a < N) (X : Fin N → Bool) : + readBit (classicalRun (swapCodes a) X) 0 = readBit X a := by + simp only [swapCodes, classicalRun_cons, classicalRun_nil, readBit_classicalStep, + List.all_cons, List.all_nil, Bool.and_true] + have h0 : (0 : ℕ) < N := by omega + simp [h0, hN, show a ≠ 0 by omega, show (0 : ℕ) ≠ a by omega] + end GateCode open GateCode diff --git a/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean b/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean index 804d03a26..ba8badb39 100644 --- a/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean +++ b/Complexity/Computability/Complexity/Classes/BQP/Amplification.lean @@ -34,7 +34,7 @@ input, `2 r` blocks of the original width `w`, and the ancillas of a threshold c (`Cslib.Quantum.Amplify.copiesCodes`); 3. a reversible counter computes whether more than `r` of the blocks' first qubits are one (`Cslib.Quantum.Counter.codes`); -4. three CNOT gates swap that answer into qubit `0` (`Cslib.Quantum.Amplify.swapCodes`). +4. three CNOT gates swap that answer into qubit `0` (`Cslib.Quantum.GateCode.swapCodes`). The copies act on disjoint blocks, so their measurement outcomes are independent (`Cslib.Quantum.Circuit.matrix_flatMap_mapWires`), and the classical steps permute the outcomes. The @@ -81,9 +81,6 @@ def copyCodes (n w k : ℕ) : List GateCode := def copiesCodes (w k : ℕ) (gs : List GateCode) : List GateCode := (List.range k).flatMap fun j => gs.map (shift ((j + 1) * w)) -/-- Three CNOT gates swapping qubit `a` into qubit `0`. -/ -def swapCodes (a : ℕ) : List GateCode := [(false, 0, [a]), (false, a, [0]), (false, 0, [a])] - /-- The first ancilla of the counter, after the input block and `2 r` copies of width `w`. -/ def base (w r : ℕ) : ℕ := (2 * r + 1) * w @@ -222,27 +219,6 @@ theorem readBit_classicalRun_copyCodes (hn : n ≤ w) (hw : 0 < w) (X : Fin (wid · simp only [Bool.and_eq_false_iff, decide_eq_false_iff_not] exact Or.inl fun ⟨i, hi, h⟩ => hp ⟨j, hj, i, by omega, h⟩ -theorem isClassical_swapCodes {N a : ℕ} (ha : 0 < a) (hN : a < N) : - IsClassical N (swapCodes a) := by - have h₀ : WellFormed N ((false, 0, [a]) : GateCode) := - ⟨by simp, by simp; omega, by simp; omega⟩ - have h₁ : WellFormed N ((false, a, [0]) : GateCode) := - ⟨by simp, by simp; omega, by simp; omega⟩ - intro g hg - simp only [swapCodes, List.mem_cons, List.not_mem_nil, or_false] at hg - rcases hg with rfl | rfl | rfl - · exact ⟨rfl, h₀⟩ - · exact ⟨rfl, h₁⟩ - · exact ⟨rfl, h₀⟩ - -/-- **The swap moves qubit `a` into qubit `0`.** -/ -theorem readBit_classicalRun_swapCodes {N a : ℕ} (ha : 0 < a) (hN : a < N) (X : Fin N → Bool) : - readBit (classicalRun (swapCodes a) X) 0 = readBit X a := by - simp only [swapCodes, classicalRun_cons, classicalRun_nil, readBit_classicalStep, - List.all_cons, List.all_nil, Bool.and_true] - have h0 : (0 : ℕ) < N := by omega - simp [h0, hN, show a ≠ 0 by omega, show (0 : ℕ) ≠ a by omega] - theorem isClassical_counter_swap (hw : 0 < w) : IsClassical (width w r) (Counter.codes (base w r) (r + 1) (fun s => (s + 1) * w) (2 * r) ++ swapCodes (answer w r)) := by From 599c6d8b7c68b6ae054242665f64bc0268ec38dd Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 00:39:33 -0400 Subject: [PATCH 4/4] =?UTF-8?q?feat(Classes/BQP):=20P=20=E2=8A=86=20BQP=20?= =?UTF-8?q?by=20reversible=20compilation=20of=20uniform=20circuits=20(#896?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Every polynomial-time Boolean function is computed exactly, with acceptance probability 1 or 0, by a uniform family of NOT/CNOT/Toffoli circuits: the polynomial-time uniform De Morgan circuits are compiled gate by gate onto fresh qubits, and the output wire is swapped into qubit 0. Arguments that are missing or name later wires read a never-written zero qubit, matching evalCode, so the compiler is correct on every gate list. Wire numbers are capped by the gate's unary index before conversion, so compilation runs in polynomial time. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Circuit/Quantum/Reversible.lean | 304 ++++++++++++++++++ .../Complexity/Classes/BQP/Classical.lean | 203 ++++++++++++ ComplexityTests/BQPClassical.lean | 46 +++ 4 files changed, 555 insertions(+) create mode 100644 Complexity/Computability/Circuit/Quantum/Reversible.lean create mode 100644 Complexity/Computability/Complexity/Classes/BQP/Classical.lean create mode 100644 ComplexityTests/BQPClassical.lean diff --git a/Complexity.lean b/Complexity.lean index 1c966dc5d..1de8e877b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -941,6 +941,7 @@ public import Complexity.Computability.Circuit.Quantum.Classical public import Complexity.Computability.Circuit.Quantum.Code public import Complexity.Computability.Circuit.Quantum.Counter public import Complexity.Computability.Circuit.Quantum.Parallel +public import Complexity.Computability.Circuit.Quantum.Reversible public import Complexity.Computability.Circuit.Quantum.Uniform public import Complexity.Computability.Circuit.Rational public import Complexity.Computability.Circuit.Rational.Affine @@ -1049,6 +1050,7 @@ 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.Amplification +public import Complexity.Computability.Complexity.Classes.BQP.Classical 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/Reversible.lean b/Complexity/Computability/Circuit/Quantum/Reversible.lean new file mode 100644 index 000000000..c7792f731 --- /dev/null +++ b/Complexity/Computability/Circuit/Quantum/Reversible.lean @@ -0,0 +1,304 @@ +/- +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.Classical +public import Complexity.Computability.Circuit.Quantum.Uniform +public import Complexity.Computability.Circuit.Boolean.EvaluationTime +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.Nat.Binary +import Mathlib.Data.List.GetD + +/-! +# Reversible compilation of Boolean circuits + +A De Morgan gate list (`Complexity/Computability/Circuit/Boolean/Encoding.lean`) on `n` inputs is +compiled into NOT, CNOT and Toffoli gate codes (`Cslib.Quantum.Reversible.codes`). Input `i` sits on +qubit `i` and gate `j` writes its value onto the fresh qubit `n + j`, the numbering of wires in +circuit codes. A constant gate is a NOT or nothing, a negation is a CNOT followed by a NOT, a +conjunction is a Toffoli gate, and a disjunction `a ∨ b = a ⊕ b ⊕ (a ∧ b)` is two CNOT gates and a +Toffoli gate. An argument that is missing, or that names a wire not computed before the gate, is +read from a qubit `z` that no gate writes, which stays zero; this matches `Cslib.Circuits.evalCode`, +which reads such arguments as `false`, so the compilation is correct for every gate list +(`Cslib.Quantum.Reversible.readBit_classicalRun_codes`). Nothing is uncomputed: the circuit is +measured once at the end, and only one qubit matters. + +Wire numbers in circuit codes are binary; the compiler caps each argument by the unary number of its +gate before converting it, so it runs in polynomial time +(`Cslib.Quantum.Reversible.computableInPolyTime_codes`). + +## Main definitions + +* `Cslib.Quantum.Reversible.gateCodes`: the gate codes of one De Morgan gate. +* `Cslib.Quantum.Reversible.codes`: the gate codes of a De Morgan gate list. + +## Main results + +* `Cslib.Quantum.Reversible.isClassical_codes`: the compiled circuit is classical. +* `Cslib.Quantum.Reversible.readBit_classicalRun_codes`: it computes the wire values of the gate + list. +* `Cslib.Quantum.Reversible.computableInPolyTime_codes`: it is compiled in polynomial time. +-/ + +@[expose] public section + +namespace Cslib.Quantum.Reversible + +open Circuits Circuits.Boolean GateCode Turing.MultiTapeTM + +/-- Argument `i` of a gate whose wire is `t`, capped at `t`; `t` when the argument is missing. -/ +def capArg (t : ℕ) (args : List ℕ) (i : ℕ) : ℕ := + if i < args.length then min t (args.getD i 0) else t + +/-- The qubit read for argument `i` of a gate writing qubit `t`: the wire it names, when that wire +is computed before the gate, and the zero qubit `z` otherwise. -/ +def argQubit (z t : ℕ) (args : List ℕ) (i : ℕ) : ℕ := + if capArg t args i < t then capArg t args i else z + +/-- The gate codes computing the De Morgan gate `g` onto the fresh qubit `t`, reading missing or +not yet computed arguments from the zero qubit `z`. -/ +def gateCodes (z t : ℕ) (g : Op × List ℕ) : List GateCode := + match g.1 with + | .const b => if b then [(false, t, [])] else [] + | .not => [(false, t, [argQubit z t g.2 0]), (false, t, [])] + | .and => + if argQubit z t g.2 0 = argQubit z t g.2 1 then [(false, t, [argQubit z t g.2 0])] + else [(false, t, [argQubit z t g.2 0, argQubit z t g.2 1])] + | .or => + if argQubit z t g.2 0 = argQubit z t g.2 1 then [(false, t, [argQubit z t g.2 0])] + else [(false, t, [argQubit z t g.2 0]), (false, t, [argQubit z t g.2 1]), + (false, t, [argQubit z t g.2 0, argQubit z t g.2 1])] + +/-- **The reversible compilation** of a De Morgan gate list on `n` inputs: gate `j` is computed +onto qubit `n + j`, with `z` the zero qubit. -/ +def codes (n z : ℕ) (gates : List (Op × List ℕ)) : List GateCode := + gates.zipIdx.flatMap fun p => gateCodes z (n + p.2) p.1 + +theorem codes_append_singleton (n z : ℕ) (gates : List (Op × List ℕ)) (g : Op × List ℕ) : + codes n z (gates ++ [g]) = codes n z gates ++ gateCodes z (n + gates.length) g := by + simp [codes, List.zipIdx_append] + +/-! ### Correctness -/ + +variable {W : ℕ} + +theorem argQubit_lt_or_eq (z t : ℕ) (args : List ℕ) (i : ℕ) : + argQubit z t args i < t ∨ argQubit z t args i = z := by + unfold argQubit + split_ifs with h + · exact Or.inl h + · exact Or.inr rfl + +/-- **The qubit read for an argument holds its value**, when the qubits hold the wire values +`vals` computed before the gate. -/ +theorem readBit_argQubit {z t : ℕ} (hz : t ≤ z) {Y : Fin W → Bool} {vals : List Bool} + (hvals : vals.length = t) (hY : ∀ p, readBit Y p = vals.getD p false) (args : List ℕ) + (i : ℕ) : readBit Y (argQubit z t args i) = args[i]?.elim false (vals.getD · false) := by + have hfalse (p : ℕ) (hp : t ≤ p) : vals.getD p false = false := by + rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)] + rfl + unfold argQubit capArg + by_cases hi : i < args.length + · rw [List.getElem?_eq_getElem hi, Option.elim_some, List.getD_eq_getElem _ _ hi] + simp only [hi, ite_true] + by_cases ha : args[i] < t + · rw [min_eq_right ha.le, ite_eq_left ha, hY] + · rw [min_eq_left (not_lt.mp ha), ite_eq_right (lt_irrefl t), hY, hfalse z hz, + hfalse _ (not_lt.mp ha)] + · rw [List.getElem?_eq_none (not_lt.mp hi)] + simp only [hi, ite_false, lt_irrefl, Option.elim_none] + rw [hY, hfalse z hz] + +theorem isClassical_gateCodes {z t : ℕ} (htz : t < z) (hz : z < W) (g : Op × List ℕ) : + IsClassical W (gateCodes z t g) := by + have ha (i : ℕ) := argQubit_lt_or_eq z t g.2 i + have ht : t < W := htz.trans hz + have hlt (i : ℕ) : argQubit z t g.2 i < W := by rcases ha i with h | h <;> omega + have hne (i : ℕ) : t ≠ argQubit z t g.2 i := by rcases ha i with h | h <;> omega + have hnot : WellFormed W ((false, t, []) : GateCode) := ⟨by simp, by simp, by simpa using ht⟩ + have hcnot (i : ℕ) : WellFormed W ((false, t, [argQubit z t g.2 i]) : GateCode) := + ⟨by simp, by simpa using hne i, by simpa [ht] using hlt i⟩ + have htof (h : argQubit z t g.2 0 ≠ argQubit z t g.2 1) : + WellFormed W ((false, t, [argQubit z t g.2 0, argQubit z t g.2 1]) : GateCode) := + ⟨by simp, by simp [hne 0, hne 1, h], by simp [ht, hlt 0, hlt 1]⟩ + intro c hc + obtain ⟨op, args⟩ := g + cases op with + | const b => + cases b + · simp only [gateCodes, Bool.false_eq_true, ite_false, List.not_mem_nil] at hc + · simp only [gateCodes, ite_true, List.mem_singleton] at hc + exact hc ▸ ⟨rfl, hnot⟩ + | not => + simp only [gateCodes, List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl + · exact ⟨rfl, hcnot 0⟩ + · exact ⟨rfl, hnot⟩ + | and => + simp only [gateCodes] at hc + split_ifs at hc with h + · exact (List.mem_singleton.mp hc) ▸ ⟨rfl, hcnot 0⟩ + · exact (List.mem_singleton.mp hc) ▸ ⟨rfl, htof h⟩ + | or => + simp only [gateCodes] at hc + split_ifs at hc with h + · exact (List.mem_singleton.mp hc) ▸ ⟨rfl, hcnot 0⟩ + · simp only [List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl | rfl + · exact ⟨rfl, hcnot 0⟩ + · exact ⟨rfl, hcnot 1⟩ + · exact ⟨rfl, htof h⟩ + +/-- **One compiled gate appends its value**: if the qubits hold the wire values `vals` computed +before the gate `g` and zeros after them, its codes add the value of `g` on qubit `t`. -/ +theorem readBit_classicalRun_gateCodes {z t : ℕ} (htz : t < z) (hz : z < W) + {Y : Fin W → Bool} {vals : List Bool} (hvals : vals.length = t) + (hY : ∀ p, readBit Y p = vals.getD p false) (g : Op × List ℕ) (p : ℕ) : + readBit (classicalRun (gateCodes z t g) Y) p = + (vals ++ [interpretation g.1 fun a => g.2[a.val]?.elim false (vals.getD · false)]).getD p + false := by + have hread : ∀ c ∈ gateCodes z t g, ∀ c' ∈ gateCodes z t g, c.2.1 ∉ c'.2.2 := by + have hne (i : ℕ) : t ≠ argQubit z t g.2 i := by + rcases argQubit_lt_or_eq z t g.2 i with h | h <;> omega + intro c hc c' hc' + obtain ⟨op, args⟩ := g + cases op with + | const b => cases b <;> simp_all [gateCodes] + | not => simp only [gateCodes, List.mem_cons, List.not_mem_nil, or_false] at hc hc' + rcases hc with rfl | rfl <;> rcases hc' with rfl | rfl <;> simp [hne 0] + | and => + simp only [gateCodes] at hc hc' + split_ifs at hc hc' <;> simp only [List.mem_singleton] at hc hc' <;> subst hc hc' <;> + simp [hne 0, hne 1] + | or => + simp only [gateCodes] at hc hc' + split_ifs at hc hc' <;> + simp only [List.mem_cons, List.not_mem_nil, or_false] at hc hc' <;> + (try rcases hc with rfl | rfl | rfl) <;> (try rcases hc' with rfl | rfl | rfl) <;> + simp [hne 0, hne 1] + rw [readBit_classicalRun_of_forall_notMem (isClassical_gateCodes htz hz g) hread, hY] + have harg (i : ℕ) := readBit_argQubit htz.le hvals hY g.2 i + have hget : (vals ++ [interpretation g.1 fun a => g.2[a.val]?.elim false + (vals.getD · false)]).getD p false = + if p = t then interpretation g.1 fun a => g.2[a.val]?.elim false (vals.getD · false) + else vals.getD p false := by + rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD] + split_ifs with hp + · subst hp + simp [hvals] + · rcases lt_or_gt_of_ne hp with h | h + · rw [List.getElem?_append_left (by omega)] + · rw [List.getElem?_eq_none (by simp; omega), List.getElem?_eq_none (by omega)] + rw [hget] + have ht : vals.getD t false = false := by + rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)] + rfl + obtain ⟨op, args⟩ := g + by_cases hp : p = t + · subst p + rw [ht, show (interpretation op fun a => args[a.val]?.elim false (vals.getD · false)) = + interpretation op fun a => readBit Y (argQubit z t args a) from + congrArg _ (funext fun a => (harg a).symm)] + cases op with + | const b => cases b <;> simp [gateCodes, interpretation] + | not => simp [gateCodes, interpretation] + | and => + simp only [gateCodes] + split_ifs with h + · simp [interpretation, ← h] + · simp [interpretation] + | or => + simp only [gateCodes] + split_ifs with h + · simp [interpretation, ← h] + · simp only [List.foldl_cons, List.foldl_nil, List.all_cons, List.all_nil, + decide_true, Bool.true_and, Bool.and_true, Bool.false_xor, interpretation, + Fin.val_zero, Fin.val_one] + cases readBit Y (argQubit z t args 0) <;> cases readBit Y (argQubit z t args 1) <;> rfl + · rw [ite_eq_right hp] + cases op with + | const b => cases b <;> simp [gateCodes, hp] + | not => simp [gateCodes, hp] + | and => + simp only [gateCodes] + split_ifs <;> simp [hp] + | or => + simp only [gateCodes] + split_ifs <;> simp [hp] + +theorem isClassical_codes {n z : ℕ} {gates : List (Op × List ℕ)} (hz : n + gates.length ≤ z) + (hW : z < W) : IsClassical W (codes n z gates) := by + refine IsClassical.flatMap fun p hp => isClassical_gateCodes ?_ hW p.1 + have := (List.mem_zipIdx hp).2.1 + omega + +/-- **The compiled circuit computes the gate list's wire values**: started from the input bits +`xs` and zeros, qubit `p` ends with the value of wire `p` (`false` past the last wire). -/ +theorem readBit_classicalRun_codes {n z : ℕ} {gates : List (Op × List ℕ)} + (hz : n + gates.length ≤ z) (hW : z < W) {xs : List Bool} (hxs : xs.length = n) + {X : Fin W → Bool} (hX : ∀ p, readBit X p = xs.getD p false) (p : ℕ) : + readBit (classicalRun (codes n z gates) X) p = + (evalCode interpretation false xs gates).getD p false := by + induction gates using List.reverseRecOn generalizing p with + | nil => rw [codes, List.zipIdx_nil, List.flatMap_nil, classicalRun_nil, evalCode_nil, hX] + | append_singleton gates g ih => + simp only [List.length_append, List.length_singleton] at hz + rw [codes_append_singleton, classicalRun_append, evalCode_append_singleton] + exact readBit_classicalRun_gateCodes (by omega) hW (by simp [hxs]) (ih (by omega)) g p + +/-! ### Polynomial time -/ + +variable {γ : Type} {enc : γ ↪ List Bool} + +/-- One gate written with decisions on its operation, for polynomial-time compilation. -/ +private theorem gateCodes_eq (z t : ℕ) (g : Op × List ℕ) : + gateCodes z t g = + if g.1 = .const true then [(false, t, [])] + else if g.1 = .not then [(false, t, [argQubit z t g.2 0]), (false, t, [])] + else if g.1 = .and then + (if argQubit z t g.2 0 = argQubit z t g.2 1 then [(false, t, [argQubit z t g.2 0])] + else [(false, t, [argQubit z t g.2 0, argQubit z t g.2 1])]) + else if g.1 = .or then + (if argQubit z t g.2 0 = argQubit z t g.2 1 then [(false, t, [argQubit z t g.2 0])] + else [(false, t, [argQubit z t g.2 0]), (false, t, [argQubit z t g.2 1]), + (false, t, [argQubit z t g.2 0, argQubit z t g.2 1])]) + else [] := by + obtain ⟨op, args⟩ := g + cases op with + | const b => cases b <;> simp [gateCodes] + | not => simp [gateCodes] + | and => simp [gateCodes] + | or => simp [gateCodes] + +theorem computableInPolyTime_gateCodes {z t : γ → ℕ} {g : γ → Op × List ℕ} + (hz : ComputableInPolyTime z enc encUnary) (ht : ComputableInPolyTime t enc encUnary) + (hg : ComputableInPolyTime g enc encGate) : + ComputableInPolyTime (fun c => gateCodes (z c) (t c) (g c)) enc (encList encGateCode) := by + have harg (i : ℕ) : ComputableInPolyTime (fun c => argQubit (z c) (t c) (g c).2 i) enc + encUnary := by + unfold argQubit capArg + fun_prop + have h₀ := harg 0 + have h₁ := harg 1 + simp only [gateCodes_eq] + fun_prop + +/-- **The reversible compilation runs in polynomial time.** -/ +theorem computableInPolyTime_codes {n z : γ → ℕ} {gates : γ → List (Op × List ℕ)} + (hn : ComputableInPolyTime n enc encUnary) (hz : ComputableInPolyTime z enc encUnary) + (hgates : ComputableInPolyTime gates enc (encList encGate)) : + ComputableInPolyTime (fun c => codes (n c) (z c) (gates c)) enc (encList encGateCode) := by + have hg : ComputableInPolyTime (fun q : γ × ((Op × List ℕ) × ℕ) => + gateCodes (z q.1) (n q.1 + q.2.2) q.2.1) (encPair enc (encPair encGate encUnary)) + (encList encGateCode) := + computableInPolyTime_gateCodes (by fun_prop) (by fun_prop) (by fun_prop) + unfold codes + fun_prop + +end Cslib.Quantum.Reversible diff --git a/Complexity/Computability/Complexity/Classes/BQP/Classical.lean b/Complexity/Computability/Complexity/Classes/BQP/Classical.lean new file mode 100644 index 000000000..9881713af --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/BQP/Classical.lean @@ -0,0 +1,203 @@ +/- +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.Complexity.Classes.P +public import Complexity.Computability.Circuit.Quantum.Reversible +import Complexity.Computability.Complexity.Problems.CircuitValue.Completeness +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.Nat.Binary + +/-! +# Classical computation in `BQP` + +Every polynomial-time Boolean function is computed **exactly** by a uniform family of quantum +circuits over the NOT, CNOT and Toffoli gates (`Cslib.Complexity.exists_uniformCircuitFamily`): +its acceptance probability is `1` on the instances where the function is true and `0` elsewhere. +Hence `P ⊆ BQP` (`Cslib.Complexity.P_subset_BQP`). + +The family compiles the polynomial-time uniform Boolean circuits of +`Cslib.Complexity.CircuitValue.exists_uniformCircuits`. On inputs of length `n`, the De Morgan +circuit with `G` gates is compiled into reversible gates on `n + G + 1` qubits +(`Cslib.Quantum.Reversible.codes`): gate `j` writes the fresh qubit `n + j`, and the last qubit +stays zero. Three CNOT gates then swap the output wire into qubit `0` +(`Cslib.Quantum.Reversible.circuitCodes`). A classical circuit maps the input basis state to a basis +state, so the final measurement reads the circuit's output with certainty. This is the gate-by-gate +simulation of Boolean circuits by permutation gates in [Arora, Barak][AroraBarak09], Chapter 10 +(Section 20.4 of the January 2007 web draft, used there for Theorem 20.17, `BPP ⊆ BQP`), without +the final uncomputation, which is unnecessary when only qubit `0` is measured. + +## Main definitions + +* `Cslib.Quantum.Reversible.circuitCodes`: the quantum gate codes of a De Morgan circuit code. +* `Cslib.Quantum.UniformCircuitFamily.ofBooleanCircuits`: the family of a polynomial-time uniform + family of De Morgan circuits. + +## Main results + +* `Cslib.Quantum.Reversible.acceptProb_circuitCodes`: the compiled circuit accepts with + probability `1` or `0`, according to the output of the De Morgan circuit. +* `Cslib.Complexity.exists_uniformCircuitFamily`: exact quantum computation of polynomial-time + Boolean functions. +* `Cslib.Complexity.P_subset_BQP`. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Circuits Circuits.Boolean GateCode Turing.MultiTapeTM + +namespace Reversible + +/-- The qubit holding output wire `o` of a gate list compiled with zero qubit `z`. -/ +def outQubit (z o : ℕ) : ℕ := min z o + +/-- **The quantum gate codes of a De Morgan circuit code** on `n` inputs: compile its gates onto +`n + G` qubits, with zero qubit `n + G`, and swap its first output wire into qubit `0`. -/ +def circuitCodes (n : ℕ) (code : List (Op × List ℕ) × List ℕ) : List GateCode := + codes n (n + code.1.length) code.1 ++ + if outQubit (n + code.1.length) (code.2.getD 0 0) = 0 then [] + else swapCodes (outQubit (n + code.1.length) (code.2.getD 0 0)) + +theorem isClassical_circuitCodes (n : ℕ) (code : List (Op × List ℕ) × List ℕ) : + IsClassical (n + code.1.length + 1) (circuitCodes n code) := by + refine IsClassical.append.mpr ⟨isClassical_codes le_rfl (by omega), ?_⟩ + split_ifs with h + · intro g hg + simp at hg + · exact isClassical_swapCodes (Nat.pos_of_ne_zero h) (by unfold outQubit; omega) + +/-- **The compiled circuit reads the De Morgan circuit's output**: started from the input `x` of +length `n`, it accepts with probability `1` when the first output wire of the code is true on `x`, +and `0` otherwise. -/ +theorem acceptProb_circuitCodes {n : ℕ} (code : List (Op × List ℕ) × List ℕ) {x : List Bool} + (hx : x.length = n) : + acceptProb (n + code.1.length + 1) (circuitCodes n code) x = + if evalOutput x code.1 (code.2.getD 0 0) then 1 else 0 := by + set W := n + code.1.length + 1 + set z := n + code.1.length + set o := code.2.getD 0 0 + have hX (p : ℕ) : readBit (inputState W x) p = x.getD p false := by + by_cases hp : p < W + · rw [readBit_of_lt _ hp] + rfl + · rw [readBit_of_le _ (not_lt.mp hp), List.getD_eq_getElem?_getD, + List.getElem?_eq_none (by omega)] + rfl + have hcodes := readBit_classicalRun_codes (W := W) (gates := code.1) le_rfl (by omega) hx hX + -- the compiled gates leave the output wire on `outQubit z o` + have hout : readBit (classicalRun (codes n z code.1) (inputState W x)) (outQubit z o) = + evalOutput x code.1 o := by + have hlen : (evalCode interpretation false x code.1).length = z := by simp [hx, z] + rw [hcodes, evalOutput] + unfold outQubit + rcases le_or_gt z o with h | h + · rw [min_eq_left h, List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, + List.getElem?_eq_none (by omega), List.getElem?_eq_none (by omega)] + · rw [min_eq_right h.le] + have h0 : 0 < W := by omega + -- qubit `0` of the final basis state + have hfinal : readBit (classicalRun (circuitCodes n code) (inputState W x)) 0 = + evalOutput x code.1 o := by + rw [circuitCodes, classicalRun_append] + split_ifs with h + · rw [classicalRun_nil, ← h, hout] + · rw [readBit_classicalRun_swapCodes (Nat.pos_of_ne_zero h) (by unfold outQubit; omega), hout] + have hmem : classicalRun (circuitCodes n code) (inputState W x) ∈ accepting W ↔ + evalOutput x code.1 o = true := by + rw [mem_accepting h0, + ← readBit_fin (classicalRun (circuitCodes n code) (inputState W x)) (⟨0, h0⟩ : Fin W)] + change readBit _ 0 = true ↔ _ + rw [hfinal] + rw [acceptProb, Circuit.run_ofCodes (isClassical_circuitCodes n code), measureProb_ket] + exact if_congr hmem rfl rfl + +variable {γ : Type} {enc : γ ↪ List Bool} + +/-- **The compilation of circuit codes runs in polynomial time.** -/ +theorem computableInPolyTime_circuitCodes {n : γ → ℕ} + {code : γ → List (Op × List ℕ) × List ℕ} (hn : ComputableInPolyTime n enc encUnary) + (hcode : ComputableInPolyTime code enc encCode) : + ComputableInPolyTime (fun c => circuitCodes (n c) (code c)) enc (encList encGateCode) := by + have hz : ComputableInPolyTime (fun c => n c + (code c).1.length) enc encUnary := by fun_prop + have hgates := computableInPolyTime_codes hn hz (gates := fun c => (code c).1) (by fun_prop) + have hout : ComputableInPolyTime (fun c => outQubit (n c + (code c).1.length) + ((code c).2.getD 0 0)) enc encUnary := by + unfold outQubit + fun_prop + simp only [circuitCodes, swapCodes] + fun_prop + +end Reversible + +namespace UniformCircuitFamily + +/-- **The quantum family of a polynomial-time uniform family of De Morgan circuits**: the circuit +for inputs of length `n` compiled into reversible gates. -/ +def ofBooleanCircuits (circuits : (n : ℕ) → Circuits.Circuit signature n 1) + (hcode : ComputableInPolyTime (fun n => (circuits n).code) encUnary encCode) : + UniformCircuitFamily where + width n := n + (circuits n).code.1.length + 1 + gates n := Reversible.circuitCodes n (circuits n).code + computableInPolyTime_width := by fun_prop + computableInPolyTime_gates := Reversible.computableInPolyTime_circuitCodes (by fun_prop) hcode + le_width n := by omega + width_pos n := by omega + wellFormed n g hg := (Reversible.isClassical_circuitCodes n _ g hg).2 + +/-- The family of compiled circuits accepts with probability `1` or `0`, according to the output of +the De Morgan circuit for the input's length. -/ +theorem acceptProb_ofBooleanCircuits (circuits : (n : ℕ) → Circuits.Circuit signature n 1) + (hcode : ComputableInPolyTime (fun n => (circuits n).code) encUnary encCode) (x : List Bool) : + (ofBooleanCircuits circuits hcode).acceptProb x = + if (circuits x.length).eval interpretation (fun i => x[i]) 0 then 1 else 0 := by + rw [acceptProb] + change Quantum.acceptProb (x.length + (circuits x.length).code.1.length + 1) + (Reversible.circuitCodes x.length (circuits x.length).code) x = _ + rw [Reversible.acceptProb_circuitCodes _ rfl, Circuits.Circuit.eval_eq_evalOutput, + show (List.ofFn fun i : Fin x.length => x[i]) = x from List.ofFn_getElem] + congr 3 + +end UniformCircuitFamily + +end Cslib.Quantum + +namespace Cslib.Complexity + +open Quantum Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} + +/-- **Exact quantum computation of polynomial-time Boolean functions**: a polynomial-time Boolean +function is computed by a polynomial-time uniform family of NOT, CNOT and Toffoli circuits that +accepts with probability `1` where the function is true and `0` where it is false. -/ +theorem exists_uniformCircuitFamily {f : α → Bool} (hf : ComputableInPolyTime f enc encBool) : + ∃ F : UniformCircuitFamily, ∀ a, F.acceptProb (enc a) = if f a then 1 else 0 := by + obtain ⟨circuits, hcode, hcorrect⟩ := CircuitValue.exists_uniformCircuits hf + exact ⟨UniformCircuitFamily.ofBooleanCircuits circuits hcode, fun a => by + rw [UniformCircuitFamily.acceptProb_ofBooleanCircuits, hcorrect]⟩ + +/-- **`P ⊆ BQP`**: deterministic polynomial time is contained in bounded-error quantum polynomial +time, with zero error. -/ +theorem P_subset_BQP : P enc ⊆ BQP enc := by + rintro A ⟨f, hf, hA⟩ + obtain ⟨F, hF⟩ := exists_uniformCircuitFamily hf + refine ⟨F, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ + · rw [hF, (hA a).mp ha] + norm_num + · rw [hF, show f a = false by simpa [hA a] using ha] + norm_num + +end Cslib.Complexity diff --git a/ComplexityTests/BQPClassical.lean b/ComplexityTests/BQPClassical.lean new file mode 100644 index 000000000..c4ff08297 --- /dev/null +++ b/ComplexityTests/BQPClassical.lean @@ -0,0 +1,46 @@ +/- +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.Classical +import Complexity.Computability.Complexity.Problems.CircuitValue + +/-! `P ⊆ BQP`: the reversible compilation of a concrete De Morgan gate list, its exact acceptance +probability, and the circuit value problem in `BQP`. -/ + +namespace ComplexityTests.BQPClassical + +open Cslib Cslib.Quantum Cslib.Complexity Cslib.Circuits Cslib.Circuits.Boolean + +/-- Exclusive or of the inputs `0, 1` as a De Morgan gate list: wire `2` is `x₀ ∨ x₁`, wire `3` is +`x₀ ∧ x₁`, wire `4` is `¬ x₀ ∧ x₁`, and wire `5` is their conjunction. -/ +def xorGates : List (Op × List ℕ) := [(.or, [0, 1]), (.and, [0, 1]), (.not, [3]), (.and, [2, 4])] + +-- Compiled onto `2 + 4 + 1` qubits, qubit `5` holds `x₀ ⊕ x₁`. +example : readBit (GateCode.classicalRun (Reversible.codes 2 6 xorGates) + (fun i : Fin 7 => decide (i = 0))) 5 = true := by decide +example : readBit (GateCode.classicalRun (Reversible.codes 2 6 xorGates) + (fun i : Fin 7 => decide (i.val < 2))) 5 = false := by decide + +-- A repeated argument compiles to a CNOT, and an argument naming a later wire reads `false`. +example : readBit (GateCode.classicalRun (Reversible.codes 1 3 [(.or, [0, 0]), (.and, [0, 7])]) + (fun i : Fin 4 => decide (i = 0))) 1 = true := by decide +example : readBit (GateCode.classicalRun (Reversible.codes 1 3 [(.or, [0, 0]), (.and, [0, 7])]) + (fun i : Fin 4 => decide (i = 0))) 2 = false := by decide + +-- The compiled exclusive or accepts `10` with certainty and rejects `11` with certainty. +example : acceptProb (2 + xorGates.length + 1) (Reversible.circuitCodes 2 (xorGates, [5])) + [true, false] = 1 := by + have h : evalOutput [true, false] xorGates 5 = true := by decide + exact (Reversible.acceptProb_circuitCodes (n := 2) (xorGates, [5]) rfl).trans (ite_eq_left h) +example : acceptProb (2 + xorGates.length + 1) (Reversible.circuitCodes 2 (xorGates, [5])) + [true, true] = 0 := by + have h : ¬evalOutput [true, true] xorGates 5 = true := by decide + exact (Reversible.acceptProb_circuitCodes (n := 2) (xorGates, [5]) rfl).trans (ite_eq_right h) + +/-- The circuit value problem is in `BQP`. -/ +example : CircuitValue ∈ BQP encCircuitValue := P_subset_BQP CircuitValue.mem_P + +end ComplexityTests.BQPClassical