From 6ff7baea753cee37a416bc3e964d97e5dc1a6e88 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 04:17:24 -0400 Subject: [PATCH 1/2] feat(QueryComplexity/Quantum): quantum query lower bounds by polynomials (#896) The polynomial method of Beals, Buhrman, Cleve, Mosca and de Wolf on the query model of #923: amplitudes after t queries have degree <= t, outcome probabilities degree <= 2T, hence adeg_eps(f) <= 2T, deg(f) <= 2T for exact algorithms, bs(f) <= 8T^2 (exact) and 16T^2 (error 1/3), D(f) <= 4096 T^6, and N <= 16T^2 for OR_N. NisanSzegedy gains the range-aware form needed for the constant 16. Search.lean and Grover.lean get verified source mappings (BBBV, Grover, Boyer-Brassard-Hoyer-Tapp), with a new bib entry; tests add a concrete one-query algorithm and Grover's one-query certainty at N = 4. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../QueryComplexity/NisanSzegedy.lean | 56 +++- .../QueryComplexity/Quantum/Grover.lean | 16 +- .../QueryComplexity/Quantum/Polynomial.lean | 281 ++++++++++++++++++ .../QueryComplexity/Quantum/Search.lean | 48 +-- ComplexityTests/QuantumGrover.lean | 13 + ComplexityTests/QuantumPolynomial.lean | 84 ++++++ references.bib | 13 + 8 files changed, 480 insertions(+), 32 deletions(-) create mode 100644 Complexity/Computability/QueryComplexity/Quantum/Polynomial.lean create mode 100644 ComplexityTests/QuantumPolynomial.lean diff --git a/Complexity.lean b/Complexity.lean index 3e9cd54e70..57d61db671 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2141,6 +2141,7 @@ public import Complexity.Computability.QueryComplexity.Monotone public import Complexity.Computability.QueryComplexity.NisanSzegedy public import Complexity.Computability.QueryComplexity.OneSided public import Complexity.Computability.QueryComplexity.Quantum.Grover +public import Complexity.Computability.QueryComplexity.Quantum.Polynomial public import Complexity.Computability.QueryComplexity.Quantum.Search public import Complexity.Computability.QueryComplexity.Randomized public import Complexity.Computability.QueryComplexity.Randomized.Nisan diff --git a/Complexity/Computability/QueryComplexity/NisanSzegedy.lean b/Complexity/Computability/QueryComplexity/NisanSzegedy.lean index f0f3463df3..cfb4c0ba31 100644 --- a/Complexity/Computability/QueryComplexity/NisanSzegedy.lean +++ b/Complexity/Computability/QueryComplexity/NisanSzegedy.lean @@ -33,7 +33,12 @@ function `g(y) = p(x ⊕ ⋃_{yⱼ = 1} Bⱼ)` on `{0,1}ᵇ` still has degree at most `D` with the same bounds at the integers `0, …, b`, and the mean value theorem gives a point of `[0, 1]` where `q' ≥ 1 - 2ε`. The Nisan–Szegedy lemma, a consequence of Markov's inequality (`Polynomial.mul_le_sq_mul_of_le_abs_eval_derivative`), then gives -`(1 - 2ε) b ≤ D² (1 - 2ε + 1 + 2ε) = 2 D²`. +`(1 - 2ε) b ≤ D² (1 - 2ε + 1 + 2ε) = 2 D²`. If `p` takes values in `[-δ, 1 + δ]`, the same +argument gives `(1 - 2ε) b ≤ (2 - 2ε + 2δ) D²` +(`QueryComplexity.one_sub_two_mul_mul_blockSensitivity_le_of_mem_Icc`). The case `δ = 0`, of a +polynomial that is a probability, is the step in the proof of Theorem 4.13 of +[BealsBuhrmanCleveMoscaDeWolf2001] (arXiv:quant-ph/9802049v3) that gives `bs(f) ≤ 16 T²` for +`T`-query quantum algorithms (`Cslib.Quantum.blockSensitivity_le_sixteen_mul_sq`). With Huang's theorem `deg(f) ≤ s(f)²` this gives `bs(f) ≤ 2 s(f)⁴`, and with `D(f) ≤ bs(f)³` [BealsBuhrmanCleveMoscaDeWolf2001] it gives `D(f) ≤ 216 adeg(f)⁶`. @@ -44,6 +49,8 @@ The sharper exact-degree bound `D(f) ≤ 2 deg(f)³` is proved in * `Cslib.QueryComplexity.one_sub_two_mul_mul_blockSensitivity_le_of_mem_lowDegree`: a real function of degree at most `D` within `ε` of `f` gives `(1 - 2ε) bs(f) ≤ 2 D²`. +* `Cslib.QueryComplexity.one_sub_two_mul_mul_blockSensitivity_le_of_mem_Icc`: if it also takes + values in `[-δ, 1 + δ]` and `ε < 1/2`, then `(1 - 2ε) bs(f) ≤ (2 - 2ε + 2δ) D²`. * `Cslib.QueryComplexity.blockSensitivity_le_two_mul_degree_sq`: `bs(f) ≤ 2 deg(f)²`. * `Cslib.QueryComplexity.one_sub_two_mul_mul_blockSensitivity_le`: `(1 - 2ε) bs(f) ≤ 2 adeg_ε(f)²`. @@ -117,13 +124,18 @@ private theorem bitVal_flipBlocks_mem_lowDegree {m : ℕ} {B : Fin m → Block n private theorem bitVal_mem_Icc (b : Bool) : bitVal ℝ b ∈ Set.Icc (0 : ℝ) 1 := by cases b <;> simp -/-- **The Nisan–Szegedy argument**: if a real function of degree at most `D` is within `ε` of `f` -at every input, then `(1 - 2ε) bs(f) ≤ 2 D²`. -/ -theorem one_sub_two_mul_mul_blockSensitivity_le_of_mem_lowDegree {p : BitString n → ℝ} {D : ℕ} - (hp : p ∈ lowDegree ℝ (Fin n) D) {ε : ℝ} (hpf : ∀ x, |p x - bitVal ℝ (f x)| ≤ ε) : - (1 - 2 * ε) * blockSensitivity f ≤ 2 * D ^ 2 := by - rcases le_or_gt (1 - 2 * ε) 0 with hε | hε - · exact (mul_nonpos_of_nonpos_of_nonneg hε (Nat.cast_nonneg _)).trans (by positivity) +/-- **The Nisan–Szegedy argument with a range**: if a real function of degree at most `D` is within +`ε < 1/2` of `f` at every input and takes values in `[-δ, 1 + δ]`, then +`(1 - 2ε) bs(f) ≤ (2 - 2ε + 2δ) D²`. A function within `ε` of `f` takes values in `[-ε, 1 + ε]`, +which gives `2 D²`; a probability, with values in `[0, 1]`, gives `(2 - 2ε) D²`. -/ +theorem one_sub_two_mul_mul_blockSensitivity_le_of_mem_Icc {p : BitString n → ℝ} {D : ℕ} + (hp : p ∈ lowDegree ℝ (Fin n) D) {ε δ : ℝ} (hpf : ∀ x, |p x - bitVal ℝ (f x)| ≤ ε) + (hpI : ∀ x, p x ∈ Set.Icc (-δ) (1 + δ)) (hε2 : 2 * ε < 1) : + (1 - 2 * ε) * blockSensitivity f ≤ (2 - 2 * ε + 2 * δ) * D ^ 2 := by + have hε : 0 < 1 - 2 * ε := by linarith + have hδ : 0 ≤ 2 - 2 * ε + 2 * δ := by + have := hpI fun _ => false + linarith [this.1, this.2] -- an input and a family of pairwise disjoint sensitive blocks attaining `bs(f)` obtain ⟨x, -, hx⟩ := exists_mem_eq_sup univ univ_nonempty (blockSensitivityAt f) obtain ⟨F, hF, hFcard⟩ := exists_mem_eq_sup (sensitiveFamilies f x) @@ -133,7 +145,7 @@ theorem one_sub_two_mul_mul_blockSensitivity_le_of_mem_lowDegree {p : BitString set m := #F rcases Nat.eq_zero_or_pos m with hm | hm · rw [hm, Nat.cast_zero, mul_zero] - positivity + exact mul_nonneg hδ (by positivity) set B : Fin m → Block n := fun j => (F.equivFin.symm j : Block n) have hBF (j : Fin m) : B j ∈ F := (F.equivFin.symm j).2 have hBinj : Function.Injective B := fun j j' h => @@ -160,10 +172,12 @@ theorem one_sub_two_mul_mul_blockSensitivity_le_of_mem_lowDegree {p : BitString set g : BitString m → ℝ := fun y => h (flipBlocks B x y) have hg : g ∈ lowDegree ℝ (Fin m) D := comp_mem_lowDegree (bitVal_flipBlocks_mem_lowDegree hB x) hh - have hgI (y : BitString m) : g y ∈ Set.Icc (-ε) (1 + ε) := by - have h₁ := abs_le.1 (hhf (flipBlocks B x y)) - have h₂ := bitVal_mem_Icc (f (flipBlocks B x y) ^^ f x) - exact ⟨by linarith [h₁.1, h₂.1], by linarith [h₁.2, h₂.2]⟩ + have hgI (y : BitString m) : g y ∈ Set.Icc (-δ) (1 + δ) := by + have h₁ := hpI (flipBlocks B x y) + simp only [g, h] + split_ifs + · exact ⟨by linarith [h₁.2], by linarith [h₁.1]⟩ + · exact h₁ have hg₀ (y : BitString m) (hy : weight y = 0) : g y ≤ ε := by have hy' : ({j | y j = true} : Finset (Fin m)) = ∅ := card_eq_zero.1 hy have := (abs_le.1 (hhf (flipBlocks B x y))).2 @@ -187,7 +201,7 @@ theorem one_sub_two_mul_mul_blockSensitivity_le_of_mem_lowDegree {p : BitString have hlayer {k : ℕ} (hk : k ≤ m) : ({x : BitString m | weight x = k} : Finset (BitString m)).Nonempty := weightLayer_nonempty hk - have hqI (k : ℕ) (hk : k ≤ m) : q.eval (k : ℝ) ∈ Set.Icc (-ε) (1 + ε) := by + have hqI (k : ℕ) (hk : k ≤ m) : q.eval (k : ℝ) ∈ Set.Icc (-δ) (1 + δ) := by rw [hq k (by rw [Fintype.card_fin]; exact hk), layerAverage] exact ⟨le_expect (hlayer hk) fun y _ => (hgI y).1, expect_le (hlayer hk) fun y _ => (hgI y).2⟩ @@ -212,6 +226,20 @@ theorem one_sub_two_mul_mul_blockSensitivity_le_of_mem_lowDegree {p : BitString (by rw [hξq]; exact (by linarith : 1 - 2 * ε ≤ q.eval 1 - q.eval 0).trans (le_abs_self _)) linarith +/-- **The Nisan–Szegedy argument**: if a real function of degree at most `D` is within `ε` of `f` +at every input, then `(1 - 2ε) bs(f) ≤ 2 D²`. -/ +theorem one_sub_two_mul_mul_blockSensitivity_le_of_mem_lowDegree {p : BitString n → ℝ} {D : ℕ} + (hp : p ∈ lowDegree ℝ (Fin n) D) {ε : ℝ} (hpf : ∀ x, |p x - bitVal ℝ (f x)| ≤ ε) : + (1 - 2 * ε) * blockSensitivity f ≤ 2 * D ^ 2 := by + rcases le_or_gt (1 - 2 * ε) 0 with hε | hε + · exact (mul_nonpos_of_nonpos_of_nonneg hε (Nat.cast_nonneg _)).trans (by positivity) + have := one_sub_two_mul_mul_blockSensitivity_le_of_mem_Icc hp hpf (δ := ε) (fun x => ?_) + (by linarith) + · linarith + · have h₁ := abs_le.1 (hpf x) + have h₂ := bitVal_mem_Icc (f x) + exact ⟨by linarith [h₁.1, h₂.1], by linarith [h₁.2, h₂.2]⟩ + /-- **Nisan–Szegedy**: `bs(f) ≤ 2 deg(f)²`. -/ theorem blockSensitivity_le_two_mul_degree_sq (f : BooleanFunction n) : blockSensitivity f ≤ 2 * degree f ^ 2 := by diff --git a/Complexity/Computability/QueryComplexity/Quantum/Grover.lean b/Complexity/Computability/QueryComplexity/Quantum/Grover.lean index 6269cf2b9c..2efb2c755c 100644 --- a/Complexity/Computability/QueryComplexity/Quantum/Grover.lean +++ b/Complexity/Computability/QueryComplexity/Quantum/Grover.lean @@ -30,6 +30,17 @@ and the uniform superposition of the other items. So `z` is measured with probab `(2k + 1) θ` lies within `θ` of `π / 2`, and the success probability is at least `1 - 1 / N` (`Cslib.Quantum.grover_success`). +**Source mapping.** The algorithm is Grover's (§3 of arXiv:quant-ph/9605043v3): it alternates the +inversion of the phase of the marked item with the diffusion transform `D_ij = 2/N` for `i ≠ j`, +`D_ii = -1 + 2/N` (equation (4.0)), the inversion about the average (§4). Grover takes `N = 2^n` +and implements `D = WRW` with Walsh–Hadamard transforms (Theorem 1 in §5); here `D` is the +reflection about `|s⟩` for every `N ≥ 2`, and only queries are counted. Grover shows a success +probability of at least `1/2` after `O(√N)` iterations. The closed form `sin((2k + 1) θ)` and the +choice `⌊π / (4θ)⌋`, with failure probability at most `1/N` and at most `π√N / 4` iterations, are +from [Boyer, Brassard, Høyer, Tapp][BoyerBrassardHoyerTapp1998] (numbering of +arXiv:quant-ph/9605034v1): §2, equation (2), and §3 with one solution. For `N = 4` the angle is +`π / 6` and one query succeeds with certainty, their §3.1. + ## Main definitions * `Cslib.Quantum.uniform`: the uniform superposition. @@ -46,6 +57,8 @@ and the uniform superposition of the other items. So `z` is measured with probab ## References * [L. K. Grover, *A Fast Quantum Mechanical Algorithm for Database Search*][Grover1996] +* [M. Boyer, G. Brassard, P. Høyer, A. Tapp, *Tight Bounds on Quantum + Searching*][BoyerBrassardHoyerTapp1998] -/ @[expose] public section @@ -224,7 +237,8 @@ theorem regProb_run_grover (hN : 2 ≤ N) (z : Fin N) (k : ℕ) : Complex.norm_real, Real.norm_eq_abs, sq_abs] ring -/-- **Grover's algorithm** [Grover][Grover1996]: for `N ≥ 2` and every `z`, with +/-- **Grover's algorithm** [Grover][Grover1996], with the analysis of [Boyer, Brassard, Høyer, +Tapp][BoyerBrassardHoyerTapp1998]: for `N ≥ 2` and every `z`, with `T = ⌊π / (4θ)⌋` queries, where `θ = arcsin(1 / √N)`, the algorithm outputs the marked item `z` with probability at least `1 - 1 / N`, and `T ≤ π √N / 4`. -/ theorem grover_success (hN : 2 ≤ N) (z : Fin N) : diff --git a/Complexity/Computability/QueryComplexity/Quantum/Polynomial.lean b/Complexity/Computability/QueryComplexity/Quantum/Polynomial.lean new file mode 100644 index 0000000000..e3e59530ac --- /dev/null +++ b/Complexity/Computability/QueryComplexity/Quantum/Polynomial.lean @@ -0,0 +1,281 @@ +/- +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.QueryComplexity.Quantum.Search +public import Complexity.Computability.QueryComplexity.NisanSzegedy +public import Complexity.Computability.QueryComplexity.Threshold + +/-! +# Quantum query lower bounds by polynomials + +The *polynomial method* of [Beals, Buhrman, Cleve, Mosca, de Wolf][BealsBuhrmanCleveMoscaDeWolf2001] +bounds the queries of a quantum algorithm below by the degree of a polynomial. In the query model +of `Cslib.Quantum.run`, each amplitude of the state after `t` queries is, as a function of the input +`x`, a complex function of degree at most `t` on the cube (`Cslib.Quantum.amplitude_mem_lowDegree`): +the oracle multiplies each amplitude by `1 - 2 b x_i`, of degree `1`, and the isometries between +queries take linear combinations of amplitudes, which keeps the degree. So the probability +`∑_{p ∈ S} |ψ_p|²` of measuring an outcome in a set `S` is a real function of degree at most `2T` +(`Cslib.Quantum.measureProb_run_mem_lowDegree`), the sum of the squares of the real and imaginary +parts of the amplitudes (`Cslib.BitString.re_mem_lowDegree`, `Cslib.BitString.im_mem_lowDegree`). + +An algorithm that accepts each input `x` with probability within `ε` of `f(x)` thus gives an +`ε`-approximation of `f` of degree at most `2T`, so `adeg_ε(f) ≤ 2T` +(`Cslib.Quantum.approxDegree_le_two_mul`), and `deg(f) ≤ 2T` if it computes `f` exactly +(`Cslib.Quantum.degree_le_two_mul`). The Nisan–Szegedy argument +(`Cslib.QueryComplexity.one_sub_two_mul_mul_blockSensitivity_le_of_mem_Icc`), applied to this +polynomial with values in `[0, 1]`, bounds the block sensitivity: `bs(f) ≤ 8 T²` for exact +algorithms and `bs(f) ≤ 16 T²` for error `1/3` (`Cslib.Quantum.blockSensitivity_le_eight_mul_sq`, +`Cslib.Quantum.blockSensitivity_le_sixteen_mul_sq`). +With `D(f) ≤ bs(f)³` a deterministic decision tree of depth at most `4096 T⁶` computes `f` +(`Cslib.Quantum.complexity_le_mul_pow_six`). Since `bs(OR_N) = N`, computing the disjunction of +`N` bits with error `1/3` takes `T ≥ √N / 4` queries (`Cslib.Quantum.card_le_sixteen_mul_sq`): the +decision form of the search lower bound, whose search form is the BBBV bound +`Cslib.Quantum.card_sub_two_le`. + +**Source mapping** (numbering of arXiv:quant-ph/9802049v3). The source models a network as +unitaries `U₀, O, U₁, …, O, U_T` on `m` qubits, where the query `O` maps `|i, b, z⟩` to +`|i, b ⊕ x_i, z⟩`, followed by a measurement of the final state (§3.2). Here the isometries are +arbitrary, the workspace is any finite type, and the oracle is the controlled phase oracle, which +is the bit oracle conjugated by Hadamard gates on the control bit (`Cslib.Quantum.phaseOracle`). +Lemma 4.1 is `amplitude_mem_lowDegree`, and Lemma 4.2 is `measureProb_run_mem_lowDegree`, for an +arbitrary set of outcomes. Theorem 4.3 (`Q_E(f) ≥ deg(f)/2`) is `degree_le_two_mul` and +Theorem 4.8 (`Q_2(f) ≥ adeg(f)/2`) is `approxDegree_le_two_mul`, for an arbitrary error `ε`. +Theorem 4.13 (`Q_E(f) ≥ √(bs(f)/8)` and `Q_2(f) ≥ √(bs(f)/16)`) is +`blockSensitivity_le_eight_mul_sq` and `blockSensitivity_le_sixteen_mul_sq`, and Theorem 5.4 +(`D(f) ≤ 4096 Q_2(f)⁶`) is `complexity_le_mul_pow_six`. The bound `√N / 4` for `OR_N` is +stated in §6. Like the source, these bounds hold for each algorithm; there is no separate +definition of quantum query complexity. + +## Main results + +* `Cslib.Quantum.amplitude_mem_lowDegree`: after `t` queries the amplitudes have degree at most + `t`. +* `Cslib.Quantum.measureProb_run_mem_lowDegree`: after `T` queries the probability of an outcome + set has degree at most `2T`. +* `Cslib.Quantum.approxDegree_le_two_mul`, `Cslib.Quantum.degree_le_two_mul`: `adeg_ε(f) ≤ 2T`, + and `deg(f) ≤ 2T` for exact algorithms. +* `Cslib.Quantum.blockSensitivity_le_eight_mul_sq`, + `Cslib.Quantum.blockSensitivity_le_sixteen_mul_sq`: `bs(f) ≤ 8 T²` for exact algorithms and + `bs(f) ≤ 16 T²` for error `1/3`. +* `Cslib.Quantum.complexity_le_mul_pow_six`: `D(f) ≤ 4096 T⁶` for error `1/3`. +* `Cslib.Quantum.card_le_sixteen_mul_sq`: computing `OR_N` with error `1/3` needs `N ≤ 16 T²`. + +## References + +* [R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, *Quantum lower bounds by + polynomials*][BealsBuhrmanCleveMoscaDeWolf2001] +* [N. Nisan, M. Szegedy, *On the degree of Boolean functions as real polynomials*][NisanSzegedy1994] +-/ + +public section + +namespace Cslib + +namespace BitString + +variable {ι : Type*} {D : ℕ} + +/-- The monomials over `ℂ` are the monomials over `ℝ`, which take the values `0` and `1`. -/ +private theorem monomial_complex (S : Finset ι) (x : ι → Bool) : + monomial ℂ S x = (monomial ℝ S x : ℂ) := by + rw [monomial_apply, monomial_apply] + split_ifs <;> simp + +/-- The real and imaginary parts of a complex function of degree at most `D` on the cube have +degree at most `D`. -/ +private theorem re_im_mem_lowDegree {f : (ι → Bool) → ℂ} (hf : f ∈ lowDegree ℂ ι D) : + (fun x => (f x).re) ∈ lowDegree ℝ ι D ∧ (fun x => (f x).im) ∈ lowDegree ℝ ι D := by + induction hf using Submodule.span_induction with + | mem g hg => + obtain ⟨S, hS, rfl⟩ := hg + simp only [monomial_complex, Complex.ofReal_re, Complex.ofReal_im] + exact ⟨monomial_mem_lowDegree hS, const_mem_lowDegree D 0⟩ + | zero => exact ⟨const_mem_lowDegree D 0, const_mem_lowDegree D 0⟩ + | add g h _ _ hg hh => + simp only [Pi.add_apply, Complex.add_re, Complex.add_im] + exact ⟨Submodule.add_mem _ hg.1 hh.1, Submodule.add_mem _ hg.2 hh.2⟩ + | smul c g _ hg => + simp only [Pi.smul_apply, smul_eq_mul, Complex.mul_re, Complex.mul_im] + exact ⟨Submodule.sub_mem _ (Submodule.smul_mem _ c.re hg.1) (Submodule.smul_mem _ c.im hg.2), + Submodule.add_mem _ (Submodule.smul_mem _ c.re hg.2) (Submodule.smul_mem _ c.im hg.1)⟩ + +/-- The real part of a complex function of degree at most `D` on the cube has degree at most +`D`. -/ +theorem re_mem_lowDegree {f : (ι → Bool) → ℂ} (hf : f ∈ lowDegree ℂ ι D) : + (fun x => (f x).re) ∈ lowDegree ℝ ι D := + (re_im_mem_lowDegree hf).1 + +/-- The imaginary part of a complex function of degree at most `D` on the cube has degree at most +`D`. -/ +theorem im_mem_lowDegree {f : (ι → Bool) → ℂ} (hf : f ∈ lowDegree ℂ ι D) : + (fun x => (f x).im) ∈ lowDegree ℝ ι D := + (re_im_mem_lowDegree hf).2 + +end BitString + +namespace Quantum + +open Finset BitString QueryComplexity + +variable {N : ℕ} {W : Type*} [Fintype W] + +/-- A linear map of a finite-dimensional Euclidean space takes each coordinate to a linear +combination of the coordinates of its argument. -/ +private theorem linearMap_apply_eq_sum {ι : Type*} [Fintype ι] [DecidableEq ι] + (L : EuclideanSpace ℂ ι →ₗ[ℂ] EuclideanSpace ℂ ι) (ψ : EuclideanSpace ℂ ι) (p : ι) : + (L ψ).ofLp p = ∑ q, (L (EuclideanSpace.single q 1)).ofLp p * ψ.ofLp q := by + conv_lhs => rw [← (EuclideanSpace.basisFun ι ℂ).sum_repr ψ] + simp [map_sum, map_smul, mul_comm] + +/-- **The amplitudes after `t` queries are polynomials of degree at most `t`** +[Beals, Buhrman, Cleve, Mosca, de Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: for every basis state +`p`, the amplitude of `p` after `t` queries is, as a function of the input, a complex function of +degree at most `t` on the cube. -/ +theorem amplitude_mem_lowDegree (U : ℕ → State N W →ₗᵢ[ℂ] State N W) (ψ₀ : State N W) (t : ℕ) + (p : Fin N × Bool × W) : + (fun x => (run U ψ₀ x t).ofLp p) ∈ lowDegree ℂ (Fin N) t := by + classical + induction t generalizing p with + | zero => exact const_mem_lowDegree (R := ℂ) (ι := Fin N) 0 ((U 0 ψ₀).ofLp p) + | succ t ih => + have h : (fun x => (run U ψ₀ x (t + 1)).ofLp p) = ∑ q, fun x => + (U (t + 1) (EuclideanSpace.single q 1)).ofLp p * + ((if q.2.1 && x q.1 then -1 else 1) * (run U ψ₀ x t).ofLp q) := by + funext x + have := linearMap_apply_eq_sum (U (t + 1)).toLinearMap (phaseOracle x (run U ψ₀ x t)) p + simp only [LinearIsometry.coe_toLinearMap] at this + simp only [run, Finset.sum_apply, this, phaseOracle_apply] + rw [h] + refine sum_mem_lowDegree _ fun q _ => ?_ + obtain ⟨i, b, w⟩ := q + have hfac : (fun x : Fin N → Bool => (if b && x i then -1 else 1 : ℂ)) ∈ + lowDegree ℂ (Fin N) 1 := by + cases b + · simpa using const_mem_lowDegree (R := ℂ) (ι := Fin N) 1 1 + · convert Submodule.sub_mem _ (one_mem_lowDegree (R := ℂ) (ι := Fin N) 1) + (Submodule.smul_mem _ (2 : ℂ) (bitVal_mem_lowDegree (R := ℂ) i)) using 1 + funext x + cases hx : x i <;> norm_num [bitVal, hx] + have := Submodule.smul_mem _ ((U (t + 1) (EuclideanSpace.single (i, b, w) 1)).ofLp p) + (mul_mem_lowDegree hfac (ih (i, b, w))) + rw [Nat.add_comm 1 t] at this + exact this + +/-- **The acceptance probability after `T` queries is a polynomial of degree at most `2T`** +[Beals, Buhrman, Cleve, Mosca, de Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: for every set `S` of +outcomes, the probability that measuring the state after `T` queries gives an outcome in `S` is, as +a function of the input, a real function of degree at most `2T` on the cube. -/ +theorem measureProb_run_mem_lowDegree (U : ℕ → State N W →ₗᵢ[ℂ] State N W) (ψ₀ : State N W) + (T : ℕ) (S : Finset (Fin N × Bool × W)) : + (fun x => measureProb (run U ψ₀ x T) S) ∈ lowDegree ℝ (Fin N) (2 * T) := by + have h : (fun x => measureProb (run U ψ₀ x T) S) = ∑ p ∈ S, + ((fun x => ((run U ψ₀ x T).ofLp p).re) ^ 2 + (fun x => ((run U ψ₀ x T).ofLp p).im) ^ 2) := by + funext x + simp only [measureProb, Finset.sum_apply, Pi.add_apply, Pi.pow_apply, Complex.sq_norm, + Complex.normSq_apply] + refine sum_congr rfl fun p _ => ?_ + ring + rw [h] + exact sum_mem_lowDegree _ fun p _ => Submodule.add_mem _ + (pow_mem_lowDegree (re_mem_lowDegree (amplitude_mem_lowDegree U ψ₀ T p)) 2) + (pow_mem_lowDegree (im_mem_lowDegree (amplitude_mem_lowDegree U ψ₀ T p)) 2) + +/-- For a unit initial state, the probability of an outcome set lies in `[0, 1]`. -/ +private theorem measureProb_run_mem_Icc (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} + (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) (S : Finset (Fin N × Bool × W)) (x : Fin N → Bool) : + measureProb (run U ψ₀ x T) S ∈ Set.Icc (-0 : ℝ) (1 + 0) := by + refine ⟨by simpa using measureProb_nonneg _ S, ?_⟩ + have := measureProb_le_measureProb_univ (run U ψ₀ x T) S + rw [measureProb_univ, norm_run, hψ₀] at this + simpa using this + +/-- **Approximate degree bounds quantum queries** [Beals, Buhrman, Cleve, Mosca, de +Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: if a `T`-query algorithm accepts every input `x`, by an +outcome in `S`, with probability within `ε` of `f(x)`, then `adeg_ε(f) ≤ 2T`. -/ +theorem approxDegree_le_two_mul {f : BooleanFunction N} {ε : ℝ} + (U : ℕ → State N W →ₗᵢ[ℂ] State N W) (ψ₀ : State N W) (T : ℕ) + (S : Finset (Fin N × Bool × W)) + (h : ∀ x, |measureProb (run U ψ₀ x T) S - bitVal ℝ (f x)| ≤ ε) : + approxDegree ε f ≤ 2 * T := + approxDegree_le_of_mem_lowDegree (measureProb_run_mem_lowDegree U ψ₀ T S) h + +/-- **Degree bounds exact quantum queries** [Beals, Buhrman, Cleve, Mosca, de +Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: if a `T`-query algorithm accepts every input `x`, by an +outcome in `S`, with probability exactly `f(x)`, then `deg(f) ≤ 2T`. -/ +theorem degree_le_two_mul {f : BooleanFunction N} (U : ℕ → State N W →ₗᵢ[ℂ] State N W) + (ψ₀ : State N W) (T : ℕ) (S : Finset (Fin N × Bool × W)) + (h : ∀ x, measureProb (run U ψ₀ x T) S = bitVal ℝ (f x)) : + degree f ≤ 2 * T := by + have := approxDegree_le_two_mul (f := f) (ε := 0) U ψ₀ T S fun x => by simp [h x] + rwa [approxDegree_zero] at this + +/-- **Block sensitivity bounds exact quantum queries** [Beals, Buhrman, Cleve, Mosca, de +Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: if a `T`-query algorithm accepts every input `x`, by an +outcome in `S`, with probability exactly `f(x)`, then `bs(f) ≤ 8 T²`. -/ +theorem blockSensitivity_le_eight_mul_sq {f : BooleanFunction N} + (U : ℕ → State N W →ₗᵢ[ℂ] State N W) (ψ₀ : State N W) (T : ℕ) + (S : Finset (Fin N × Bool × W)) (h : ∀ x, measureProb (run U ψ₀ x T) S = bitVal ℝ (f x)) : + blockSensitivity f ≤ 8 * T ^ 2 := + (blockSensitivity_le_two_mul_degree_sq f).trans <| by + have := Nat.pow_le_pow_left (degree_le_two_mul U ψ₀ T S h) 2 + rw [mul_pow] at this + omega + +/-- **Block sensitivity bounds bounded-error quantum queries**: if a `T`-query algorithm with a unit +initial state accepts every input `x`, by an outcome in `S`, with probability within `ε < 1/2` of +`f(x)`, then `(1 - 2ε) bs(f) ≤ 8 (1 - ε) T²`. -/ +theorem one_sub_two_mul_mul_blockSensitivity_le {f : BooleanFunction N} {ε : ℝ} + (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) + (S : Finset (Fin N × Bool × W)) (h : ∀ x, |measureProb (run U ψ₀ x T) S - bitVal ℝ (f x)| ≤ ε) + (hε : 2 * ε < 1) : + (1 - 2 * ε) * blockSensitivity f ≤ 8 * (1 - ε) * T ^ 2 := by + have := one_sub_two_mul_mul_blockSensitivity_le_of_mem_Icc + (measureProb_run_mem_lowDegree U ψ₀ T S) h (measureProb_run_mem_Icc U hψ₀ T S) hε + push_cast at this + linarith + +/-- **Block sensitivity bounds bounded-error quantum queries** [Beals, Buhrman, Cleve, Mosca, de +Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: if a `T`-query algorithm with a unit initial state accepts +every input `x`, by an outcome in `S`, with probability within `1/3` of `f(x)`, then +`bs(f) ≤ 16 T²`. -/ +theorem blockSensitivity_le_sixteen_mul_sq {f : BooleanFunction N} + (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) + (S : Finset (Fin N × Bool × W)) + (h : ∀ x, |measureProb (run U ψ₀ x T) S - bitVal ℝ (f x)| ≤ 1 / 3) : + blockSensitivity f ≤ 16 * T ^ 2 := by + have := Quantum.one_sub_two_mul_mul_blockSensitivity_le U hψ₀ T S h (by norm_num) + have h' : (blockSensitivity f : ℝ) ≤ 16 * T ^ 2 := by linarith + exact_mod_cast h' + +/-- **Deterministic simulation of bounded-error quantum queries** [Beals, Buhrman, Cleve, Mosca, +de Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: if a `T`-query algorithm with a unit initial state +accepts every input `x`, by an outcome in `S`, with probability within `1/3` of `f(x)`, then a +deterministic decision tree of depth at most `4096 T⁶` computes `f`. -/ +theorem complexity_le_mul_pow_six {f : BooleanFunction N} + (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) + (S : Finset (Fin N × Bool × W)) + (h : ∀ x, |measureProb (run U ψ₀ x T) S - bitVal ℝ (f x)| ≤ 1 / 3) : + DecisionTree.complexity f ≤ 4096 * T ^ 6 := + (DecisionTree.complexity_le_blockSensitivity_pow_three f).trans + ((Nat.pow_le_pow_left (blockSensitivity_le_sixteen_mul_sq U hψ₀ T S h) 3).trans_eq (by ring)) + +/-- **The search lower bound, decision form** [Beals, Buhrman, Cleve, Mosca, de +Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: if a `T`-query algorithm with a unit initial state +computes the disjunction `OR_N` of its `N` input bits with error at most `1/3`, accepting every +input `x`, by an outcome in `S`, with probability within `1/3` of `OR_N(x)`, then `N ≤ 16 T²`. -/ +theorem card_le_sixteen_mul_sq (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} + (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) (S : Finset (Fin N × Bool × W)) + (h : ∀ x, |measureProb (run U ψ₀ x T) S - bitVal ℝ (threshold N 1 x)| ≤ 1 / 3) : + N ≤ 16 * T ^ 2 := + blockSensitivity_threshold_one_right.symm.trans_le + (blockSensitivity_le_sixteen_mul_sq U hψ₀ T S h) + +end Quantum + +end Cslib diff --git a/Complexity/Computability/QueryComplexity/Quantum/Search.lean b/Complexity/Computability/QueryComplexity/Quantum/Search.lean index f411495aab..77860fbcae 100644 --- a/Complexity/Computability/QueryComplexity/Quantum/Search.lean +++ b/Complexity/Computability/QueryComplexity/Quantum/Search.lean @@ -19,24 +19,38 @@ linear isometries `U₀, …, U_T` of a finite-dimensional state space `ℂ^{Fin query register, a control bit and a workspace `W`, with `T` applications of the *controlled phase oracle* `O_x |i, b, w⟩ = (-1)^{b · x_i} |i, b, w⟩` (`Cslib.Quantum.phaseOracle`, `Cslib.Quantum.run`). Up to Hadamard gates on the control bit this is the standard bit oracle -`|i, b⟩ ↦ |i, b ⊕ x_i⟩`, so the model is the standard one of [Bennett, Bernstein, Brassard, -Vazirani][BBBV1997]. Its output is the measurement of the query register: the probability of -outcome `i` is `∑_{b, w} |ψ(i, b, w)|²` (`Cslib.Quantum.regProb`). - -**Bennett–Bernstein–Brassard–Vazirani.** Searching for a single marked item among `N` takes -`Ω(√N)` queries: if, for every `z`, the algorithm outputs `z` with probability at least `2 / 3` on -the input `e_z` marking only `z`, then `N - 2 ≤ 144 T²` (`Cslib.Quantum.card_sub_two_le`) -[Bennett, Bernstein, Brassard, Vazirani][BBBV1997]. - -The proof is the hybrid argument. On the all-zero input the oracle is the identity; replacing it by -`O_{e_z}` at one query moves the state by `2 ‖Π_z φ‖`, where `Π_z` projects onto query index `z` -with control bit `1` (`Cslib.Quantum.ctrlProj`) and `φ` is the state before that query. So the -final states differ by at most `2 ∑_{t < T} ‖Π_z φ_t‖`, and by Cauchy–Schwarz and -`∑_z ‖Π_z φ‖² ≤ ‖φ‖² = 1`, +`|i, b⟩ ↦ |i, b ⊕ x_i⟩`, so the model is the standard quantum query model. Its output is the +measurement of the query register: the probability of outcome `i` is `∑_{b, w} |ψ(i, b, w)|²` +(`Cslib.Quantum.regProb`). + +**The search lower bound.** Searching for a single marked item among `N` takes `Ω(√N)` queries: +if, for every `z`, the algorithm outputs `z` with probability at least `2 / 3` on the input `e_z` +marking only `z`, then `N - 2 ≤ 144 T²` (`Cslib.Quantum.card_sub_two_le`). The proof is the +hybrid argument of [Bennett, Bernstein, Brassard, Vazirani][BBBV1997]. + +On the all-zero input the oracle is the identity; replacing it by `O_{e_z}` at one query moves +the state by `2 ‖Π_z φ‖`, where `Π_z` projects onto query index `z` with control bit `1` +(`Cslib.Quantum.ctrlProj`) and `φ` is the state before that query. So the final states differ by +at most `2 ∑_{t < T} ‖Π_z φ_t‖`, and by Cauchy–Schwarz and `∑_z ‖Π_z φ‖² ≤ ‖φ‖² = 1`, `∑_z ‖ψ_T^{e_z} - ψ_T^0‖² ≤ 4 T²` (`Cslib.Quantum.sum_sq_norm_run_sub_le`). Success on `e_z` but not on the all-zero input, for all but at most two `z`, forces each of these distances to be at least `1 / 6`. +**Source mapping** (numbering of arXiv:quant-ph/9701001v1, the preprint of [BBBV1997]). The source +works with oracle quantum Turing machines. Its query magnitude `q_y(|φ_i⟩)` (Definition 3.2) is +the squared norm of the part of the state that queries `y`; here this is `‖ctrlProj z φ‖²`, the +part with query index `z` and control bit `1`, which is the part the oracle of `e_z` acts on. +Theorem 3.3 bounds how far the final state moves when the answers to a set of queries of small +total query magnitude are changed; `norm_run_sub_le` is the case of the query `z` at every time, +in the triangle-inequality form `2 ∑_s ‖Π_z φ_s‖`, and `sum_sq_norm_run_sub_le` adds +Cauchy–Schwarz and `∑_z q_z ≤ 1`, as in the proof of Corollary 3.4. Theorem 3.1 compares the +outcome distributions of nearby states (total variation at most `4ε`); `regProb_sub_le` is the +per-outcome bound used here. The source applies Corollary 3.4 to prove that relative to a random +oracle `NP` is not contained in `BQTime(o(2^{n/2}))` (Theorem 3.5), which is not formalized here; +`card_sub_two_le` is the search lower bound in its standard query-model form, with the constants +of this proof. The decision form, for computing `OR_N`, is `Cslib.Quantum.card_le_sixteen_mul_sq`, +by the polynomial method. + ## Main definitions * `Cslib.Quantum.phaseOracle`: the controlled phase oracle of `x`. @@ -258,9 +272,9 @@ theorem regProb_sub_le {ψ φ : State N W} (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ have h3 : 0 ≤ ‖proj z ψ‖ + ‖proj z φ‖ := by positivity nlinarith [norm_nonneg (ψ - φ), norm_nonneg (proj z ψ), norm_nonneg (proj z φ)] -/-- **The BBBV lower bound for search** [Bennett, Bernstein, Brassard, Vazirani][BBBV1997]: if a -`T`-query algorithm with a unit initial state outputs `z` with probability at least `2 / 3` on the -input marking only `z`, for every `z`, then `N - 2 ≤ 144 T²`. -/ +/-- **The quantum search lower bound** by the hybrid argument of [Bennett, Bernstein, Brassard, +Vazirani][BBBV1997]: if a `T`-query algorithm with a unit initial state outputs `z` with probability +at least `2 / 3` on the input marking only `z`, for every `z`, then `N - 2 ≤ 144 T²`. -/ theorem card_sub_two_le (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) (hsucc : ∀ z, 2 / 3 ≤ regProb (run U ψ₀ (marked z) T) z) : (N : ℝ) - 2 ≤ 144 * (T : ℝ) ^ 2 := by diff --git a/ComplexityTests/QuantumGrover.lean b/ComplexityTests/QuantumGrover.lean index ede547df1a..9f047f8074 100644 --- a/ComplexityTests/QuantumGrover.lean +++ b/ComplexityTests/QuantumGrover.lean @@ -33,4 +33,17 @@ example (z : Fin 4) : regProb (run (grover 4) (uniform 4) (marked z) 0) z = Real.sin (groverAngle 4) ^ 2 := by simpa using regProb_run_grover (by norm_num) z 0 +-- With `N = 4` the Grover angle is `arcsin(1/2) = π / 6`, so `(2 · 1 + 1) θ = π / 2`: a single +-- query finds the marked item with certainty. +theorem groverAngle_four : groverAngle 4 = Real.pi / 6 := by + have h : (Real.sqrt ((4 : ℕ) : ℝ))⁻¹ = Real.sin (Real.pi / 6) := by + rw [Real.sin_pi_div_six, show ((4 : ℕ) : ℝ) = 2 ^ 2 by norm_num, Real.sqrt_sq (by norm_num)] + norm_num + rw [groverAngle, h, Real.arcsin_sin] <;> linarith [Real.pi_pos] + +example (z : Fin 4) : regProb (run (grover 4) (uniform 4) (marked z) 1) z = 1 := by + rw [regProb_run_grover (by norm_num), groverAngle_four, + show (2 * ((1 : ℕ) : ℝ) + 1) * (Real.pi / 6) = Real.pi / 2 by push_cast; ring, + Real.sin_pi_div_two, one_pow] + end ComplexityTests.QuantumGrover diff --git a/ComplexityTests/QuantumPolynomial.lean b/ComplexityTests/QuantumPolynomial.lean new file mode 100644 index 0000000000..d91889770e --- /dev/null +++ b/ComplexityTests/QuantumPolynomial.lean @@ -0,0 +1,84 @@ +/- +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.QueryComplexity.Quantum.Polynomial +import Complexity.Computability.Circuit.Quantum.Basic + +/-! The polynomial method: a one-query algorithm that reads its input bit exactly, so the +hypotheses of the lower bounds are satisfiable by a non-constant function. -/ + +namespace ComplexityTests.QuantumPolynomial + +open Cslib Cslib.Quantum Cslib.BitString Cslib.QueryComplexity + +/-- With one query index and a trivial workspace, a basis state is determined by its control bit. -/ +def ctrl : Fin 1 × Bool × Unit ≃ Bool := + (Equiv.uniqueProd (Bool × Unit) (Fin 1)).trans (Equiv.prodUnique Bool Unit) + +/-- The Hadamard gate on the control bit. -/ +noncomputable def hadamardCtrl : State 1 Unit →ₗᵢ[ℂ] State 1 Unit := + (unitaryEquiv ⟨Gate.hadamardMatrix.submatrix ctrl ctrl, + Matrix.submatrix_equiv_mem_unitary.mpr Gate.hadamardMatrix_mem_unitaryGroup⟩).toLinearIsometry + +/-- The one-query algorithm `H O_x H |0, 0⟩`, which ends in `|0, x₀⟩`. -/ +noncomputable def readBit : ℕ → State 1 Unit →ₗᵢ[ℂ] State 1 Unit := fun _ => hadamardCtrl + +/-- The initial state `|0, 0, ()⟩`. -/ +noncomputable def ψ₀ : State 1 Unit := ket (0, false, ()) + +theorem norm_ψ₀ : ‖ψ₀‖ = 1 := norm_ket _ + +/-- The accepting outcome: control bit `1`. -/ +def accept : Finset (Fin 1 × Bool × Unit) := {(0, true, ())} + +private theorem inv_sqrt_two_mul_self : ((Real.sqrt 2)⁻¹ : ℂ) * ((Real.sqrt 2)⁻¹ : ℂ) = 1 / 2 := by + rw [← mul_inv, ← Complex.ofReal_mul, Real.mul_self_sqrt (by norm_num)] + norm_num + +/-- The algorithm accepts with probability exactly `x₀`. -/ +theorem measureProb_readBit (x : Fin 1 → Bool) : + measureProb (run readBit ψ₀ x 1) accept = bitVal ℝ (x 0) := by + have hamp : (run readBit ψ₀ x 1).ofLp (0, true, ()) = bitVal ℂ (x 0) := by + simp only [run, readBit, hadamardCtrl, LinearIsometryEquiv.coe_toLinearIsometry, + unitaryEquiv_apply, Matrix.mulVec, dotProduct, phaseOracle_apply, ψ₀, ket_apply, + Fintype.sum_prod_type, Fin.sum_univ_one, Fintype.sum_bool, Fintype.univ_unit, + Finset.sum_singleton, Matrix.submatrix_apply, ctrl, Equiv.trans_apply, + Equiv.uniqueProd_apply, Equiv.prodUnique_apply, Gate.hadamardMatrix] + cases x 0 + · simp [bitVal] + · simp only [Bool.and_self, ↓reduceIte, Complex.ofReal_inv, neg_mul, one_mul, Fin.isValue, + Prod.mk.injEq, Bool.true_eq_false, and_true, and_false, mul_zero, Bool.and_false, + Bool.false_eq_true, mul_one, zero_add, mul_neg, neg_neg, Bool.and_true, bitVal] + linear_combination 2 * inv_sqrt_two_mul_self + rw [measureProb, accept, Finset.sum_singleton, hamp] + cases x 0 <;> simp [bitVal] + +/-- The algorithm computes the disjunction of one bit exactly. -/ +theorem measureProb_readBit_threshold (x : Fin 1 → Bool) : + measureProb (run readBit ψ₀ x 1) accept = bitVal ℝ (threshold 1 1 x) := by + rw [measureProb_readBit] + congr 1 + cases hx : x 0 <;> simp [threshold, weight, hx, Finset.filter_singleton] + +-- The exact and bounded-error bounds apply to it. +example : degree (threshold 1 1) ≤ 2 * 1 := + degree_le_two_mul readBit ψ₀ 1 accept measureProb_readBit_threshold + +example : blockSensitivity (threshold 1 1) ≤ 8 * 1 ^ 2 := + blockSensitivity_le_eight_mul_sq readBit ψ₀ 1 accept measureProb_readBit_threshold + +example : 1 ≤ 16 * 1 ^ 2 := + card_le_sixteen_mul_sq readBit norm_ψ₀ 1 accept fun x => by + rw [measureProb_readBit_threshold] + norm_num + +-- The acceptance probability of any algorithm is a polynomial of degree at most `2T`. +example (W : Type) [Fintype W] (U : ℕ → State 3 W →ₗᵢ[ℂ] State 3 W) (ψ : State 3 W) + (S : Finset (Fin 3 × Bool × W)) : + (fun x => measureProb (run U ψ x 2) S) ∈ lowDegree ℝ (Fin 3) 4 := + measureProb_run_mem_lowDegree U ψ 2 S + +end ComplexityTests.QuantumPolynomial diff --git a/references.bib b/references.bib index be4a34de03..bd6902b1f2 100644 --- a/references.bib +++ b/references.bib @@ -831,6 +831,19 @@ @phdthesis{Boyack1985 url = {https://people.csail.mit.edu/rivest/student-theses/phd-1985-boyack.pdf} } +@article{BoyerBrassardHoyerTapp1998, + author = {Boyer, Michel and Brassard, Gilles and H{\o}yer, Peter and Tapp, Alain}, + title = {Tight Bounds on Quantum Searching}, + journal = {Fortschritte der Physik}, + volume = {46}, + number = {4--5}, + pages = {493--505}, + year = {1998}, + doi = {10.1002/(SICI)1521-3978(199806)46:4/5<493::AID-PROP493>3.0.CO;2-P}, + eprint = {quant-ph/9605034}, + archivePrefix = {arXiv} +} + @article{Braverman2010, author = {Braverman, Mark}, title = {Polylogarithmic Independence Fools {AC$^0$} Circuits}, From 6b08129b34207eabd13458d64d9ee1ca15b4359a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 04:21:29 -0400 Subject: [PATCH 2/2] feat(QueryComplexity/Quantum): exact parity needs N/2 quantum queries Corollary of deg(PARITY_N) = N and Theorem 4.3 of Beals et al.; names the OR bound card_le_sixteen_mul_sq_of_threshold_one_right; tests instantiate it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../QueryComplexity/Quantum/Polynomial.lean | 31 +++++++++++++------ .../QueryComplexity/Quantum/Search.lean | 4 +-- ComplexityTests/QuantumPolynomial.lean | 9 +++++- 3 files changed, 32 insertions(+), 12 deletions(-) diff --git a/Complexity/Computability/QueryComplexity/Quantum/Polynomial.lean b/Complexity/Computability/QueryComplexity/Quantum/Polynomial.lean index e3e59530ac..8a79c6509c 100644 --- a/Complexity/Computability/QueryComplexity/Quantum/Polynomial.lean +++ b/Complexity/Computability/QueryComplexity/Quantum/Polynomial.lean @@ -34,9 +34,11 @@ algorithms and `bs(f) ≤ 16 T²` for error `1/3` (`Cslib.Quantum.blockSensitivi `Cslib.Quantum.blockSensitivity_le_sixteen_mul_sq`). With `D(f) ≤ bs(f)³` a deterministic decision tree of depth at most `4096 T⁶` computes `f` (`Cslib.Quantum.complexity_le_mul_pow_six`). Since `bs(OR_N) = N`, computing the disjunction of -`N` bits with error `1/3` takes `T ≥ √N / 4` queries (`Cslib.Quantum.card_le_sixteen_mul_sq`): the -decision form of the search lower bound, whose search form is the BBBV bound -`Cslib.Quantum.card_sub_two_le`. +`N` bits with error `1/3` takes `T ≥ √N / 4` queries +(`Cslib.Quantum.card_le_sixteen_mul_sq_of_threshold_one_right`): the decision form of the search +lower bound, whose search form is the BBBV bound `Cslib.Quantum.card_sub_two_le`. Since +`deg(PARITY_N) = N`, computing the parity of `N` bits exactly takes `T ≥ N / 2` queries +(`Cslib.Quantum.card_le_two_mul_of_parity`). **Source mapping** (numbering of arXiv:quant-ph/9802049v3). The source models a network as unitaries `U₀, O, U₁, …, O, U_T` on `m` qubits, where the query `O` maps `|i, b, z⟩` to @@ -48,9 +50,9 @@ arbitrary set of outcomes. Theorem 4.3 (`Q_E(f) ≥ deg(f)/2`) is `degree_le_two Theorem 4.8 (`Q_2(f) ≥ adeg(f)/2`) is `approxDegree_le_two_mul`, for an arbitrary error `ε`. Theorem 4.13 (`Q_E(f) ≥ √(bs(f)/8)` and `Q_2(f) ≥ √(bs(f)/16)`) is `blockSensitivity_le_eight_mul_sq` and `blockSensitivity_le_sixteen_mul_sq`, and Theorem 5.4 -(`D(f) ≤ 4096 Q_2(f)⁶`) is `complexity_le_mul_pow_six`. The bound `√N / 4` for `OR_N` is -stated in §6. Like the source, these bounds hold for each algorithm; there is no separate -definition of quantum query complexity. +(`D(f) ≤ 4096 Q_2(f)⁶`) is `complexity_le_mul_pow_six`. The bound `√N / 4` for `OR_N` and the +bound `N / 2` for exact `PARITY_N` are stated in §6. Like the source, these bounds hold for each +algorithm; there is no separate definition of quantum query complexity. ## Main results @@ -64,7 +66,9 @@ definition of quantum query complexity. `Cslib.Quantum.blockSensitivity_le_sixteen_mul_sq`: `bs(f) ≤ 8 T²` for exact algorithms and `bs(f) ≤ 16 T²` for error `1/3`. * `Cslib.Quantum.complexity_le_mul_pow_six`: `D(f) ≤ 4096 T⁶` for error `1/3`. -* `Cslib.Quantum.card_le_sixteen_mul_sq`: computing `OR_N` with error `1/3` needs `N ≤ 16 T²`. +* `Cslib.Quantum.card_le_sixteen_mul_sq_of_threshold_one_right`: computing `OR_N` with error `1/3` + needs `N ≤ 16 T²`. +* `Cslib.Quantum.card_le_two_mul_of_parity`: computing `PARITY_N` exactly needs `N ≤ 2T`. ## References @@ -269,13 +273,22 @@ theorem complexity_le_mul_pow_six {f : BooleanFunction N} Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: if a `T`-query algorithm with a unit initial state computes the disjunction `OR_N` of its `N` input bits with error at most `1/3`, accepting every input `x`, by an outcome in `S`, with probability within `1/3` of `OR_N(x)`, then `N ≤ 16 T²`. -/ -theorem card_le_sixteen_mul_sq (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} - (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) (S : Finset (Fin N × Bool × W)) +theorem card_le_sixteen_mul_sq_of_threshold_one_right (U : ℕ → State N W →ₗᵢ[ℂ] State N W) + {ψ₀ : State N W} (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) (S : Finset (Fin N × Bool × W)) (h : ∀ x, |measureProb (run U ψ₀ x T) S - bitVal ℝ (threshold N 1 x)| ≤ 1 / 3) : N ≤ 16 * T ^ 2 := blockSensitivity_threshold_one_right.symm.trans_le (blockSensitivity_le_sixteen_mul_sq U hψ₀ T S h) +/-- **Exact parity takes `N / 2` queries** [Beals, Buhrman, Cleve, Mosca, de +Wolf][BealsBuhrmanCleveMoscaDeWolf2001]: if a `T`-query algorithm accepts every input `x`, by an +outcome in `S`, with probability exactly the parity of `x`, then `N ≤ 2T`. -/ +theorem card_le_two_mul_of_parity (U : ℕ → State N W →ₗᵢ[ℂ] State N W) (ψ₀ : State N W) (T : ℕ) + (S : Finset (Fin N × Bool × W)) + (h : ∀ x, measureProb (run U ψ₀ x T) S = bitVal ℝ (parity N x)) : + N ≤ 2 * T := + degree_parity.symm.trans_le (degree_le_two_mul U ψ₀ T S h) + end Quantum end Cslib diff --git a/Complexity/Computability/QueryComplexity/Quantum/Search.lean b/Complexity/Computability/QueryComplexity/Quantum/Search.lean index 77860fbcae..b76af26018 100644 --- a/Complexity/Computability/QueryComplexity/Quantum/Search.lean +++ b/Complexity/Computability/QueryComplexity/Quantum/Search.lean @@ -48,8 +48,8 @@ outcome distributions of nearby states (total variation at most `4ε`); `regProb per-outcome bound used here. The source applies Corollary 3.4 to prove that relative to a random oracle `NP` is not contained in `BQTime(o(2^{n/2}))` (Theorem 3.5), which is not formalized here; `card_sub_two_le` is the search lower bound in its standard query-model form, with the constants -of this proof. The decision form, for computing `OR_N`, is `Cslib.Quantum.card_le_sixteen_mul_sq`, -by the polynomial method. +of this proof. The decision form, for computing `OR_N`, is +`Cslib.Quantum.card_le_sixteen_mul_sq_of_threshold_one_right`, by the polynomial method. ## Main definitions diff --git a/ComplexityTests/QuantumPolynomial.lean b/ComplexityTests/QuantumPolynomial.lean index d91889770e..b38a1b070a 100644 --- a/ComplexityTests/QuantumPolynomial.lean +++ b/ComplexityTests/QuantumPolynomial.lean @@ -71,10 +71,17 @@ example : blockSensitivity (threshold 1 1) ≤ 8 * 1 ^ 2 := blockSensitivity_le_eight_mul_sq readBit ψ₀ 1 accept measureProb_readBit_threshold example : 1 ≤ 16 * 1 ^ 2 := - card_le_sixteen_mul_sq readBit norm_ψ₀ 1 accept fun x => by + card_le_sixteen_mul_sq_of_threshold_one_right readBit norm_ψ₀ 1 accept fun x => by rw [measureProb_readBit_threshold] norm_num +-- With one bit, parity is the bit itself, so the algorithm also computes parity exactly. +example : 1 ≤ 2 * 1 := + card_le_two_mul_of_parity readBit ψ₀ 1 accept fun x => by + rw [measureProb_readBit] + congr 1 + cases hx : x 0 <;> simp [parity, hx] + -- The acceptance probability of any algorithm is a polynomial of degree at most `2T`. example (W : Type) [Fintype W] (U : ℕ → State 3 W →ₗᵢ[ℂ] State 3 W) (ψ : State 3 W) (S : Finset (Fin 3 × Bool × W)) :