Operational adversary lower bounds and query characterizations #
Ported from the corresponding upstream modules listed by the source sections below.
References beginning with Source name these retained sections.
The real-matrix / complex-vector bridge #
The adversary side of this project is real: advPMOn is a supremum of L2
operator norms of real matrices, and SourceSpectral supplies the bilinear
bound |x ⬝ᵥ A *ᵥ y| ≤ ‖A‖ √(x⬝ᵥx) √(y⬝ᵥy). The quantum side is complex. The
progress measure of the lower bound lives in between: it is a real matrix Γ
contracted against a family of complex vectors,
∑ x, ∑ y, Γ x y * Re ⟪u x, v y⟫.
This section proves the one inequality that connects them,
|∑ x, ∑ y, Γ x y * Re ⟪u x, v y⟫| ≤ ‖Γ‖ · √(∑ x, ‖u x‖²) · √(∑ y, ‖v y‖²),
which is Risk 2 of the plan discharged: no complex operator-norm theory is needed, and the existing real API is used unchanged.
The proof is the obvious one once the real part is expanded coordinatewise:
Re ⟪u, v⟫ = ∑ h, (Re uₕ Re vₕ + Im uₕ Im vₕ), so the double sum is
∑ h, (aᵣ(h) ⬝ᵥ Γ *ᵥ bᵣ(h) + aᵢ(h) ⬝ᵥ Γ *ᵥ bᵢ(h)), a sum over the basis of
real bilinear forms. Bounding each by SourceSpectral and applying
Cauchy–Schwarz twice — once to combine the real and imaginary parts at a fixed
basis vector, once to sum over the basis — gives the claim. Working with the
real part throughout (rather than the complex Gram value and its modulus) is
what keeps this elementary; the progress measure is defined with Re for the
same reason.
The bridge #
The bridge. A real matrix contracted against complex vector families is bounded by its operator norm times the two total squared norms.
The adversary progress measure #
For an adversary matrix Γ, a weight vector δ, and a family of states ψ x
indexed by the promise domain, the progress is
progress Γ δ δ' ψ = ∑ x, ∑ y, Γ x y · Re ⟪δ x • ψ x, δ' y • ψ y⟫.
The two weight vectors are not a generalization for its own sake: they are
what lets the endgame use the bilinear characterization of the operator norm
(l2_opNorm_le_of_forall_dotProduct, already in SourceSpectral) instead of a
norm-attaining eigenvector, which the project does not have and which would
need the spectral theorem.
Three facts drive the lower bound, and they are the three theorems here:
progress_mulVec— an input-independent unitary does not change it. This is why only queries can make progress.progress_const— at time zero all the states coincide, so the progress isδ ⬝ᵥ Γ *ᵥ δ', which the bilinear characterization can make as close to‖Γ‖as one likes.abs_progress_oracle_sub_le— one query changes it by at most2c √(∑ δ²) √(∑ δ'²), wherecbounds every‖Γ ⊙ advDOn read i‖.
The query step is where the model meets the adversary matrix. Decompose a state
by its query-index register, ψ = ∑_o qRestrict idxOf o ψ over o : Option ι.
The oracle preserves each sector, acts as the identity on the idle sector
none, and on the sector some i depends on the input only through its i-th
letter. So a pair x, y contributes to the change only through sectors i
with read x i ≠ read y i — precisely the support of the mask advDOn read i.
Replacing Γ by Γ ⊙ advDOn read i on the sector i is therefore free, and
the bridge bounds each of the two resulting Gram forms by ‖Γ ⊙ advDOn read i‖
times that sector's weight. Summing over sectors needs only that the sector
weights add up to the total, plus one Cauchy–Schwarz over the sectors.
The Gram form #
A real matrix contracted against two families of complex vectors.
Equations
- QuantumQueryComplexity.gramForm Γ u v = ∑ x : X, ∑ y : X, Γ x y * (QuantumQueryComplexity.qInner (u x) (v y)).re
Instances For
Masking is free when the masked-out pairs contribute equally to both Gram forms.
Sector decomposition by the query-index register #
The query-index register, used as a readout map.
Equations
Instances For
How the oracle acts on the sectors #
The oracle preserves each sector.
On the idle sector the oracle is the identity.
On the sector some i the oracle depends on the input only through its
i-th letter.
The progress measure #
The master bound on the progress.
An input-independent unitary does not change the progress.
The query step #
The weighted family restricted to the sector o.
Equations
- QuantumQueryComplexity.sectFam o δ ψ x = ↑(δ x) • QuantumQueryComplexity.qRestrict QuantumQueryComplexity.idxOf o (ψ x)
Instances For
The oracle acts on the sector families through the state family.
The weight carried by the sector o.
Equations
- QuantumQueryComplexity.sectorWeight δ ψ o = ∑ x : X, QuantumQueryComplexity.qNormSq (QuantumQueryComplexity.sectFam o δ ψ x)
Instances For
One query changes the progress by at most 2c times the two weights.
The output condition #
At the end of a successful computation the progress must be small: an
adversary matrix is supported on pairs with different f-values, and a state
that announces f x with probability at least 1 - ε is nearly orthogonal to
one that announces f y ≠ f x.
Split each final state along the outcome it is supposed to announce,
ψ x = A x + B x, A x = qRestrict readout (f x) (ψ x),
so ‖A x‖² ≥ 1 - ε and ‖B x‖² ≤ ε. The A–A term of the expanded Gram
form vanishes entirely: where Γ is nonzero the two outcomes differ, and
distinct outcomes are orthogonal (qInner_qRestrict_of_ne); where the outcomes
agree Γ is zero. The remaining three terms are bounded by the bridge, giving
|progress| ≤ ‖Γ‖ (2√ε + ε).
On the constant. The sharp bound for this step is 2√(ε(1-ε)), which is
what makes ε = 1/3 work in the literature. For general finite outputs the
matrix-level argument here gives 2√ε + ε instead, which is < 1 exactly
when ε < 3 - 2√2 ≈ 0.1716. For Boolean outputs the sharp constant IS
recovered directly — SourceQuantumLowerBoundOutputBool (the error parts are orthogonal on the
adversary matrix's support, and the masses are linked), consumed by
SourceQuantumLowerBoundMainBool for the ε = 1/3 lower bound. Amplification remains the
relevant route only for general outputs, where the B–B term does not
vanish.
The output condition. On final states that are correct with probability
at least 1 - ε, the progress of any adversary matrix is at most
‖Γ‖ (2√ε + ε).
The adversary lower bound #
Every quantum algorithm that computes f on the promise
read with error at most ε makes at least
(1 - (2√ε + ε)) / 2 · advPMOn read f
queries. The three ingredients are the ones proved in SourceQuantumLowerBoundProgress and
SourceQuantumLowerBoundOutput: the progress starts at δ ⬝ᵥ Γ *ᵥ δ', moves by at most 2 per
query, and ends below ‖Γ‖ (2√ε + ε).
Why two weight vectors. The classical proof takes δ to be a
norm-attaining eigenvector of Γ, so that the initial progress is ‖Γ‖.
That needs the spectral theorem for real symmetric matrices, which this project
has deliberately avoided. Carrying two weight vectors instead makes the initial
progress the bilinear form δ ⬝ᵥ Γ *ᵥ δ', and SourceSpectral's
l2_opNorm_le_of_forall_dotProduct — already proved, and used throughout the
adversary side — converts a bound on all of those into a bound on ‖Γ‖. The
only extra work is normalizing an arbitrary pair of vectors, which is four
lines.
The error threshold is 2√ε + ε < 1, i.e. ε < 3 - 2√2 ≈ 0.1716; see
SourceQuantumLowerBoundOutput for why this is not the sharp 2√(ε(1-ε)) and what recovers the
conventional ε = 1/3.
The progress of an algorithm #
The progress carried by an algorithm's states after t queries.
Equations
- QuantumQueryComplexity.algProgress Γ δ δ' A read t = QuantumQueryComplexity.progress Γ δ δ' fun (x : X) => A.state (read x) t
Instances For
Before any query the progress is the bilinear form.
One query moves the progress by at most 2.
After q queries the progress has moved by at most 2q.
The lower bound #
The telescoping step, parametric in the output constant: any bound
‖Γ‖·κ on the progress after q queries bounds the initial bilinear form by
‖Γ‖·κ + 2q.
The bilinear form of any feasible adversary matrix is bounded by the algorithm's query count and error.
The endgame, parametric in the output constant. If every feasible
adversary matrix satisfies the bilinear bound ‖Γ‖·κ + 2q on unit weight
vectors, then (1 − κ)·advPMOn ≤ 2q. Instantiated by
advPMOn_le_of_computes with κ = 2√ε + ε, and by the Boolean sharpening
(SourceQuantumLowerBoundMainBool) with κ = 2√(ε(1−ε)).
The adversary lower bound. A q-query algorithm with error ε forces
advPMOn read f ≤ 2q / (1 - (2√ε + ε)).
The bound on the query complexity #
Bounded-error quantum query complexity is at least
(1 - (2√ε + ε))/2 times the adversary bound, for any error ε with
2√ε + ε < 1.
A concrete instance of the lower bound: at error 1/16 the constant is
7/32. (The threshold 2√ε + ε < 1 holds for every ε < 3 - 2√2 ≈ 0.1716.)
The sharp output condition, for Boolean outputs #
SourceQuantumLowerBoundOutput bounds the final progress by ‖Γ‖(2√ε + ε) for any decidable
output type; this section proves the sharp constant 2√(ε(1−ε)) when the
output is Boolean — which is what makes ε = 1/3 work without amplification.
Two extra facts are available for O = Bool, and they are exactly what the
matrix-level argument needs:
- The
B–Bterm vanishes too. With two outcomes the error part isB x = qRestrict p (!f x) (ψ x); on the support ofΓthe outputs differ, so!f x ≠ !f yand the error parts are orthogonal — the sameqInner_qRestrict_of_nethat killed theA–Aterm. Only the two cross terms survive. - The masses are linked, not just bounded.
‖A‖² + ‖B‖² = 1per input, so the weighted masses satisfy∑‖δA‖² = 1 − βwithβ = ∑‖δB‖² ≤ εexactly, and the two cross terms are√(1−β)√β' + √β√(1−β').
The scalar maximization √(1−β)√β' + √β√(1−β') ≤ 2√(ε(1−ε)) for
β, β' ∈ [0, ε], ε ≤ 1/2 is where the sharp constant comes from: after the
AM–GM step cc' ≤ 1 − (s² + s'²)/2 the square of the left side is at most
(s+s')²(1−ss'), whose maximum over [0,√ε]² is at the corner — proved by
two monotone steps, each an explicit product-of-nonnegatives factorization
(poly_step), no calculus.
No spectral decomposition, no Helstrom measurement theory: the same bridge as
SourceQuantumLowerBoundOutput, with the Boolean structure supplying the two extra facts.
The scalar maximization #
The sharp output condition #
The sharp output condition for Boolean outputs. On final states that
are correct with probability at least 1 - ε, ε ≤ 1/2, the progress of any
adversary matrix is at most ‖Γ‖ · 2√(ε(1−ε)).
The adversary lower bound at the sharp Boolean constant #
SourceQuantumLowerBoundMain proves the lower bound with output constant 2√ε + ε, which
requires ε < 3 − 2√2 ≈ 0.1716. For Boolean outputs the sharp constant
2√(ε(1−ε)) of SourceQuantumLowerBoundOutputBool plugs into the same parametric endgame
(advPMOn_le_of_bilinear), and 2√(ε(1−ε)) < 1 holds for every
ε < 1/2 — in particular at the conventional ε = 1/3:
mul_advPMOn_le_qQueryOn_of_error_third :
(1/36) · advPMOn read f ≤ Q_{1/3}(f)
promise-native, no amplification, no repetition compiler. The constant check
behind 1/36 is (3 − 2√2)/6 ≥ 1/36 ↔ 289 ≥ 288 — the sharp constant at
ε = 1/3 is (3 − 2√2)/6 ≈ 0.0286, and 1/36 ≈ 0.0278 sits just under it.
The Boolean-sharp adversary bound: a q-query algorithm with error
ε ≤ 1/2 forces (1 − 2√(ε(1−ε)))·advPMOn read f ≤ 2q.
The sharp lower bound on Boolean query complexity: every ε ≤ 1/2
with 2√(ε(1−ε)) < 1 works — the threshold is ε < 1/2, not
ε < 3 − 2√2.
The conventional-error instance: (1/36)·advPMOn read f ≤ Q_{1/3}(f)
for Boolean f, promise-native.
Plurality amplification, and the general-output 1/3 lower bound #
For a Boolean output the sharp 1/3 lower bound
(1/36)·ADV±ₚ(f) ≤ Q_{1/3}(f) needs no amplification
(SourceQuantumLowerBoundMainBool); for a general finite output type the lower
bound was known only at the characterization's own error,
(7/32)·ADV±ₚ(f) ≤ Q_{1/16}(f). This section closes the gap by plurality
amplification: run a 1/3-error algorithm 43 times independently and
announce the most frequent answer.
The analysis is an exponential-moment (Markov) bound, not a Chernoff bound
and not a binomial-tail library. If W is the number of wrong runs, the
product structure of the independent-run compiler (SourceQuantumProductRun,
exact product statistics) gives
E[2^W] = ∏ᵢ (1 + Pr[run i wrong]) ≤ (4/3)^43,
so Pr[W ≥ 22] ≤ (4/3)^43 / 2^22 = 2^64 / 3^43 < 1/16; and with at most
21 wrong runs the correct answer has a strict majority, hence is the
plurality. Thus
Q_{1/16}(f) ≤ 43·Q_{1/3}(f) (finite outputs),
and with the 1/16 lower bound, (7/1376)·ADV±ₚ(f) ≤ Q_{1/3}(f).
Contents: the k-fold product realization over an arbitrary finite output
type (Realizes.foldRec, the Boolean Realizes.fold generalized); the
exponential-moment tail sum_prod_tail_le; the plurality readout
plurality and its majority lemma; amplify_plurality at general k and
ε; and the 43-run endpoints.
The exponential-moment tail sum_prod_tail_le (with wrongCount) lives in
SourceQuantumTail.
The plurality readout #
The plurality readout: the most frequent value of the record (the earliest among ties).
Equations
- QuantumQueryComplexity.plurality y = (List.argmax (QuantumQueryComplexity.voteCount y) (List.map y (List.finRange (k + 1)))).getD (y 0)
Instances For
A wrong plurality has at least ⌈(k+1)/2⌉ wrong runs.
Plurality amplification #
Plurality amplification. k + 1 independent runs of an algorithm
with error ε for a finite-output function, read out by plurality, compute
the same function with error (1 + ε)^{k+1} / 2^{⌈(k+1)/2⌉}, at k + 1
times the cost.
The 43-run endpoints #
43 runs at error 1/3 give error below 1/16:
(4/3)^43 / 2^22 = 2^64 / 3^43 < 1/16.
Q_{1/16}(f) ≤ 43·Q_{1/3}(f) for finite outputs.
The general-output 1/3 lower bound:
(7/1376)·ADV±ₚ(f) ≤ Q_{1/3}(f) for any finite nonempty output type, on
any promise. 7/1376 = (7/32)/43.
The total-function form: (7/1376)·ADV±(f) ≤ Q_{1/3}(f).
The fixed-error characterization for total Boolean functions #
The first end-to-end deliverable of the quantum layer:
(7/32) · ADV±(f) ≤ Q_{1/16}(f) ≤ 2¹⁴ · ADV±(f)
for every total Boolean function f : (ι → Bool) → Bool
(qQuery_characterized_by_advPM). The lower half is the operational bound
(mul_advPMOn_le_qQueryOn_of_error_sixteenth at read = id); the upper half
chains strong duality (exists_dualPair_of_advPM_lt, giving dual pairs
of cost arbitrarily close to ADV±), the total-to-promise restriction
(HasDual.hasDualOn), and uniform extraction
(qQueryOn_le_of_hasDualOn_uniform). Taking arbitrarily small slack gives
Q_{1/16}(f) ≤ 8192(1 + ADV±(f)) without assuming an optimal dual exists.
For nonconstant functions, one_le_advPM supplies ADV± ≥ 1, so this is at
most 2¹⁴·ADV±. Constant functions cost zero queries.
This module combines the strong-duality results in Adversary with the operational
quantum hierarchy. Build the complete project with lake build LeanPool.QuantumQuery.
The conventional-error form is here too
(boundedErrorQQuery_characterized_by_advPM):
(1/36) · ADV±(f) ≤ Q_{1/3}(f) ≤ 2¹⁴ · ADV±(f)
— the upper half by error monotonicity, the lower half by the sharp Boolean
output condition of SourceQuantumLowerBoundOutputBool (no amplification).
The oracle-simulation theorem (SourceQuantumSimulation) transports the
characterization into the conventional model
(xorQQuery_characterized_by_advPM, below): the standard Boolean XOR
oracle with explicit idle-index and blank-answer sectors, at two queries
per query. Convention, stated for precision: that XOR model lives on the
same basis Option ι × Option Bool × W, acting as the textbook XOR on the
some-answer sector and as the identity on the idle and blank sectors; the
further padding equivalence to a literal ι × Bool × W basis is a standard
harmless extension and is not separately formalized.
The additive uniform upper bound, for total Boolean functions:
strong duality and uniform extraction give Q_{1/16}(f) ≤ 8192(1 + ADV±(f)).
Arbitrarily small slack suffices; dual optimizer attainment is not needed.
The algorithmic upper bound, for total Boolean functions:
Q_{1/16}(f) ≤ 2¹⁴·ADV±(f). The additive uniform bound absorbs its constant
term using ADV± ≥ 1 for nonconstant functions; constants need no queries.
The fixed-error characterization for total Boolean functions
: (7/32)·ADV±(f) ≤ Q_{1/16}(f) ≤ 2¹⁴·ADV±(f).
The conventional-error upper bound is free (error monotonicity):
Q_{1/3}(f) ≤ Q_{1/16}(f) ≤ 2¹⁴·ADV±(f).
The conventional-error lower bound for total Boolean functions:
(1/36)·ADV±(f) ≤ Q_{1/3}(f), via the sharp Boolean output condition — no
amplification.
The conventional-error characterization at ε = 1/3:
(1/36)·ADV±(f) ≤ Q_{1/3}(f) ≤ 2¹⁴·ADV±(f) for total Boolean f.
The characterization in the Boolean XOR-oracle model: for total
Boolean f, at error 1/3, using the idle and blank sectors of SourceQuantumXorOracle,
(1/72)·ADV±(f) ≤ Qˣ_{1/3}(f) ≤ 2¹⁵·ADV±(f),
by the two-queries-per-query simulation of SourceQuantumSimulation applied
to the transposition-model characterization.
The promise-Boolean characterization #
Promise strong duality (SourceDualityMainOn) feeds the promise-native
extraction, and the lower bound was promise-native from the start.
The promise upper bound from the promise adversary bound.
The promise-Boolean characterization at fixed error 1/16
: for any read-determined Boolean promise problem on a
finite nonempty alphabet,
(7/32)·ADV±ₚ(f) ≤ Q_{1/16}(f) ≤ 8192(1 + 8√|σ|·ADV±ₚ(f)). The unsuffixed
name is the general-output theorem below.
The multiplicative form at 1/16, for problems nonconstant on the
promise: Q_{1/16}(f) ≤ 2¹⁷·√|σ|·ADV±ₚ(f).
The promise-Boolean characterization at bounded error 1/3: the
lower half is the sharp promise-native Boolean bound, the upper half is error
monotonicity into the 1/16 extraction.
Finite outputs (the bit-encoding route) #
Each encoding bit of f is a post-composition, so its promise adversary
bound is at most f's (advPMOn_comp_le); the promise-Boolean
characterization supplies a 1/16-algorithm per bit, and the independent-run
machinery (SourceQuantumAmplify, SourceQuantumFiniteOutput) amplifies and joins them.
The general-output upper bound: for f : X → O with O a finite
nonempty output type of m values, on any promise and finite nonempty
alphabet,
Q_{1/16}(f) ≤ 2·B·(Nat.clog 2 (3B)) · 8192(1 + 8√|σ|·ADV±ₚ(f)),
B = Nat.clog 2 m
(Nat.clog 2 0 = 0, so singleton outputs are included) — the
O(log m · loglog m · √|σ| · ADV±ₚ) shape, at the SAME fixed error
1/16 as the lower bound: with t = Nat.clog 2 (3B) the assembled error is 0
for B = 0, exactly 1/16 for B = 1, and at most 1/(9B) ≤ 1/18 for
B ≥ 2.
The conventional-error form, by monotonicity.
The finite-output characterization (the reserved unsuffixed name):
the promise adversary bound characterizes fixed-error quantum query
complexity — the same error 1/16 on both sides — for any finite nonempty
output type, up to the alphabet factor √|σ| and a log m · loglog m
output factor.
The finite-output characterization at the conventional error 1/3
the lower half by plurality amplification over 43 runs
(SourceQuantumPlurality, Q_{1/16} ≤ 43·Q_{1/3}), the upper half by monotonicity
from the 1/16 bound.
(7/1376)·ADV±ₚ(f) ≤ Q_{1/3}(f)
≤ 2·B·(Nat.clog 2 (3B)) · 8192(1 + 8√|σ|·ADV±ₚ(f)), B = Nat.clog 2 m.
The multiplicative asymptotic at the characterization's own error:
absorbing the additive 1 via half_le_advPMOn,
Q_{1/16}(f) ≤ 2¹⁸·B·(Nat.clog 2 (3B))·√|σ|·ADV±ₚ(f), B = Nat.clog 2 m
(Nat.clog 2 0 = 0).
The conventional-error multiplicative form, by monotonicity.
The finite-output characterization at 1/3, multiplicative
the plurality-amplified lower bound paired with the
multiplicative upper bound, so that "characterization" is literally a
two-sided proportionality —
(7/1376)·ADV±ₚ(f) ≤ Q_{1/3}(f) ≤ 2¹⁸·B·(Nat.clog 2 (3B))·√|σ|·ADV±ₚ(f),
B = Nat.clog 2 m.