Adversary matrices, semidefinite duality, and composition #
Ported from the corresponding upstream modules listed by the source sections below.
References beginning with Source name these retained sections.
The negative-weight adversary bound: definitions #
We define the negative-weight adversary bound ADV± of Høyer–Lee–Špalek
(quant-ph/0611054, Definition 2) for a total function f : (ι → σ) → O, in the
division-free primal form of Belovs–Lee (arXiv:2004.06439, Definition 6):
advPM f = sup { ‖Γ‖ | Γ symmetric, Γ x y = 0 whenever f x = f y, and ‖Γ ⊙ D i‖ ≤ 1 for every input index i }
where D i = advD i is the difference matrix with (D i) x y = 1 iff
x i ≠ y i, ⊙ is the Hadamard (entrywise) product, and ‖·‖ is the spectral
(L2 operator) norm. Since Γ = 0 is feasible, the value set is nonempty and
advPM f ≥ 0; no division or Γ ≠ 0 side condition is needed.
Nothing here uses two-valuedness of the input alphabet σ or of the output type
O: advD needs only DecidableEq σ for its if, and IsAdvMatrix uses
f x = f y as a proposition, never as a decidable test. The Boolean theory is
recovered at σ = O = Bool, which is how every downstream file uses it; the
general alphabet is what makes non-Boolean problems such as maximum finding
expressible.
We also define the classical nonnegative-weight bound adv (HLŠ Definition 1)
by adding the entrywise nonnegativity constraint.
The difference matrix D_i (HLŠ §2, BL Definition 6): (advD i) x y = 1
if x i ≠ y i and 0 otherwise.
Instances For
An adversary matrix for f (HLŠ §2): a real symmetric matrix supported on
pairs of inputs with different f-values. Taking x = y shows the diagonal
vanishes.
Equations
- QuantumQueryComplexity.IsAdvMatrix f Γ = (Γ.IsHermitian ∧ ∀ (x y : ι → σ), f x = f y → Γ x y = 0)
Instances For
The negative-weight adversary bound ADV±(f) (HLŠ Definition 2, in the
division-free form of BL Definition 6).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The classical (nonnegative-weight) adversary bound ADV(f)
(HLŠ Definition 1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Maximum finding: the function and its level counts #
maxFun x = ⊔ᵢ x i for x : ι → A with A a linear order and ι a nonempty
finite index type. This is the non-Boolean function whose adversary bound we
study; at A = Bool it is exactly orN.
We use Finset.sup' over univ rather than Finset.max': max' takes a
Finset A, so stating it would force (Finset.univ.image x).max', dragging in
[DecidableEq A] and an image-nonemptiness proof. sup' ranges over ι
directly and needs neither.
Alongside it we define cnt p x, the number of coordinates of x on which a
Bool-valued predicate p holds, and the normalised indicator wt p x.
Predicates are Bool-valued rather than Prop-valued throughout this
development so that no Decidable instance ever has to be carried, matched, or
unified.
The maximum of a tuple: maxFun x = ⊔ᵢ x i.
Equations
Instances For
Level counts #
If the cut holds at the maximum then some coordinate realises it, so the
count is positive. This is what makes the division by cnt in the dual
solution harmless.
The normalised indicator of a cut #
The indicator of {i | p (x i)}, normalised to sum to 1.
Equations
- QuantumQueryComplexity.wt p x i = (if p (x i) = true then 1 else 0) / ↑(QuantumQueryComplexity.cnt p x)
Instances For
Spectral-norm infrastructure for the adversary bound #
Layer-0 lemmas about the L2 operator norm of real matrices. All
EuclideanSpace/WithLp friction is quarantined inside the proofs of this
file: every exported statement is phrased with raw Matrix, *ᵥ, ⬝ᵥ and
Real.sqrt (x ⬝ᵥ x).
Main results:
abs_dotProduct_mulVec_le— the master bilinear bound|x ⬝ᵥ A *ᵥ y| ≤ ‖A‖ * √(x ⬝ᵥ x) * √(y ⬝ᵥ y);l2_opNorm_le_of_forall_dotProduct— its converse;abs_entry_le_l2_opNorm— entries are bounded by the norm;l2_opNorm_le_sum_abs— the crude bound‖A‖ ≤ ∑ |A x y|;abs_eigenvalue_le_norm— eigenvalues are bounded by the norm.
Reindexing a square matrix along an injection of index types does not increase the L2 operator norm.
The eigenvalue layer #
For a real symmetric matrix, the L2 operator norm equals the sup norm of
the eigenvalue vector. Proof: spectral theorem plus unitary invariance of the
C*-norm, plus ‖diagonal v‖ = ‖v‖.
Spanning-eigenvector bound. If a family of eigenvectors of a real
symmetric matrix spans the whole space and all its eigenvalues are bounded by
B in absolute value, then ‖A‖ ≤ B. Members of the family are allowed to
be zero.
Conjugation by a ±1 diagonal matrix preserves the L2 operator norm.
Basic properties of the adversary bound #
Accessor lemmas for advPM as a conditionally complete supremum, the a priori
bound ‖Γ‖ ≤ card² for feasible matrices (which makes the value set bounded
above), and the un-normalized witness lemma norm_div_le_advPM — the workhorse
for proving lower bounds on advPM.
All entries of a feasible matrix are bounded by 1 in absolute value:
off-diagonal entries embed into some Γ ⊙ advD i, and entries with
f x = f y (in particular the diagonal) vanish.
The a priori bound making the advPM value set bounded above.
Every feasible matrix certifies a lower bound on advPM.
ε-accessor: any value below advPM f is beaten by a feasible witness.
Un-normalized witness lemma: an adversary matrix all of whose Schur
norms are at most c certifies ‖Γ‖ / c ≤ advPM f. This is the paper's
ratio formulation, division-free at the point of use.
The elementary two-entry witness #
The elementary adversary matrix e_{xy} + e_{yx} supported on a single
symmetric pair of entries.
Equations
- QuantumQueryComplexity.pairMatrix x y = Matrix.single x y 1 + Matrix.single y x 1
Instances For
Masking a pair matrix by a difference matrix either leaves it alone or kills it, according to whether the pair differs in that coordinate.
Bipartite support structure of adversary matrices #
An adversary matrix N for g vanishes on same-colored pairs (g u = g v),
so it maps vectors supported on one color class into the other class.
Consequently an eigenvector with nonzero eigenvalue must have nonzero
restriction to both color classes (brestrict_ne_zero,
IsAdvMatrix.exists_eigenvector_support). This is the nonvanishing input to
the ≥ direction of the composed-matrix norm formula (HLŠ Lemma 16).
A matrix vanishing on same-colored pairs maps a b-supported vector to a
!b-supported one, with the values of the full product.
An eigenvector with nonzero eigenvalue of a color-bipartite matrix has nonzero restriction to each color class.
Wrapper for the composition layer: an eigenvector with nonzero eigenvalue
of an adversary matrix for g has support in every color class of g.
The Schur-multiplier norm bound #
The key estimate ‖X ⊙ P‖ ≤ d * ‖X‖ for a positive semidefinite P whose
diagonal entries are at most d (norm_hadamard_posSemidef_le), proved via a
Gram decomposition of P and Cauchy–Schwarz. In the composition theorem this
replaces the sign-flipping analysis of HLŠ Lemma 16 (following the PSD
viewpoint of Belovs–Lee, arXiv:2004.06439 §4).
Also: small PSD facts — the all-ones matrix, the 2×2 seed
[[R, λ], [λ, R]] for |λ| ≤ R, and M + ‖M‖ • 1 ≥ 0 for symmetric M
(BL Lemma 18). The "PSD lift" fact (BL Fact 2) is mathlib's
Matrix.PosSemidef.submatrix, which takes an arbitrary index map.
The all-ones matrix is positive semidefinite.
Schur-multiplier bound (Belovs–Lee): if P is positive semidefinite
with all diagonal entries at most d, then ‖X ⊙ P‖ ≤ d * ‖X‖.
M + ‖M‖ • 1 is positive semidefinite for symmetric M
(BL Lemma 18).
The composed adversary matrix (hat formulation) #
Following Belovs–Lee (arXiv:2004.06439, Definitions 17 and 19), the composed
adversary matrix for h = f ∘ gᵏ is built from an outer matrix Γf and inner
matrices M i via hat N = N + ‖N‖ • 1:
compose g Γf M x y = Γf (tilde g x) (tilde g y) * ∏ i, hat (M i) (x·ᵢ) (y·ᵢ)
For a g-shaped N (symmetric, vanishing on pairs with g u = g v), hat N
agrees entrywise with the color-block convention of HLŠ Definition 6:
same-color blocks are ‖N‖·I, different-color blocks are N.
The block decomposition is abstract #
The inner inputs are not assumed to form a Boolean cube. Everything below
is stated for a composed input type Z equipped with an equivalence
e : Z ≃ (α → Y) onto tuples of inner inputs drawn from an arbitrary finite
type Y, with a colouring g : α → Y → Bool.
This permits composition of promise problems whose inner inputs range over a
subtype rather than a cube. The spectral content never sees the cube: the two
places two-valuedness is used are the colouring's output and the outer cube
α → Bool, and both survive.
The original cube statements are recovered verbatim as the instance
e := cubeBlocks α β, so no downstream file changes.
The hat matrix #
Composition over an abstract block decomposition #
The i-th block of a composed input.
Equations
- QuantumQueryComplexity.sliceE e z i = e z i
Instances For
The vector of inner-function values of a composed input.
Equations
- QuantumQueryComplexity.tildeE e g z i = g i (QuantumQueryComplexity.sliceE e z i)
Instances For
BL Definition 19 over an abstract block decomposition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cube instance #
The original statements, recovered by taking the block decomposition to be the currying equivalence.
The block decomposition of a Boolean cube into α blocks of shape β.
Equations
Instances For
The i-th block of a composed input.
Equations
Instances For
The constant family of inner functions (the uniform case).
Equations
- QuantumQueryComplexity.constFam g x✝ = g
Instances For
BL Definition 19, uniform-alphabet form: the composed matrix.
Equations
Instances For
The dual (minimisation) form of the adversary bound #
The dual of the adversary SDP (Lee–Mittal–Reichardt–Špalek–Szegedy; stated as
Theorem 7 of Belovs–Lee, arXiv:2004.06439) asks for two families of vectors
u x i, v x i indexed by inputs x and query positions i, satisfying
∑_{i : x i ≠ y i} ⟪u x i, v y i⟫ = 1 if g x ≠ g y, and = 0 if g x = g y,
with objective max_x ∑_i ‖u x i‖² (and the same for v). The constraints
on pairs with g x = g y are the extra ones isolated by LMRSS; they are what
makes dual solutions compose.
This section defines feasible dual solutions (DualPair), the dual value
advDual as an infimum of costs, and proves weak duality
advPM g ≤ advDual g (advPM_le_advDual) by the same Gram-plus-Cauchy–Schwarz
argument that underlies the Schur-multiplier bound.
Strong duality is proved later in SourceDualityMain by Hahn–Banach separation:
advDual_eq_advPM identifies the two values, and advPM_composeFun_eq gives
unconditional exact Boolean block composition.
A feasible solution of the dual program for g, with vectors of
dimension K. DecidableEq σ is what makes the coordinate mask
if x i = y i meaningful, and DecidableEq O the output test
if g x = g y; no finiteness of σ is needed here, since the constraint
never sums over inputs.
- u : (ι → σ) → ι → K → ℝ
The first vector family.
- v : (ι → σ) → ι → K → ℝ
The second vector family.
- constraint (x y : ι → σ) : (∑ i : ι, if x i = y i then 0 else ∑ k : K, self.u x i k * self.v y i k) = if g x = g y then 0 else 1
The dual feasibility constraint, including the LMRSS constraints on pairs with equal
g-value.
Instances For
The cost of a dual solution is bounded by c.
Equations
Instances For
Transporting a dual solution along a bijection of the dimension type.
Equations
Instances For
Weak duality #
The two estimates behind weak duality are stated for an arbitrary finite
type X of inputs rather than for the cube ι → σ. Nothing in them uses the
product structure — only that the matrices are indexed by inputs — and the extra
generality is what lets SourcePromiseDefs reuse them verbatim for a
promise domain.
The core estimate of weak duality: a sum of bilinear forms of norm at
most one, reweighted by dual vectors of cost at most c, is bounded by
c times the product of the vector lengths.
Weak duality: every feasible dual solution of cost at most c bounds
the adversary bound by c.
A feasible dual solution always exists #
The number of coordinates on which two inputs differ.
Equations
- QuantumQueryComplexity.diffCard x y = {i : ι | x i ≠ y i}.card
Instances For
A dual solution of finite (very lossy) cost, showing the dual program is
always feasible: u x i is the standard basis vector of x, and the mass of
v y i is spread over the coordinates where the inputs differ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dual value #
The value of the dual program.
Equations
Instances For
Weak duality.
The b-sum form of the composed matrix #
The first rewriting lemma (composeE_apply_sum): the entry
composeE e g Γf M x y can be written as a sum over all outer inputs
b : α → Bool, with guards if g i (sliceE e y i) = b i making the
b = tildeE e g y fiber automatic. This eliminates the non-factoring
occurrence Γf x_tilde y_tilde before any sum/product interchange.
As in SourceCompositionHat the block decomposition is abstract; the cube statement is the
instance at cubeBlocks.
The outer auxiliary matrices Γf ⊙ Emat and their PSD structure #
For an assignment of eigenvalues lamv i (with |lamv i| ≤ R i), the matrix
Emat R lamv a b = ∏ i, if a i = b i then R i else lamv i
is positive semidefinite: it is the entrywise product over i : α of lifts of
the 2×2 seeds [[R i, lamv i], [lamv i, R i]] along the coordinate maps
a ↦ a i (mathlib's Matrix.PosSemidef.submatrix — BL Fact 2 — plus the
Schur product theorem Matrix.PosSemidef.hadamard). Its diagonal is
∏ i, R i, so the Schur-multiplier bound gives
‖Γf ⊙ Emat R lamv‖ ≤ (∏ i, R i) * ‖Γf‖ — replacing the sign-flipping
analysis of HLŠ Lemma 16.
At a "vertex" (lamv i = ε i * R i with ε i = ±1), Γf ⊙ Emat becomes a
±1-diagonal conjugate of (∏ R) • Γf (hadamard_Emat_vertex), which is the
witness used in the ≥ direction.
Entrywise products of PSD matrices lifted along arbitrary maps are PSD
(Finset induction from the Schur product theorem; BL Facts 2 and 3).
Entrywise products of PSD matrices lifted along coordinate evaluations are PSD.
The outer auxiliary matrix of HLŠ Lemma 16 (denoted A_c there, with
lamv i the eigenvalue selected in slot i).
Equations
Instances For
The adversary bound on a promise domain #
advPM f is a single worst-case number attached to a total function on the
cube ι → σ. Some bounds are genuinely instance-sensitive: the semilattice
product costs O(√(n log|L_x|)) where L_x is generated by the letters of the
input x at hand, and that cannot be said with a free x on only one side of
an inequality about a total function.
The fix is to let the inputs be an arbitrary finite type X together with an
observation map
read : X → ι → σ,
so that a query at i returns read x i. Every occurrence of x i = y i in
the definitions becomes read x i = read y i, and nothing else changes:
advPMOn, DualPairOn and weak duality are the same statements with the cube
replaced by X. The total case is X = (ι → σ) with read x = x.
The point of the definitions is DualPair.restrictTo: a dual solution for a
total function restricts to the promise at no cost, and the restricted cost
is the maximum of the pointwise masses over the promise only. So a bound whose
per-input analysis needs a hypothesis about that input — a critical budget, say —
gives a promise bound as soon as the promise guarantees the hypothesis.
The primal bound #
The difference matrix of a promise domain: 1 exactly when a query at i
distinguishes the two promise inputs.
Equations
Instances For
An adversary matrix on a promise domain.
Equations
- QuantumQueryComplexity.IsAdvMatrixOn f Γ = (Γ.IsHermitian ∧ ∀ (x y : X), f x = f y → Γ x y = 0)
Instances For
The adversary bound of a function on a promise domain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dual #
A feasible dual solution on a promise domain.
- u : X → ι → K → ℝ
The first vector family.
- v : X → ι → K → ℝ
The second vector family.
- constraint (x y : X) : (∑ i : ι, if read x i = read y i then 0 else ∑ k : K, self.u x i k * self.v y i k) = if f x = f y then 0 else 1
Feasibility, with the mask read through
read.
Instances For
The cost of a dual solution on a promise domain.
Equations
Instances For
Weak duality on a promise domain. The same Gram-plus-Cauchy–Schwarz
argument as advPM_le_of_dualPair; only the mask is read through read.
Restricting a total dual solution to a promise #
A total dual solution restricted to a promise domain. The vectors are
unchanged: the promise constraint at (x, y) is the total constraint at
(read x, read y).
Equations
Instances For
The restricted cost is the maximum of the pointwise masses over the promise only — which is the entire point of the construction.
Gram encoding of the dual program, on a promise domain #
The promise-domain mirror of SourceDualityGram: the input space is an
abstract finite X read through read : X → ι → σ, the constraint mask is
read x i = read y i, and the target is [f x ≠ f y]. Everything else —
the convexification by passing to Gram matrices, the rank-one decomposition
back to a DualPairOn — is the same change of variables.
The total case is the instance X = ι → σ, read = id; it is kept as the
separate SourceDualityGram because its statements (DualPair, advPM) are
pinned by downstream consumers.
The affine data of the promise dual program #
The right-hand side of the dual feasibility constraint on the promise
domain: 1 on pairs with distinct values, 0 otherwise.
Equations
Instances For
The left-hand side of the dual feasibility constraint, as a function of
the Gram matrix, with the mask read through read.
Equations
Instances For
Linearity #
A positive semidefinite Gram matrix has nonnegative costs.
Rank-one Gram matrices #
From a Gram matrix to a dual solution #
Every positive semidefinite matrix satisfying the promise dual constraints
is the Gram matrix of a feasible DualPairOn of the same cost.
A promise certificate for the identity read is a total-input certificate.
Instances For
The conversion preserves both vector families and hence the cost bound.
Gram encoding of the dual program #
A feasible dual solution (DualPair) is a pair of vector families u x i,
v y i; the dual constraints and the dual cost depend on those families only
through their inner products, i.e. only through the Gram matrix of the whole
family. This section makes that change of variables explicit, which is what
convexifies the dual program: the set of feasible Gram matrices is the
intersection of the (convex) positive semidefinite cone with affine
constraints, whereas the set of feasible vector families is not convex.
Indexing the combined family by GramIdx ι σ = (ι → σ) × ι × Bool — false
tagging a u-vector and true a v-vector — the dictionary is
gramR G = dualTarget g↔ theDualPair.constraintequations,gramCost G b x ≤ cfor allb,x↔DualPair.IsCostLe c.
Both directions of the translation are proved: gramOfDual builds the Gram
matrix of a dual solution, and exists_dualPair_of_gram extracts a dual
solution of dimension Fin m from any positive semidefinite G satisfying the
constraints, via the rank-one decomposition
Matrix.posSemidef_iff_eq_sum_vecMulVec.
Index type for the Gram matrix of a dual solution: (x, i, false) indexes
the vector u x i and (x, i, true) indexes v x i.
Equations
- QuantumQueryComplexity.GramIdx ι σ = QuantumQueryComplexity.GramIdxOn (ι → σ) ι
Instances For
The affine data of the dual program #
The right-hand side of the dual feasibility constraint:
dualTarget g x y = 1 if g x ≠ g y and 0 otherwise.
Instances For
The left-hand side of the dual feasibility constraint, as a function of the Gram matrix.
Equations
Instances For
Linearity #
Rank-one Gram matrices #
From a dual solution to its Gram matrix #
The two vector families of a dual solution, packed into a single matrix
whose rows are indexed by GramIdx ι σ.
Equations
Instances For
The Gram matrix of a dual solution.
Equations
Instances For
From a Gram matrix back to a dual solution #
Every positive semidefinite matrix satisfying the dual constraints is the
Gram matrix of a feasible dual solution of the same cost. The dimension comes
out as Fin m, which is the shape advDual normalises to.
Pulling a dual solution back along an embedding of coordinates #
A subproblem of a divide-and-conquer algorithm reads only a block of the
input. Formally it is pullbackFun e f x = f (x ∘ e) for an injection
e : κ → ι of the block into the full coordinate set.
A dual solution for f transports to one for pullbackFun e f at the same
cost: place the j-th vector of the original solution at coordinate e j and
zero elsewhere. Injectivity is what makes this work — each coordinate of ι
receives at most one vector, so the ℓ² masses simply move rather than adding
up, and the masked sum over ι restricts to the masked sum over κ.
This is how upstream Max/Staircase.lean's bound for maxFun on a κ-indexed
input becomes a bound for "the maximum over a block" as a function of the whole
array, with cost governed by the block size |κ| and not by |ι|.
Restricting a function to a block of coordinates.
Equations
- QuantumQueryComplexity.pullbackFun e f x = f fun (j : κ) => x (e j)
Instances For
Spreading a κ-indexed family over ι #
The value placed at coordinate i by a κ-indexed family.
Instances For
Injectivity makes spread multiplicative: at most one κ-index lands on
any given coordinate.
Summing a spread family over ι recovers the sum over κ.
A dual solution pulled back along an injection of coordinates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pullback costs exactly what the original solution costs — the ℓ² mass
moves from κ to the image of e without accumulating.
Freezing the coordinates outside a block #
The dual of padding. A function of n variables can be regarded as a function
of N ≥ n variables in which the last N - n are held at fixed, known values;
that is what "append N - n known identity matrices to the input" means, and a
dual solution for the padded problem restricts to one for the original at
unchanged cost.
Two conditions are needed, and between them they say that the adversary mask is
transported exactly. hin says the embedded coordinates are read faithfully —
two inputs agree at i precisely when the padded inputs agree at e i — and
hout says the frozen coordinates never depend on the input, so they contribute
nothing to the mask. Injectivity of e is what stops the ℓ² masses from
accumulating, exactly as in pullback.
Unlike alphaMap, the alphabets on the two sides need not match: padding
typically enlarges σ to Option σ in order to name the frozen letter.
A dual solution restricted along a padding.
Equations
Instances For
The restriction costs no more than the padded solution: the ℓ² mass at the
frozen coordinates is simply discarded.
Recoding the alphabet #
Recoding the input alphabet along a map m.
Equations
- QuantumQueryComplexity.alphaFun m f x = f fun (i : ι) => m (x i)
Instances For
A dual solution transports along an injective recoding of the alphabet, at unchanged cost.
Injectivity is exactly what is needed and no more: it keeps the adversary mask
x i ≠ y i in step with m (x i) ≠ m (y i), so the masked sums agree term by
term. A non-injective recoding would merge inputs and let extra coordinates
into the sum.
The use here is order-reversing: v ↦ M - 1 - v is a bijection of Fin M, so a
solution for a maximum becomes one for a minimum without any separate
development.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Transporting along an equality of functions #
A dual solution for f is one for any function equal to f. The vector
families are unchanged, so all costs are too.
Instances For
Enlarging the dimension type #
Padding a dual solution with zero coordinates, along an injection of dimension types. Costs are unchanged.
This is what lets solutions built over different dimension types be fed to
composeShared, which needs a single type for all subproblems.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The eigen-computation for composed matrices (HLŠ Lemma 16, Items 1–2) #
The crux of the composition theorem: for eigenvectors v i of the inner
matrices M i (eigenvalues lamv i) and an eigenvector w of the outer
auxiliary matrix Γf ⊙ Emat (‖M ·‖) lamv (eigenvalue μ), the tensor
vector
tensorVec g v w x = w (tilde g x) * ∏ i, v i (slice x i)
is an eigenvector of compose g Γf M with eigenvalue μ
(compose_mulVec_tensorVec).
The two supporting identities:
hat_guarded_row_sum(K1) — the per-block action, replacing HLŠ Eq. (3) and all restriction-vector bookkeeping by a scalar computation;sum_prod_slice(K2) — the sum/product interchange along(α × β) → Bool ≃ α → β → Bool.
As in SourceCompositionHat everything is proved over an abstract block decomposition
e : Z ≃ (α → Y); the cube statements are the cubeBlocks instance.
This includes promise problems whose inner inputs form a subtype. Nothing in the
spectral argument sees the difference: K1 uses only that the colouring is
Bool-valued, and K2 is Fintype.prod_sum transported along e.
An adversary matrix for a colouring of an arbitrary type #
IsAdvMatrix is tied to a cube of inputs. The inner inputs of a composition
range over an arbitrary finite type, so the same notion is
needed there; at a cube the two are definitionally equal.
A symmetric matrix supported on pairs of differently-coloured points.
Equations
- QuantumQueryComplexity.IsAdvCol g N = (N.IsHermitian ∧ ∀ (u v : Y), g u = g v → N u v = 0)
Instances For
The bipartite-support lemma for a colouring of an arbitrary type: an
eigenvector with nonzero eigenvalue of an adversary matrix for g has support
in every colour class of g. (SourceBipartite proves this over an arbitrary
index type already; only the IsAdvMatrix wrapper was cube-tied.)
The spectral core over an abstract block decomposition #
The tensor eigenvector of the composed matrix.
Equations
- QuantumQueryComplexity.tensorVecE e g v w x = w (QuantumQueryComplexity.tildeE e g x) * ∏ i : α, v i (QuantumQueryComplexity.sliceE e x i)
Instances For
K3', the crux in general form: applying the composed matrix to a
tensor vector amounts to applying the outer auxiliary matrix Γf ⊙ Emat to
the outer factor. (HLŠ Lemma 16, Items 1–2, for an arbitrary outer
vector.)
K3: tensor vectors built from inner eigenvectors and an eigenvector of the outer auxiliary matrix are eigenvectors of the composed matrix, with the outer eigenvalue.
The cube instance #
Positive semidefinite matrices of bounded trace #
For a positive semidefinite matrix the spectral norm is at most the trace: the eigenvalues are nonnegative, so the largest is at most their sum.
The squared norm of a standard coordinate vector.
A linear functional bounded on a trace ball has the corresponding homogeneous bound in every nonzero rank-one direction.
The two convex sets of the separation argument, on a promise domain #
The shared implementation for promise and total inputs: the ambient coordinate space is
DualOmegaOn X → ℝ, the compact set is the image of the truncated positive
semidefinite cone over GramIdxOn X ι, and the closed set is the box around
the promise dual target. norm_le_trace_of_posSemidef and
apply_eq_sum_single are generic and imported, not re-proved.
The coordinate index of the ambient space: a pair of promise inputs for each constraint, and an input with a side tag for each cost variable.
Instances For
The affine data of the promise dual program, read off a Gram matrix.
Equations
- QuantumQueryComplexity.gramLOn read G = Sum.elim (fun (q : X × X) => QuantumQueryComplexity.gramROn read G q.1 q.2) fun (q : X × Bool) => QuantumQueryComplexity.gramCostOn G q.2 q.1
Instances For
gramLOn as a linear map.
Equations
- QuantumQueryComplexity.gramLOnₗ read = { toFun := QuantumQueryComplexity.gramLOn read, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Positive semidefinite matrices of trace at most T.
Equations
- QuantumQueryComplexity.psdBallOn X ι T = {G : Matrix (QuantumQueryComplexity.GramIdxOn X ι) (QuantumQueryComplexity.GramIdxOn X ι) ℝ | G.PosSemidef ∧ G.trace ≤ T}
Instances For
The two sets #
The image of the truncated positive semidefinite cone.
Equations
Instances For
The target of the promise dual program: constraint block equal to
dualTargetOn f, cost block in [0, c].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The corner of the box.
Equations
- QuantumQueryComplexity.dualCornerOn f c = Sum.elim (fun (q : X × X) => QuantumQueryComplexity.dualTargetOn f q.1 q.2) fun (x : X × Bool) => c
Instances For
The two convex sets of the separation argument #
The dual program is separated from its target inside the finite-dimensional
coordinate space DualOmega ι σ → ℝ, whose coordinates are indexed by a pair
of inputs (the constraint gramR) or by an input together with a side tag (the
two costs gramCost). The map assembling those coordinates from a Gram matrix
is gramL.
Two sets live there:
gramImage T, the image of the positive semidefinite matrices of trace at mostT— convex because the positive semidefinite cone is, and compact because that truncated cone is closed and bounded in a finite-dimensional space (‖G‖ ≤ G.tracefor positive semidefiniteG);dualBox g c, the points whose constraint block is the dual target and whose cost block lies in[0, c]— convex and closed.
Truncating the cone at a finite trace is what makes gramImage compact, and
hence what lets geometric_hahn_banach_compact_closed apply without any
closedness-of-image argument; the truncation is harmless because a dual
solution of cost at most c has trace at most 2 c · card (ι → σ).
This section also records apply_eq_sum_single, which reads the coefficients of a
continuous linear functional off its values on the standard basis.
The coordinate index of the ambient space of the separation argument: a pair of inputs for each constraint, and an input with a side tag for each cost variable.
Equations
Instances For
The affine data of the dual program, read off a Gram matrix.
Equations
Instances For
gramL as a linear map.
Instances For
Positive semidefinite matrices of trace at most T.
Equations
- QuantumQueryComplexity.psdBall ι σ T = QuantumQueryComplexity.psdBallOn (ι → σ) ι T
Instances For
The two sets #
The image of the truncated positive semidefinite cone: the affine data
achievable by dual solutions of total weight at most T.
Equations
Instances For
The target of the dual program: constraint block equal to dualTarget g,
cost block in [0, c].
Equations
Instances For
The corner of the box: the dual target with every cost variable at c.
Equations
Instances For
Reading off the coefficients of a functional #
From a positive semidefinite certificate to an adversary matrix #
This section contains the elementary half of strong duality: the construction that turns the multipliers produced by a separating hyperplane back into a feasible primal witness.
The data is a symmetric matrix Γ, a strictly positive weight p on inputs,
and the inequality
|s ⬝ᵥ (Γ ⊙ advD i) *ᵥ t| ≤ ∑ₓ p x · s x ² + ∑ᵧ p y · t y ² (for every i),
which says exactly that the block matrix [[diag p, (Γ ⊙ advD i)/2], [·, diag p]]
is positive semidefinite. Rescaling by √p on both sides turns it into the
adversary feasibility constraint: Γ' x y = Γ x y / (√(p x) √(p y)) satisfies
‖Γ' ⊙ advD i‖ ≤ 2. Masking off the pairs with equal g-value costs nothing
in norm (l2_opNorm_hadamard_dualTarget_le, using that a two-valued mask is an
average of the identity and a ±1 diagonal conjugation), and evaluating the
resulting adversary matrix on the unit vector √p / ‖√p‖ returns the pairing
⟪Γ, dualTarget g⟫ / (2 ∑ p).
The generic norm estimate is proved here. The total-input certificate theorem
lt_advPM_of_certificate is derived from the promise construction below.
Two auxiliary norm bounds #
A bilinear form dominated by the sum of the squared lengths of its
arguments comes from a matrix of norm at most 2. (Optimising the scaling
a ↦ λ a, b ↦ λ⁻¹ b is what turns the arithmetic mean into the geometric
one.)
The main construction #
The primal witness API on a promise domain #
SourcePromiseDefs supplies the upper eliminator
advPMOn_le; this section supplies the introduction rules, so that a witness
matrix certifies ‖Γ‖ ≤ advPMOn read f directly.
There is one hypothesis here that the total case does not need. advPM is a
supremum over feasible matrices, and boundedness of that set comes from the
observation that a feasible matrix vanishes wherever no query separates the two
inputs. On a promise domain two distinct inputs may look identical at every
query, and then nothing constrains Γ there at all: the value set is unbounded
and sSup degenerates. So every lemma below assumes
hdet : ∀ x y, read x = read y → f x = f y,
i.e. the observations determine the output. Injectivity of read implies
this condition, as separates_of_injective records.
An injective observation map determines the output.
All entries of a feasible matrix are bounded by 1: entries with equal
output vanish, and the rest are separated by some query.
The a priori bound making the advPMOn value set bounded above.
Every feasible matrix certifies a lower bound on advPMOn.
The un-normalized witness lemma on a promise domain. Exhibit a matrix,
bound its masked norms by c, and read off ‖Γ‖ / c.
The ε-accessor, for arguments that need a witness beating a given value.
The total case is a promise on the whole cube #
A sanity check that the promise API really extends the total one: reading the
identity on the full cube gives back advPM.
Spanning by tensor eigenvectors (HLŠ Lemma 16, Item 3) #
The family of tensor vectors tensorVecE e g (v' · (c ·)) (ofLp (W c j)) — over
all eigen-index assignments c : α → Y and all members j of an orthonormal
basis W c of the outer space — spans the whole composed space.
Route: pure tensors of orthonormal families are orthonormal
(tensor_orthonormalE, via the sum_prod_sliceE interchange), hence linearly
independent; their cardinality equals the dimension, so they span; and each
pure tensor lies in the span of the family because tensorVecE is linear in
its outer argument and W c is a basis.
As in SourceCompositionHat the block decomposition is abstract: everything is proved for
e : Z ≃ (α → Y) with Y an arbitrary finite type, and the cube statements are
the cubeBlocks instance. The only cube-specific step was the dimension count
Fintype.card ((α × β) → Bool) = Fintype.card (α → (β → Bool)), which is now
just Fintype.card_congr e.symm.
This section is the second (and last) WithLp/EuclideanSpace quarantine zone.
S2: transporting a spanning statement from EuclideanSpace to the
plain Pi module.
Spanning over an abstract block decomposition #
S1: pure tensors of orthonormal families are orthonormal.
S3: the tensor eigenvector family spans everything.
The cube instance #
S1, cube form.
S3, cube form.
Post-composition lowers the promise adversary bound #
An adversary matrix for g ∘ f is supported on pairs with g (f x) ≠ g (f y),
hence on pairs with f x ≠ f y — so it is an adversary matrix for f, with
the same feasibility. The suprema then compare directly:
advPMOn read (g ∘ f) ≤ advPMOn read f.
This is the promise mirror of the advPM_comp_le post-processing lemma, and
it is what makes the bit encoding of a finite output type free on the
adversary side: each output bit is a post-composition of f, so its promise
adversary bound is at most that of f.
An adversary matrix for a post-composition is one for the base function.
Post-composition lowers the promise adversary bound.
Relabelling the answers #
An injective relabelling of the oracle's answers changes nothing: the masks
advDOn only ask whether two promise inputs are distinguished at i.
The adversary bound is invariant under injective relabelling of the answers.
The norm of a composed matrix (HLŠ Lemma 16 / BL Lemma 21) #
‖composeE e g Γf M‖ = ‖Γf‖ * ∏ i, ‖M i‖ for symmetric Γf and g-shaped
inner matrices M i.
≤(normE_compose_le): every tensor eigenvector's eigenvalue is an eigenvalue of someΓf ⊙ Emat, bounded via the Schur-multiplier estimate; the tensor eigenvectors span, so the spanning-eigenvector bound applies. No sign-flipping analysis is needed (this replaces HLŠ's Item 4 — and repairs the gap in BL Lemma 21's Eq. (4), whose orthogonality claim fails for ±-paired eigenvalues of the dilation).≥(le_normE_compose): at the sign vertexEmatdegenerates to a±1-diagonal conjugate of(∏ ‖M i‖) • Γf, producing an explicit tensor eigenvector with eigenvalue± ‖Γf‖ * ∏ ‖M i‖; it is nonvanishing by the bipartite-support lemma.
As in SourceCompositionHat the block decomposition is abstract, and the cube statements
norm_compose_le / le_norm_compose / norm_compose are the cubeBlocks
instance. Two side conditions appear in the general form and are automatic at
a cube: the ≤ direction is stated for a possibly empty composed type Z
(the spanning-eigenvector bound wants Nonempty), and the ≥ direction needs
Nonempty Y to select an inner eigenvalue of maximal modulus.
The vertex eigen-computation: at a sign vertex, an eigenvector of Γf
conjugated by the ±1 diagonal is an eigenvector of Γf ⊙ Emat R lam with
eigenvalue (∏ R) * θ.
The norm formula over an abstract block decomposition #
The ≤ direction of HLŠ Lemma 16.
The ≥ direction of HLŠ Lemma 16.
HLŠ Lemma 16 / BL Lemma 21, over an abstract block decomposition.
The cube instance #
The ≤ direction of HLŠ Lemma 16.
The ≥ direction of HLŠ Lemma 16.
HLŠ Lemma 16 / BL Lemma 21: the norm of the composed matrix.
From a certificate to an adversary matrix, on a promise domain #
The promise mirror of SourceDualityWitness: the multipliers of the
separating hyperplane become a feasible IsAdvMatrixOn witness, so the
certificate forces c < advPMOn read f. The two generic norm lemmas
(l2_opNorm_le_two_of_quadratic and the ±1 diagonal conjugation) are
imported, not re-proved; the ±1 mask argument uses only that the output
is two-valued, which holds verbatim for f : X → Bool.
hdet (read-determinacy) enters exactly once, through le_advPMOn — the
promise adversary bound is a supremum only over a bounded set when the
promise is determined.
Masking off the pairs with equal value does not increase the spectral
norm: for a two-valued f the mask is an average of the identity and a ±1
diagonal conjugation.
The main construction #
From a dual certificate to a primal witness, on a promise domain.
Total-input specializations of the promise witness construction #
A Boolean output mask is contractive in the operator norm.
The total-input certificate construction is the identity-read promise case.
The Hadamard-mask identity (HLŠ p. 20 / BL Eq. (8) + Claim 23) #
Masking the composed matrix by a difference matrix produces another composed
matrix: the outer matrix is masked by advD p and the inner matrix in slot p
is masked by the inner difference matrix at q:
composeE e g Γf M ⊙ advDOn (composeReadE e innerRead) (p, q) = composeE e g (Γf ⊙ advD p) (Function.update M p (M p ⊙ advDOn innerRead q))
This is an exact entrywise identity: in every configuration where the
‖·‖ • 1 part of a hat matrix could differ between the two sides, either the
outer factor (Γf ⊙ advD p) or a Kronecker delta vanishes first.
The mask is a promise mask #
The composed inputs form an arbitrary finite type Z ≃ (α → Y), and a query
(p, q) reads coordinate q of the p-th block through the inner
observation map innerRead : Y → β → σ (composeReadE). So the relevant
difference matrix is advDOn, evaluated on the inner observations.
Neither delicate step needs innerRead to be injective. In the "queries
agree" branch the p-slot hat entry vanishes because the masked inner entry
vanishes and the two blocks have different g-values, hence are distinct
blocks; in the "queries differ" branch the blocks are distinct because a single
congrArg turns differing reads into differing blocks.
The original cube statement compose_hadamard_advD is recovered as the
instance e := cubeBlocks α β with innerRead the identity, since
advDOn (fun u => u) q is advD q definitionally.
The mask identity over an abstract block decomposition #
The observation map of a composed input: the query (p, q) reads
coordinate q of the p-th block, through the inner observation map.
Equations
- QuantumQueryComplexity.composeReadE e innerRead z pq = innerRead (QuantumQueryComplexity.sliceE e z pq.1) pq.2
Instances For
The mask identity.
The cube instance #
The mask identity, cube form.
Strong duality for the adversary bound, on a promise domain #
The promise mirror of SourceDualityMain: for a read-determined Boolean
promise problem, every value above advPMOn read f is achieved by a feasible
DualPairOn:
exists_dualPairOn_of_advPMOn_lt :
advPMOn read f < c → ∃ m (P : DualPairOn read (Fin m) f), P.IsCostLe c.
The argument is the same single Hahn–Banach separation, run in the coordinate
space DualOmegaOn X → ℝ with the truncation T = 2c·|X|. Determinacy
(hdet) is a genuine hypothesis here: an undetermined pair
(read x = read y, f x ≠ f y) makes the dual program infeasible while the
primal supremum degenerates. In the proof it enters through le_advPMOn,
and in the no-query case (ι empty), where it forces f constant so the
zero dual is feasible; the X = ∅ case is vacuous and does not use it.
The ±1 masking trick
needs the output to be two-valued, which is the f : X → Bool hypothesis —
exactly the scope the Boolean characterization needs.
Combined with the promise-native lower bound and extraction
(SourceQuantumUpperBound), this yields the promise-Boolean characterization; see
SourceQuantumCharacterization.
Rank-one test matrices concentrated on one query position #
The vector of Gram indices carrying s on the u-side and t on the
v-side of the query position i₀, and zero elsewhere.
Equations
Instances For
Symmetrising a two-weight certificate #
The certificate with the two sides carrying different weights: averaging
reduces to the symmetric case, because advDOn read i and dualTargetOn f
are symmetric.
The separation argument #
Promise strong duality, existence form. For a read-determined Boolean promise problem, every value above the promise adversary bound is achieved by a feasible promise dual solution.
A nonconstant promise problem has advPMOn ≥ 1/2 #
The crude entrywise bound ‖M‖ ≤ ∑|M| on the elementary pair matrix loses a
factor of two against the total case's exact norm_pairMatrix, which is all
the characterization's constant bookkeeping needs.
The elementary promise adversary matrix supported on one symmetric pair.
Equations
- QuantumQueryComplexity.pairMatrixOn x y = Matrix.single x y 1 + Matrix.single y x 1
Instances For
A nonconstant promise problem has advPMOn ≥ 1/2: half the
elementary pair matrix is feasible.
The composition theorem for the negative-weight adversary bound #
Main result (advPM_mul_le_advPM_composeFun): for total Boolean functions
f : (α → Bool) → Bool and g : (β → Bool) → Bool,
ADV±(f) * ADV±(g) ≤ ADV±(f ∘ gᵏ)
— the composition lower bound of Høyer–Lee–Špalek (quant-ph/0611054,
Theorem 13, uniform unit-cost case) in the formulation of Belovs–Lee
(arXiv:2004.06439, Theorem 1, ≥ direction). The iterated corollary
advPM_pow_le_advPM_iterFun gives ADV±(f)^(d+1) ≤ ADV±(f^{∘(d+1)}).
Proof: for feasible witnesses Γf, Γg, the composed matrix
Γh = compose (constFam g) Γf (fun _ => Γg) is an adversary matrix for f ∘ gᵏ with
‖Γh‖ ≥ ‖Γf‖ ‖Γg‖^k (Lemma 16, ≥) and
‖Γh ⊙ advD (p,q)‖ ≤ ‖Γg‖^(k-1) (mask identity + Lemma 16, ≤), so the
un-normalized witness lemma yields advPM (f ∘ gᵏ) ≥ ‖Γf‖ ‖Γg‖; two
supremum passes finish the proof.
The masked norm bound for the composed witness (T1).
The composition theorem (HLŠ Theorem 13, uniform unit-cost case;
BL Theorem 1, ≥ direction): ADV±(f) * ADV±(g) ≤ ADV±(f ∘ gᵏ).
The iterated corollary #
Equations
- QuantumQueryComplexity.iterIdx.fintype α 0 = inst✝
- QuantumQueryComplexity.iterIdx.fintype α d.succ = { elems := QuantumQueryComplexity.iterIdx.fintype._aux_1 α d (QuantumQueryComplexity.iterIdx.fintype α d), complete := ⋯ }
Iterated composition f^{∘(d+1)}.
Equations
Instances For
Composition of dual solutions and the composition upper bound #
Dual solutions compose multiplicatively (Belovs–Lee, arXiv:2004.06439, Theorem 24; the construction is from LMRSS): tensoring an outer dual solution with an inner one,
u_{x,(p,q)} = ψ_{x_tilde,p} ⊗ u_{x·ₚ,q}, v_{x,(p,q)} = φ_{x_tilde,p} ⊗ v_{x·ₚ,q},
produces a feasible dual solution for f ∘ gᵏ of cost the product of the
costs (DualPair.compose). This is exactly where the LMRSS constraints on
pairs with g x = g y are used: they kill the blocks where the inner
function values agree.
Consequently advDual (f ∘ gᵏ) ≤ advDual f * advDual g, and by weak duality
ADV±(f ∘ gᵏ) ≤ advDual f * advDual g (advPM_composeFun_le_advDual_mul)
unconditionally. Combined with the lower bound
advPM_mul_le_advPM_composeFun this sandwiches the composed value. The
perfect composition theorem ADV±(f ∘ gᵏ) = ADV±(f) · ADV±(g) follows by
applying advPM_composeFun_eq_of_dual_eq to the strong-duality theorem
advDual_eq_advPM in SourceDualityMain. The unconditional endpoint is
advPM_composeFun_eq.
The c-weighted cost of a dual solution is bounded by V.
Stated for a general alphabet and output type: the weighted cost is what the
outer solution of a composition must control, and in
SourceComposeShared the outer function is a non-Boolean maximum.
Equations
Instances For
Composition of dual solutions (BL Theorem 24 construction).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inner mass bounds give a weighted bound on the block tensor's mass.
Weighted dual composition: a c-weighted outer bound composes with
inner solutions of costs c i to an ordinary bound.
The cost of a composed dual solution is the product of the costs.
The composition upper bound, unconditional: the adversary bound of a composed function is at most the product of the dual values.
The composed adversary bound is sandwiched between the product of the primal values and the product of the dual values.
Perfect composition from supplied duality equalities. The unconditional
advPM_composeFun_eq below discharges these using advDual_eq_advPM.
Functions whose adversary bound is certified on both sides #
HasAdvValue f c records that the adversary bound of f equals c and
that this value is certified by a dual solution — i.e. strong duality holds at
f. This is exactly the hypothesis needed for perfect composition, and it is
established for concrete functions by exhibiting a matching primal/dual pair.
Equations
Instances For
Building a HasAdvValue from a primal lower bound and a dual upper bound:
weak duality squeezes them together.
Certified values compose exactly. If strong duality holds at f and
at g, then it holds at f ∘ gᵏ, with the product value.
The weighted composition lower bound #
The composition machinery now allows a different inner function in each
block (compose g Γf M with g : α → (β → Bool) → Bool), which is what the
cost/weighted version of the adversary composition theorem needs.
advPM_composeFunFam_ge is the general weighted statement: if the outer
witness Γf satisfies
‖Γf ⊙ D_p‖ · V ≤ ‖Γf‖ · ‖M p‖ for every outer coordinate p,
— i.e. Γf certifies the value V for f with costs ‖M p‖ — and each
inner witness M i is feasible, then ADV±(f ∘ (g_1, …, g_k)) ≥ V.
This is HLŠ Theorem 13 (ADV±_α(h) ≥ ADV±_β(f) with β_i = ADV±(g_i)) in
witness form: the cost vector enters as the norms ‖M p‖ of the inner
witnesses, so no separate ADV±_α definition is needed.
The weighted composition lower bound.
The two-bit AND and OR functions have adversary bound √2 #
We compute ADV±(AND₂) = ADV±(OR₂) = √2 with a matching dual certificate,
i.e. we establish HasAdvValue and2 (√2) and HasAdvValue or2 (√2). Strong
duality is therefore available at these functions unconditionally, so the
perfect composition theorem applies to them.
The primal witness is the star matrix of HLŠ §6: the adversary matrix
supported on the two edges joining 11 to its neighbours 01 and 10. Its
spectral norm is √2 and each masked norm ‖Γ ⊙ D_i‖ is 1.
The dual witness is one-dimensional (K = Unit), with weights
α = 2^(-1/4) at 11, β = 2^(1/4) on the sensitive coordinate of each
neighbour, and δ = 2^(1/4)/2 at 00; its cost is exactly √2.
Enumeration of the four two-bit inputs #
The two-bit AND function and its primal witness #
The top eigenvector of the star matrix.
Equations
Instances For
The dual witness #
α = 2^(-1/4).
Instances For
δ = 2^(1/4)/2.
Instances For
The dual solution for AND₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ADV±(AND₂) = √2, with a matching dual certificate.
Invariance of the adversary bound under relabelling #
Negating the output, or negating a set of input bits, changes neither the
primal nor the dual value. This transfers the AND₂ computation to OR₂.
The two-bit OR function #
ADV±(OR₂) = √2, with a matching dual certificate.
Strong duality for total-input adversary bounds #
The total-input existence theorem specializes exists_dualPairOn_of_advPMOn_lt
at the identity read and transports the resulting certificate with
DualPairOn.toTotal. The Hahn–Banach separation argument is proved once, in
SourceDualityMainOn; the certificate and mask bounds are specialized in
TotalDualitySpecialization.
The total-input Gram helpers below remain available for clients of that API.
Weak duality then gives advDual g = advPM g for Boolean functions, followed
by the exact block-composition corollaries.
Rank-one test matrices concentrated on one query position #
The vector of Gram indices carrying s on the u-side and t on the
v-side of the query position i₀, and zero elsewhere.
Equations
Instances For
Symmetrising a two-weight certificate #
The certificate of lt_advPM_of_certificate with the two sides carrying
different weights: averaging Ξ with its transpose and the two weights with
each other reduces to the symmetric case, because advD i and dualTarget g
are symmetric.
The separation argument #
Strong duality, existence form. Above the adversary bound every value is achieved by a feasible dual solution.
Strong duality #
Strong duality for the adversary bound. The LMRSS dual program has no
gap: its value equals ADV±.
Consequences #
Perfect composition, unconditionally: the adversary bound is exactly multiplicative under composition.
Every Boolean function carries a matching primal/dual pair of witnesses.
Star adversary matrices #
A star matrix with centre c and leaf set S is ∑ z ∈ S, pairMatrix z c:
the symmetric matrix whose only nonzero entries are the unit weights joining
c to each leaf. Its spectral norm is √|S| (norm_starMatrix), and
masking it by a difference matrix restricts the leaf set to those leaves
differing from the centre in that coordinate
(starMatrix_hadamard_advD).
These are the optimal primal witnesses for OR and AND, and specialise to
the two-bit case of SourceAndOr.
Generic sum manipulations #
The star matrix #
The star matrix with centre c and leaves S.
Equations
- QuantumQueryComplexity.starMatrix S c = ∑ z ∈ S, QuantumQueryComplexity.pairMatrix z c
Instances For
The top eigenvector of a star matrix.
Instances For
Weighted star matrices #
Giving the edges weights w replaces the leaf count |S| by the total
squared weight ∑ w². This is what the cost version of the adversary
bound needs: for OR_k with costs c, the weighted star with w = c
certifies the value √(∑ cᵢ²) with masked norms cᵢ.
The star matrix with centre c, leaves S and edge weights w.
Equations
- QuantumQueryComplexity.wStarMatrix S c w = ∑ z ∈ S, w z • QuantumQueryComplexity.pairMatrix z c
Instances For
The total squared weight of a star.
Equations
- QuantumQueryComplexity.starWeight S w = ∑ z ∈ S, w z * w z
Instances For
The top eigenvector of a weighted star matrix.
Equations
Instances For
ADV±(OR_n) = ADV±(AND_n) = √n #
We compute the adversary bound of the n-bit OR and AND functions, with
matching dual certificates, so strong duality holds at them and they compose
perfectly.
- the primal witness for
OR_nis the star matrix centred at the all-zero input with thenweight-one inputs as leaves (SourceStar); its norm is√nand each masked norm is1; - the dual witness is one-dimensional: weight
δ = n^(-1/4)at the all-zero input, and1/(|x| δ)on the support of each nonzerox, where|x|is the Hamming weight. Its cost is exactly√n.
AND_n follows from OR_n by De Morgan, using the relabelling invariance
lemmas of SourceAndOr.
The n-bit OR function #
The all-zero input.
Equations
Instances For
The input with a single true in position i.
Equations
- QuantumQueryComplexity.unitVec i j = decide (j = i)
Instances For
The leaf set of the OR star matrix.
Instances For
The primal witness #
The dual witness #
n δ² = √n.
ADV±(OR_n) = √n, with a matching dual certificate.
The n-bit AND function #
ADV±(AND_n) = √n, with a matching dual certificate.
The weighted OR witness and weighted OR-composition #
The weighted star centred at the all-zero input, with weight c i on the
edge to the i-th unit input, is the optimal cost-c witness for OR_n:
its norm is √(∑ cᵢ²) and its i-th masked norm is cᵢ
(norm_orWStar, norm_orWStar_hadamard).
Feeding it into the weighted composition theorem gives the key inductive step for read-once formulas:
ADV±(OR_k ∘ (g₁, …, g_k)) ≥ √(∑ᵢ ADV±(gᵢ)²)
(sqrt_sum_sq_le_advPM_composeFunFam_orN), and the same for AND_k by
De Morgan.
The weighted star witness for OR_n with costs c.
Equations
Instances For
The weighted OR-composition lower bound. Composing OR_k with
inner functions certified by witnesses M i gives at least
√(∑ᵢ ‖M i‖²).
Composing AND is composing OR with negated inner functions, up to
negating the output.
The same bound for AND_k, by De Morgan.
The weighted dual and weighted dual composition #
The cost side of the weighted composition theorem. Composing an outer dual
solution with inner ones of costs c i gives a composed cost
∑_p c_p ‖ψ_{x_tilde,p}‖²,
which is the c-weighted cost of the outer solution
(DualPair.IsWeightedCostLe). So DualPair.compose_isWeightedCostLe turns
a weighted outer bound into an ordinary bound on the composition.
For OR_n with costs c the optimal weighted dual is one-dimensional, with
δₚ = √cₚ / √V at the all-zero input (where V = √(∑ cᵢ²)) and
1 / (∑_{p ∈ supp x} δₚ) on the support of each nonzero x; its c-weighted
cost is exactly V (orWDual_isWeightedCostLe). Composing gives
advDual (OR_k ∘ (g₁, …, g_k)) ≤ √(∑ᵢ cᵢ²)
whenever the inner functions have dual solutions of cost cᵢ
(advDual_composeFunFam_orN_le), matching the primal bound of
SourceWeightedOr.
The weighted cost of a dual solution #
The weighted OR dual #
δₚ = √cₚ / √V.
Equations
- QuantumQueryComplexity.orWDelta c p = √(c p) / √(QuantumQueryComplexity.orWVal c)
Instances For
The one-dimensional weighted dual weights for OR_n.
Equations
- QuantumQueryComplexity.orWDualVec c x p = if x = QuantumQueryComplexity.zeroVec then QuantumQueryComplexity.orWDelta c p else if x p = true then 1 / QuantumQueryComplexity.orWSupp c x else 0
Instances For
The weighted OR-composition upper bound #
The weighted OR-composition upper bound, matching the primal bound
sqrt_sum_sq_le_advPM_composeFunFam_orN.
Dual composition with shared inputs #
The composition in SourceDualCompose gives each inner function its
own block of variables (composeFunFam over α × β). Divide-and-conquer needs
the opposite: finitely many subproblems g p, all reading the same input x,
whose domains typically overlap. Write
sharedFun h g x = h (fun p => g p x).
Duals compose in this setting too, and the argument is shorter than the disjoint
one. Tensoring the outer solution at p with the p-th inner solution,
u x i = ⊕_p U_{g(x)} p ⊗ u^p x i, v y i = ⊕_p V_{g(y)} p ⊗ v^p y i,
the masked sum factors as
∑_{i : x i ≠ y i} ⟨u x i, v y i⟩ = ∑_p ⟨U_{g x} p, V_{g y} p⟩ · [g p x ≠ g p y],
which is exactly the outer constraint evaluated at the pair (g x, g y). No
property of the inner functions' supports is used, so they may overlap freely.
The cost telescopes the same way: the p-th block contributes
‖U_{g x} p‖² times the p-th inner cost, so an outer solution of weighted
cost V with weights c and inner solutions of cost c p compose to cost V
(DualPair.composeShared_isCostLe). That is the whole quantitative content of
"solve subproblem p at cost c p, then optimise over p".
The first-difference dual: ADV±(f) ≤ 2n for every f #
Order the coordinates arbitrarily. For inputs x ≠ y there is exactly one
coordinate at which they first differ, so
∑_{i : x i ≠ y i} [x agrees with y before i] = 1.
Tensoring that indicator with a cheap factorization of the "different output"
matrix, ⟨φ_a, ψ_b⟩ = [a ≠ b], turns it into a feasible dual solution: the
count 1 is switched on precisely when f x ≠ f y, and the LMRSS equality
constraints hold because the φψ factor already vanishes there. Each input
puts mass ‖φ‖² = 2 on each of the n coordinates, so the cost is 2n.
This is the dual attached to the trivial decision tree that reads every
coordinate in order. Its point here is that the bound carries no alphabet
dependence at all, so it complements upstream Max/Dyadic.lean, whose
2⌈log₂ m⌉√n degrades for very large alphabets.
The same construction applied to an arbitrary decision tree gives
ADV±(f) ≤ 2 D(f), and averaging duals (which is legitimate, since the
constraint is linear in ⟨u, v⟩) gives ADV±(f) ≤ 2 R₀(f). Neither helps for
maximum finding, where every coordinate must be read: D(MAX) = R₀(MAX) = n.
An arbitrary ordering of the coordinates #
An arbitrary injective ranking of the finite index type; it supplies the "reading order" of the trivial decision tree.
Equations
Instances For
Exactly one first difference #
The coordinates at which x and y differ for the first time.
Equations
- QuantumQueryComplexity.firstDiffSet x y = {i : ι | x i ≠ y i ∧ QuantumQueryComplexity.prefixOf x i = QuantumQueryComplexity.prefixOf y i}
Instances For
Distinct inputs have exactly one first difference.
A cheap factorization of the "different output" matrix #
The dual solution #
The dual solution of the trivial decision tree that reads every coordinate
in the order given by idxRank.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ADV±(f) ≤ 2n for every function on n variables, with no dependence
on the input alphabet or the output type.
Each input puts mass exactly ‖φ‖² = 2 on each coordinate.
The weighted cost of the first-difference dual: mass 2 on every
coordinate, so the c-weighted cost is 2 ∑ c.
Averaging dual solutions #
The dual constraint is linear in ⟨u x i, v y i⟩, so a convex combination
of solutions for the same function is again a solution: scale the z-th by
√(p z) and take an orthogonal direct sum, and the pairing averages copies of
the same number [f x ≠ f y].
What makes this worth doing is the cost. The averaged solution costs
∑ z, p z · (cost of the z-th solution at that input)
per input — an average of costs, not a cost of averages. A family of
solutions that is individually bad but good on average is therefore fine, which
is exactly the situation for maximum finding: for a fixed scan order an
increasing input sets a record at every step, but over a uniformly random order
the probability of a record at step t is only 1/t.
A convex combination of dual solutions for the same function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The averaged cost is the average of the costs, input by input.
The averaged weighted cost is the average of the weighted costs.
The uniform average over a nonempty finite family.
Equations
- QuantumQueryComplexity.DualPair.averageUnif P = QuantumQueryComplexity.DualPair.average P (fun (x : Z) => (↑(Fintype.card Z))⁻¹) ⋯ ⋯
Instances For
The averaged ℓ² mass at a single input. Exposing this, rather than
only the cost bound it implies, is what lets a dual solution be restricted to a
promise domain: its cost there is the maximum of these over the promise
only.
Weighted scans: the decision-tree dual with black/red weights #
A scan orders the coordinates and records, for each input and coordinate, the branch taken there and its colour. This is the algebraic core of Beigi–Taghavi's generalized-decision-tree dual, with weights assigned to nodes.
The point of the reformulation used here is that a scan is
SourceFirstDiff applied to the branch sequence instead of the raw
input. A tree node is exactly a branch-prefix, so "two paths agree until their
first different branch" is literally card_firstDiffSet, and no tree datatype is
needed. Three conditions make the argument go through:
br_ne— a differing branch forces a differing symbol, so the coordinate is visible to the adversary mask;out_eq— equal branch sequences force equal outputs, so the pairing is switched on whenever the outputs differ;black_unique— at most one branch at a node is black, which is what makes the two square-root weights cancel.
The colours are what the ordinary first-difference dual lacks. u pays
1 / W at the branch it takes, while v pays ∑ W over the other colours;
choosing W per coordinate then trades the two costs off against each other.
With constant weights this collapses back to ADV±(f) ≤ 2 D(f); with
depth-dependent weights it is what removes the alphabet dependence from maximum
finding.
A scan of the coordinates: an order, and for each input the branch taken at each coordinate together with its colour.
- rank : ι → Fin (Fintype.card ι)
The order in which coordinates are scanned.
- rank_inj : Function.Injective self.rank
The order is a genuine ordering.
- br : (ι → σ) → ι → Q
The branch taken at each coordinate.
- col : (ι → σ) → ι → Bool
Its colour:
falseis black,trueis red. - out : (ι → σ) → O
The value computed.
- br_ne (x y : ι → σ) (i : ι) : (∀ (j : ι), self.rank j < self.rank i → self.br x j = self.br y j) → self.br x i ≠ self.br y i → x i ≠ y i
At the same node, a differing branch forces a differing symbol: the branches at a node partition the alphabet, so the branch is determined by the symbol read.
Equal branch sequences force equal outputs.
- black_unique (x y : ι → σ) (i : ι) : self.col x i = false → self.col y i = false → (∀ (j : ι), self.rank j < self.rank i → self.br x j = self.br y j) → self.br x i = self.br y i
At most one branch at each node is black.
Instances For
Exactly one first divergence #
The coordinate at which two branch sequences first differ.
Instances For
The dual solution attached to a weighted scan #
u sits at the branch it takes, weighted 1/√W; v spreads over the other
colours, weighted √W. At the first differing branch the two square roots
cancel — this is where black_unique is used, since it rules out both sides
taking a black branch at the same node, which would leave no common colour.
The resulting costs are
∑ i, ‖u x i‖² ≤ 4 ∑ i, 1 / W i (col x i),
∑ i, ‖v y i‖² ≤ 4 ∑ i, (W i true + if col y i then W i false else 0),
so the weights trade one side against the other. Constant weights give the first-difference dual back; the maximum scan will make them depend on depth.
The dimension type: node, colour, branch gadget, output gadget.
Instances For
The dual solution #
The dual solution attached to a weighted scan.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exact ℓ² mass of u at one coordinate: the reciprocal weight of the
branch taken there.
Stated per coordinate, not just summed, because a weighted cost inserts a different factor at each one.
The exact ℓ² mass of u at an input: the reciprocal weights of the
branches taken.
The exact ℓ² mass of v at one coordinate: the weights of the other
colours.
The exact ℓ² mass of v at an input: the weights of the other colours.
The weighted cost of the scan dual. Each coordinate contributes its own
factor c i, which is what a composition with subproblems of differing costs
consumes.
The cost of the scan dual: u pays the reciprocal weight of the branch it
takes, v pays the weights of the other colours.
The maximum scan #
Scan the coordinates in a fixed order, keeping the largest value seen. At each
step the branch is black when the new value does not beat the running maximum,
and is the red singleton {x i} when it does.
The branch label is taken to be the running maximum after scanning i,
runAfter. This is what makes the three Scan conditions nearly free, and it
avoids induction entirely:
- the running maximum before
iis the sup of the labels strictly beforei, so equal branch prefixes give equal running maxima — no recursion needed; br_nethen saysa ⊔ x i ≠ a ⊔ y i → x i ≠ y i, which is immediate;black_uniquesays two non-records at the same node take the same branch — both labels are just the running maximuma;out_eqholds becausemaxFun xis the sup of the labels.
A branch is red exactly when the step is a strict record. That is the event
whose probability, over a uniformly random scan order, is at most 1/t — the
estimate that will make the weighted cost O(√n).
WithBot α is definitionally Option α; mathlib carries no Fintype
instance for it, and the scan needs one because the branch labels are running
maxima.
Equations
- QuantumQueryComplexity.instFintypeWithBot = { elems := QuantumQueryComplexity.instFintypeWithBot._aux_1, complete := ⋯ }
The running join #
Nothing about the running value of a scan needs a linear order: it is a
supremum, so a SemilatticeSup suffices. Keeping this section general is what
lets upstream Scan/Join.lean reuse it for products in a commutative
idempotent semigroup, where two values may be incomparable.
The coordinates scanned strictly before i.
Equations
- QuantumQueryComplexity.beforeSet rk i = {j : ι | rk j < rk i}
Instances For
The running maximum strictly before i (⊥ if nothing has been scanned).
Equations
- QuantumQueryComplexity.runBefore rk x i = (QuantumQueryComplexity.beforeSet rk i).sup fun (j : ι) => ↑(x j)
Instances For
The running maximum up to and including i.
Equations
- QuantumQueryComplexity.runAfter rk x i = QuantumQueryComplexity.runBefore rk x i ⊔ ↑(x i)
Instances For
The running maximum before i is the sup of the branch labels before
i. This is what replaces an induction on the scan order.
Equal branch prefixes give equal running maxima.
The maximum scan #
maxFun is the sup of the branch labels.
The scan #
Whether scanning i sets a strict record.
Equations
- QuantumQueryComplexity.isRecord rk x i = decide (QuantumQueryComplexity.runBefore rk x i < ↑(x i))
Instances For
The maximum scan, for a given order of the coordinates and a given
value map m : σ → A.
The letters read by the queries need not be the values being maximised: a query
returns a whole letter x i : σ, and the quantity of interest is the largest
m (x i). This costs the construction nothing, because the three Scan
conditions only ever go in the direction "differing branch ⟹ differing letter",
and m (x i) ≠ m (y i) certainly forces x i ≠ y i. A non-injective m is
therefore fine — which matters, since the entries of distinct letter matrices
routinely coincide.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The maximum scan of the input itself: the value map is the identity.
Equations
- QuantumQueryComplexity.maxScan rk hrk = QuantumQueryComplexity.maxScanMap id rk hrk
Instances For
The record lemma #
Over a uniformly random scan order, the probability that step t sets a strict
record is at most 1 / (t + 1).
No bijection onto a quotient is needed. For each position s ≤ t let
domSet x t s be the orders whose position-s coordinate strictly dominates
all the others at positions ≤ t. Then
- the
domSet x t sfors ≤ tare pairwise disjoint — a strict dominator is unique; - they are equinumerous, by composing an order with the transposition of
positions
sandt; domSet x t tis exactly the event "steptis a strict record".
So (t + 1) disjoint sets of equal size fit inside all the orders, giving
(t + 1) * |record event| ≤ n!. Ties are handled for free: if the maximum
over the first t + 1 positions is attained twice, no order is counted, which
only helps.
This is the one place where randomising the scan order earns its keep. For a fixed order an increasing input sets a record at every step.
A scan order: a bijection of the coordinates onto positions.
Equations
- QuantumQueryComplexity.Order ι = (ι ≃ Fin (Fintype.card ι))
Instances For
The orders whose position-s coordinate strictly dominates every other
coordinate at a position ≤ t.
Equations
- QuantumQueryComplexity.domSet x t s = {e : QuantumQueryComplexity.Order ι | ∀ s' ≤ t, s' ≠ s → x ((Equiv.symm e) s') < x ((Equiv.symm e) s)}
Instances For
A strict dominator is unique, so the sets are pairwise disjoint.
Swapping positions s and t matches the two dominance events.
The record bound in counting form.
Identifying the record event #
The record event is exactly the top dominance set.
The record lemma. At most a 1/(t+1) fraction of scan orders make
step t a strict record.
ADV±(MAX) = O(√n), with no alphabet dependence #
Give the coordinate scanned at time t the
weights
W(t, black) = √(t+1), W(t, red) = 1/√(t+1),
and average the resulting scan duals over all scan orders. A red branch is a
strict record, which by the record lemma happens for at most a 1/(t+1)
fraction of orders, so at each time the two contributions balance:
√(t+1) · (fraction of records) + 1/√(t+1) ≤ 2/√(t+1),
and ∑_{t<n} 1/√(t+1) ≤ 2√n. Both squared masses are therefore O(√n).
The bound is independent of the alphabet. This is what the threshold/staircase
route could not achieve: there the pairing constraints force a γ₂ factorization
of the greater-than matrix, costing Θ(log m). The scan never compares two
alphabet symbols through an inner product — the comparison happens inside the
branch structure, and the dual only ever tests branch labels for equality.
The elementary sum #
∑_{t < n} 1/√(t+1) ≤ 2√n, by telescoping.
The weights #
The u-side weight at a coordinate: √(t+1) on a record, 1/√(t+1)
otherwise.
The v-side weight at a coordinate.
Summing over the scan order #
Reindexing a sum over coordinates as a sum over times.
The key per-time estimate. Summed over all scan orders, the u-side
cost at time t is at most 2 / √(t+1) times the number of orders.
The v-side analogue: at most 3 / √(t+1) per order.
The theorem #
ADV±(MAX) ≤ 24 √n, with no dependence on the alphabet, for the maximum
of a value map applied to the letters.
Averaging the depth-weighted scan duals over all scan orders. A red branch is a
strict record, which happens for at most a 1/(t+1) fraction of orders, so the
two colour contributions balance at every time and the total is governed by
∑_t 1/√(t+1) ≤ 2√n.
Nothing about the bound sees m: neither its injectivity nor the size of the
alphabet σ of letters plays any role.
The maximum of the input itself: the value map is the identity.
ADV±(MAX) ≤ 24 √n, with no dependence on the alphabet.
Bundled dual solutions #
A divide-and-conquer construction builds one dual solution out of many, and the
dimension types of the pieces are all different: a maximum over a block of q
positions carries Order and ScanDim types built from that block, a
first-difference combination carries prefix and output gadgets, and a recursive
call carries whatever its own subtree produced. Threading those types through a
recursion requires a Sigma type and DualPair.embedDim to combine the
different finite dimensions.
So we hide the dimension:
HasDual f c — some feasible dual solution for f has cost at most c;
HasWeightedDual f c V — some solution has c-weighted cost at most V.
Every construction of SourcePullback, SourceFirstDiff, and SourceComposeShared is
restated at this level, and the Sigma-plus-embedDim step happens exactly once,
inside HasWeightedDual.composeShared. What is left are two combinators that
say what divide-and-conquer actually does:
HasDual.combine— evaluate finitely many subproblems and feed the results to an arbitrary outer function, at cost2 ∑ₚ cₚ;HasDual.max— take the maximum ofqequally expensive subproblems, at cost24 √q · c, with no dependence on the alphabet of values.
Dimension types are pinned to Type; every construction in this development
produces one (Fin, Order, ScanDim, products, sums and sigmas of these).
The two predicates #
f has a feasible dual solution of cost at most c.
Equations
- QuantumQueryComplexity.HasDual f c = ∃ (K : Type) (x : Fintype K) (P : QuantumQueryComplexity.DualPair K f), P.IsCostLe c
Instances For
f has a feasible dual solution of c-weighted cost at most V.
Equations
- QuantumQueryComplexity.HasWeightedDual f c V = ∃ (K : Type) (x : Fintype K) (P : QuantumQueryComplexity.DualPair K f), P.IsWeightedCostLe c V
Instances For
Weak duality, bundled.
Constant weights #
The one quantitative fact linking the two predicates: an ordinary bound V
is a constant-weight bound c₀ V. This is what lets a family of equally
expensive subproblems be fed to an outer solution whose cost was measured
without weights.
Transport #
A dual solution only sees which inputs share an output value.
The feasibility constraint reads = if f x = f y then 0 else 1, so nothing but
the partition of inputs into level sets enters. Two functions inducing the same
partition therefore have the same dual solutions, at the same cost — even when
their output types are different. This is what makes it harmless to recode an
output into a finite type.
A dual solution restricted to a block of coordinates: injectivity of the inclusion is what keeps the cost unchanged.
A dual solution restricted along a padding. A function of n letters is
a function of N ≥ n letters whose last N - n are frozen at known values, and
freezing costs nothing.
Recoding the input alphabet along an injection.
A function that never changes value costs nothing: both vector families are
zero, and every dual constraint reads 0 = 0.
The zero solution has weighted cost zero for every weight vector, whatever its sign.
HasDual.ofKer for the weighted predicate: recoding the output changes
neither the feasible solutions nor their cost.
Composition with shared inputs #
This is the only place where dimension types are unified. The subproblems'
solutions live in types K p depending on p; the sigma type Σ p, K p holds
them all, and DualPair.embedDim moves each into it by padding with zeros, at
no cost.
The two combinators #
Feed finitely many subproblems to an arbitrary outer function.
The first-difference dual is feasible for any outer function, so nothing about
h is assumed: it may add two tropical path weights, take a maximum of level
summaries, or assemble a whole matrix out of its entries. The price is a factor
2 on the total of the subproblem costs.
The maximum of equally expensive subproblems.
24 √q is the alphabet-free cost of maximum finding on q coordinates
(SourceScanFinal); with constant weights it turns q subproblems of
cost c₀ into their maximum at cost 24 √q · c₀. The values compared may range
over any finite linear order, and the bound does not see how large it is.
Maximum of a value map over a block of coordinates #
The base case of every divide-and-conquer over letters: a query returns a whole letter, and the quantity wanted is the largest value of some map on the letters read in a given block.
The maximum of m over the letters, as a bundled dual.
MAX itself, as a bundled dual: hasDual_maxMap at the identity value
map, with the alphabet the finite linear order being maximized. The
operational Θ(√n) endpoints extracted from these certificates live in
upstream Quantum/MaxApplications.lean.
The maximum of m over the letters in a block, at a cost governed by the
size of the block.
Infinite value types #
The scan and the first-difference gadget both need finite branch and output
types, while the values a divide-and-conquer computes naturally live somewhere
infinite — tropical path weights are elements of ℝ ∪ {-∞}.
Nothing is lost. The input space ι → σ is finite, so every function on it has
finite range; restricting to that range changes neither the level sets nor, by
HasDual.ofKer, the dual solutions. The three combinators are therefore
restated with no finiteness assumption on the values at all, and it is these
versions that a recursion over tropical matrices consumes.
A strictly monotone map commutes with maxFun. Used to compare a maximum
computed inside a finite subtype of values with the same maximum computed
outside it.
The maximum of equally expensive subproblems, over any linear order of values.
An arbitrary outer function of finitely many subproblems, over any value and output types.
Postcomposition is available within a factor two. combine' with a
one-element index set: its outer function is arbitrary, so any recoding of
the output — a coarsening included — costs at most twice the original. It is
not free in general: a dual for f satisfies an equality constraint keyed to
f's level sets, and merging two of them turns a required 1 into a
required 0. Two is an upper bound obtained this way, not a lower bound on
what a coarsening must cost — a particular recoding may well be cheaper, and
an injective one is free (HasDual.ofKer). This is the priced form of the
joint-output discipline.
A joint may be collapsed onto anything it determines, within the same factor two — with the collapsing map obtained from the determination rather than supplied. This is the form a transcript compiler needs: it builds a joint and reads off the answer that the joint determines.
Every function of n letters costs 2n, whatever its output type. The
first-difference dual with the output recoded into its finite range.
A function of a single letter costs 2. Both the letter alphabet and
the output type are arbitrary.
A finite supremum, as a maximum over a nonempty index. Padding the index
set with a none carrying ⊥ makes an empty supremum legal, so no nonemptiness
hypothesis has to be threaded through a recursion.
The supremum of a finite family of equally expensive subproblems.
The workhorse of the divide-and-conquer: q candidates each solved at cost c₀
give their maximum at cost 24 √(q+1) · c₀. Stated for Finset.sup rather than
maxFun, so that an empty candidate set — the maximum of nothing is ⊥ — is
allowed and costs nothing extra.
Two subproblems fed to an arbitrary binary outer function. This is how
two tropical path weights are multiplied — h is (+) on ℝ ∪ {-∞} — and
nothing about h is used.
The maximum of a value map over a block of letters, over any linear order
of values. This is the base case of the tropical recursion: the largest
(s,t) entry among the letters read in a block.
Bundled dual solutions on a promise domain #
SourceHasDual hides the dimension type of a dual solution for a
total function; a divide-and-conquer recursion whose subproblems live on
input-dependent promises needs the same service on DualPairOn. This section
is that layer, plus the two structural moves every promise construction
needs:
DualPairOn.ofKer— the constraint sees the output only through the equality patternf x = f y, so a solution forfis a solution for anyf'with the same kernel, at the same vectors. This is what lets a descriptor chain be repackaged as a transcript without paying anything.HasDual.restrictToOn— a total solution restricts to a promise for free (DualPair.restrictTo), which is how the windowed element-distinctness duals ofED/*become the leaves of the LDS recursion.
Cost-0 solutions exist exactly for functions that are constant on the
promise (hasDualOn_of_const): on such a promise the constraint's right-hand
side is identically 0, so the zero vectors are feasible. That is the
"value determined by the transcript" case of descriptor composition.
Recoding the output #
Output recoding. A dual solution for f is a dual solution for any
f' with the same kernel on the promise — same vectors, same cost.
Instances For
Pulling a promise solution back along a map of promises. Every
sub-promise — in particular every fiber of a descriptor — inherits the
ambient solution at the same cost, since the constraint at (y, y') is the
constraint at (e y, e y').
Equations
Instances For
The zero solution is feasible for a function that is constant on the promise.
Equations
Instances For
The bundled predicate #
f has a feasible dual solution of cost at most c on the promise
domain read.
Equations
- QuantumQueryComplexity.HasDualOn read f c = ∃ (K : Type) (x : Fintype K) (P : QuantumQueryComplexity.DualPairOn read K f), P.IsCostLe c
Instances For
Weak duality on a promise, bundled.
Total solutions as promise solutions #
A total function is the promise problem over read = id, and a DualPair
is literally a DualPairOn there — the constraint's mask id x i = id y i
is definitionally x i = y i.
A total dual solution, read as a promise solution over read = id.
Instances For
A total bundled dual is a bundled promise dual over read = id.
The converse of HasDual.hasDualOn. With both directions available
the promise-side calculus — descriptor composition in particular — can be run
inside a total development and handed back as a HasDual.
Recoding the output of a bundled solution.
Replacing the function by a pointwise equal one.
Restricting a bundled promise solution to a sub-promise, at the same cost.
A function constant on the promise costs nothing.
Moving between query index types #
A solution that only queries a sub-family of coordinates. If the
promise is observed through ι' ↪ ι — the arena of a divide-and-conquer node
is such a sub-family of the word's positions — a solution written in arena
coordinates becomes one in the ambient coordinates, at the same cost: the
ℓ² mass moves to the image of the injection without accumulating
(spread).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Arena coordinates, bundled: a promise solution written in the coordinates of a sub-family costs the same in the ambient coordinates.
Restricting a total solution #
A total dual solution restricted to a promise domain, bundled: the
vectors are unchanged, so the cost is inherited. This is how the windowed
ED duals enter a promise-relativized recursion.