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