Finite quantum algorithms, query oracles, and simulation

Ported from the corresponding upstream modules listed by the source sections below. References beginning with Source name these retained sections.

Finite-dimensional complex Hilbert space for the query model

A quantum state on a finite basis type H is a function ψ : H → ℂ, an operator is a Matrix H H ℂ, and the action of an operator on a state is U *ᵥ ψ. We keep this raw, in the same spirit as the adversary side of the project: the inner product is a plain finite sum

qInner ψ φ = ∑ h, star (ψ h) * φ h,

conjugate-linear in the first argument, and the squared norm is qNormSq ψ = ∑ h, ‖ψ h‖².

Why not EuclideanSpace ℂ H? Because most arguments downstream — the query decomposition of a state by its index register, the progress measure of the adversary lower bound, the oracle's action on a product basis — are manipulations of finite sums over the basis, and WithLp/PiLp coercions get in the way of exactly those. So the raw form is the default.

It is not a quarantine, though: qInner_eq_euclidean and qNormSq_eq_euclidean below are public, and SourceQuantumProjector crosses by them deliberately, building subspaces and orthogonal projectors in EuclideanSpace where Mathlib's theory lives and carrying the results back as matrices. Raw by default, Euclidean where Mathlib is stronger.

Main definitions

• qInner, qNormSq, IsQState (a unit vector).
• qBasis h — the computational basis state |h⟩.
• Matrix.unitaryGroup H ℂ is Mathlib's; qPerm e is the unitary that sends |b⟩ to |e b⟩, which is how every permutation oracle enters.
• IsQProjector P and the reflection qRefl P = 2P - 1.

Main results

• qInner_mulVec_mulVec, qNormSq_mulVec, IsQState.mulVec — a unitary preserves inner products, squared norms, and unit states.
• qInner_norm_le — Cauchy–Schwarz.
• qInner_mulVec_left — moving an operator across the inner product.
• qPerm_mem_unitaryGroup, qPerm_mulVec, qPerm_involutive.
• qRefl_mem_unitaryGroup, qRefl_mul_self.

The inner product

def QuantumQueryComplexity.qInner {H : Type u_1} [Fintype H] (ψ φ : H → ℂ) : ℂ

The Hermitian inner product on H → ℂ, conjugate-linear in the first argument (the physicists' convention, and Mathlib's).

Equations

• QuantumQueryComplexity.qInner ψ φ = star ψ ⬝ᵥ φ

theorem QuantumQueryComplexity.qInner_def {H : Type u_1} [Fintype H] (ψ φ : H → ℂ) : qInner ψ φ = ∑ h : H, star (ψ h) * φ h

def QuantumQueryComplexity.qNormSq {H : Type u_1} [Fintype H] (ψ : H → ℂ) : ℝ

The squared norm of a state, as a real number.

Equations

• QuantumQueryComplexity.qNormSq ψ = ∑ h : H, Complex.normSq (ψ h)

theorem QuantumQueryComplexity.qNormSq_def {H : Type u_1} [Fintype H] (ψ : H → ℂ) : qNormSq ψ = ∑ h : H, Complex.normSq (ψ h)

def QuantumQueryComplexity.IsQState {H : Type u_1} [Fintype H] (ψ : H → ℂ) : Prop

A (pure) quantum state: a unit vector.

Equations

• QuantumQueryComplexity.IsQState ψ = (QuantumQueryComplexity.qNormSq ψ = 1)

theorem QuantumQueryComplexity.qNormSq_nonneg {H : Type u_1} [Fintype H] (ψ : H → ℂ) : 0 ≤ qNormSq ψ

@[simp]

theorem QuantumQueryComplexity.qInner_self {H : Type u_1} [Fintype H] (ψ : H → ℂ) : qInner ψ ψ = ↑(qNormSq ψ)

theorem QuantumQueryComplexity.qInner_conj {H : Type u_1} [Fintype H] (ψ φ : H → ℂ) : star (qInner ψ φ) = qInner φ ψ

@[simp]

theorem QuantumQueryComplexity.qInner_zero_left {H : Type u_1} [Fintype H] (φ : H → ℂ) : qInner 0 φ = 0

@[simp]

theorem QuantumQueryComplexity.qInner_zero_right {H : Type u_1} [Fintype H] (ψ : H → ℂ) : qInner ψ 0 = 0

theorem QuantumQueryComplexity.qInner_add_right {H : Type u_1} [Fintype H] (ψ φ χ : H → ℂ) : qInner ψ (φ + χ) = qInner ψ φ + qInner ψ χ

theorem QuantumQueryComplexity.qInner_add_left {H : Type u_1} [Fintype H] (ψ φ χ : H → ℂ) : qInner (ψ + φ) χ = qInner ψ χ + qInner φ χ

theorem QuantumQueryComplexity.qInner_sub_left {H : Type u_1} [Fintype H] (ψ φ χ : H → ℂ) : qInner (ψ - φ) χ = qInner ψ χ - qInner φ χ

theorem QuantumQueryComplexity.qInner_sub_right {H : Type u_1} [Fintype H] (ψ φ χ : H → ℂ) : qInner ψ (φ - χ) = qInner ψ φ - qInner ψ χ

theorem QuantumQueryComplexity.qInner_smul_right {H : Type u_1} [Fintype H] (c : ℂ) (ψ φ : H → ℂ) : qInner ψ (c • φ) = c * qInner ψ φ

theorem QuantumQueryComplexity.qInner_smul_left {H : Type u_1} [Fintype H] (c : ℂ) (ψ φ : H → ℂ) : qInner (c • ψ) φ = star c * qInner ψ φ

theorem QuantumQueryComplexity.qInner_sum_right {H : Type u_1} [Fintype H] {α : Type u_2} (ψ : H → ℂ) (s : Finset α) (F : α → H → ℂ) : qInner ψ (∑ i ∈ s, F i) = ∑ i ∈ s, qInner ψ (F i)

theorem QuantumQueryComplexity.qInner_sum_left {H : Type u_1} [Fintype H] {α : Type u_2} (s : Finset α) (F : α → H → ℂ) (φ : H → ℂ) : qInner (∑ i ∈ s, F i) φ = ∑ i ∈ s, qInner (F i) φ

@[simp]

theorem QuantumQueryComplexity.qNormSq_zero {H : Type u_1} [Fintype H] : qNormSq 0 = 0

theorem QuantumQueryComplexity.qNormSq_smul {H : Type u_1} [Fintype H] (c : ℂ) (ψ : H → ℂ) : qNormSq (c • ψ) = Complex.normSq c * qNormSq ψ

theorem QuantumQueryComplexity.qNormSq_add {H : Type u_1} [Fintype H] (ψ φ : H → ℂ) : qNormSq (ψ + φ) = qNormSq ψ + qNormSq φ + 2 * (qInner ψ φ).re

The parallelogram expansion.

theorem QuantumQueryComplexity.qNormSq_eq_zero_iff {H : Type u_1} [Fintype H] {ψ : H → ℂ} : qNormSq ψ = 0 ↔ ψ = 0

The Euclidean bridge

The sanctioned crossing between the raw representation used everywhere here and Mathlib's inner-product-space library. These two lemmas are public on purpose: the reflection constructors of the upper bound build a subspace in EuclideanSpace ℂ H, take Mathlib's Submodule.starProjection, transport it back through WithLp.linearEquiv, and turn it into a matrix with LinearMap.toMatrix'. That route needs to state its correctness in raw terms, and these are the lemmas that let it.

Everything else in this section stays raw: the bridge is a door, not a move.

theorem QuantumQueryComplexity.qInner_eq_euclidean {H : Type u_1} [Fintype H] (ψ φ : H → ℂ) : qInner ψ φ = inner ℂ (WithLp.toLp 2 ψ) (WithLp.toLp 2 φ)

theorem QuantumQueryComplexity.qNormSq_eq_euclidean {H : Type u_1} [Fintype H] (ψ : H → ℂ) : qNormSq ψ = ‖WithLp.toLp 2 ψ‖ ^ 2

theorem QuantumQueryComplexity.qInner_norm_le {H : Type u_1} [Fintype H] (ψ φ : H → ℂ) : ‖qInner ψ φ‖ ≤ √(qNormSq ψ) * √(qNormSq φ)

Cauchy–Schwarz.

theorem QuantumQueryComplexity.sqrt_qNormSq_add_le {H : Type u_1} [Fintype H] (ψ φ : H → ℂ) : √(qNormSq (ψ + φ)) ≤ √(qNormSq ψ) + √(qNormSq φ)

The triangle inequality, in squared-norm form.

Basis states

def QuantumQueryComplexity.qBasis {H : Type u_1} [DecidableEq H] (h : H) : H → ℂ

The computational basis state |h⟩.

Equations

• QuantumQueryComplexity.qBasis h = Pi.single h 1

@[simp]

theorem QuantumQueryComplexity.qBasis_apply {H : Type u_1} [DecidableEq H] (h k : H) : qBasis h k = if k = h then 1 else 0

@[simp]

theorem QuantumQueryComplexity.qNormSq_qBasis {H : Type u_1} [Fintype H] [DecidableEq H] (h : H) : qNormSq (qBasis h) = 1

theorem QuantumQueryComplexity.isQState_qBasis {H : Type u_1} [Fintype H] [DecidableEq H] (h : H) : IsQState (qBasis h)

Unitaries

theorem QuantumQueryComplexity.one_mem_qUnitary {H : Type u_1} [Fintype H] [DecidableEq H] : 1 ∈ Matrix.unitaryGroup H ℂ

theorem QuantumQueryComplexity.mul_mem_qUnitary {H : Type u_1} [Fintype H] [DecidableEq H] {U V : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) (hV : V ∈ Matrix.unitaryGroup H ℂ) : U * V ∈ Matrix.unitaryGroup H ℂ

theorem QuantumQueryComplexity.conjTranspose_mul_self_of_unitary {H : Type u_1} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) : U.conjTranspose * U = 1

theorem QuantumQueryComplexity.qInner_mulVec_left {H : Type u_1} [Fintype H] (M : Matrix H H ℂ) (ψ φ : H → ℂ) : qInner (M.mulVec ψ) φ = qInner ψ (M.conjTranspose.mulVec φ)

Moving an operator across the inner product.

theorem QuantumQueryComplexity.qInner_mulVec_mulVec {H : Type u_1} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) (ψ φ : H → ℂ) : qInner (U.mulVec ψ) (U.mulVec φ) = qInner ψ φ

A unitary preserves the inner product.

theorem QuantumQueryComplexity.qNormSq_mulVec {H : Type u_1} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) (ψ : H → ℂ) : qNormSq (U.mulVec ψ) = qNormSq ψ

A unitary preserves the squared norm.

theorem QuantumQueryComplexity.IsQState.mulVec {H : Type u_1} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) {ψ : H → ℂ} (hψ : IsQState ψ) : IsQState (U.mulVec ψ)

A unitary maps states to states.

Permutation unitaries

Every oracle in this development is a permutation of the computational basis, so this is the workhorse. Note the inverse in the definition: Mathlib's Equiv.Perm.permMatrix σ acts on coordinates by v ∘ σ, i.e. it sends the basis state |b⟩ to |σ⁻¹ b⟩; qPerm e is normalized so that it sends |b⟩ to |e b⟩.

def QuantumQueryComplexity.qPerm {H : Type u_1} [DecidableEq H] (e : Equiv.Perm H) : Matrix H H ℂ

The unitary that sends the basis state |b⟩ to |e b⟩.

Equations

• QuantumQueryComplexity.qPerm e = Equiv.Perm.permMatrix ℂ e⁻¹

theorem QuantumQueryComplexity.qPerm_mulVec {H : Type u_1} [Fintype H] [DecidableEq H] (e : Equiv.Perm H) (ψ : H → ℂ) : (qPerm e).mulVec ψ = ψ ∘ ⇑e⁻¹

theorem QuantumQueryComplexity.qPerm_mulVec_apply {H : Type u_1} [Fintype H] [DecidableEq H] (e : Equiv.Perm H) (ψ : H → ℂ) (h : H) : (qPerm e).mulVec ψ h = ψ ((Equiv.symm e) h)

theorem QuantumQueryComplexity.qPerm_mulVec_qBasis {H : Type u_1} [Fintype H] [DecidableEq H] (e : Equiv.Perm H) (p : H) : (qPerm e).mulVec (qBasis p) = qBasis (e p)

A permutation unitary sends basis states to basis states.

@[simp]

theorem QuantumQueryComplexity.qPerm_one {H : Type u_1} [DecidableEq H] : qPerm 1 = 1

theorem QuantumQueryComplexity.qPerm_mul {H : Type u_1} [Fintype H] [DecidableEq H] (e f : Equiv.Perm H) : qPerm (e * f) = qPerm e * qPerm f

theorem QuantumQueryComplexity.qPerm_mem_unitaryGroup {H : Type u_1} [Fintype H] [DecidableEq H] (e : Equiv.Perm H) : qPerm e ∈ Matrix.unitaryGroup H ℂ

theorem QuantumQueryComplexity.qPerm_mul_self_of_involutive {H : Type u_1} [Fintype H] [DecidableEq H] {e : Equiv.Perm H} (he : Function.Involutive ⇑e) : qPerm e * qPerm e = 1

An involutive permutation gives a self-inverse unitary: query = unquery.

Projectors and reflections

def QuantumQueryComplexity.IsQProjector {H : Type u_1} [Fintype H] (P : Matrix H H ℂ) : Prop

An orthogonal projector.

Equations

• QuantumQueryComplexity.IsQProjector P = (P.conjTranspose = P ∧ P * P = P)

def QuantumQueryComplexity.qRefl {H : Type u_1} [DecidableEq H] (P : Matrix H H ℂ) : Matrix H H ℂ

The reflection about the range of a projector, 2P - 1.

Equations

• QuantumQueryComplexity.qRefl P = 2 • P - 1

theorem QuantumQueryComplexity.qRefl_conjTranspose {H : Type u_1} [Fintype H] [DecidableEq H] {P : Matrix H H ℂ} (hP : IsQProjector P) : (qRefl P).conjTranspose = qRefl P

theorem QuantumQueryComplexity.qRefl_mul_self {H : Type u_1} [Fintype H] [DecidableEq H] {P : Matrix H H ℂ} (hP : IsQProjector P) : qRefl P * qRefl P = 1

A reflection is involutive.

theorem QuantumQueryComplexity.IsQProjector.qNormSq_mulVec_le {H : Type u_1} [Fintype H] {P : Matrix H H ℂ} (hP : IsQProjector P) (ψ : H → ℂ) : qNormSq (P.mulVec ψ) ≤ qNormSq ψ

A projector shrinks: ‖Pψ‖ ≤ ‖ψ‖.

theorem QuantumQueryComplexity.IsQProjector.conj {H : Type u_1} [Fintype H] [DecidableEq H] {P U : Matrix H H ℂ} (hP : IsQProjector P) (hU : U ∈ Matrix.unitaryGroup H ℂ) : IsQProjector (U * P * U.conjTranspose)

Conjugating a projector by a unitary gives a projector.

theorem QuantumQueryComplexity.qRefl_mem_unitaryGroup {H : Type u_1} [Fintype H] [DecidableEq H] {P : Matrix H H ℂ} (hP : IsQProjector P) : qRefl P ∈ Matrix.unitaryGroup H ℂ

A reflection is unitary.

The two counting bounds of the independent-run analysis

Pure finite probability, stated over an arbitrary weight; no quantum imports.

• sum_filter_ne_le_sum_coord — the union bound over coordinates: any weight of the patterns different from a target is at most the sum over coordinates of the weight of the patterns wrong at that coordinate. (A standalone utility, currently unused: the tuple join ended up using Weierstrass on the diagonal instead, and plurality amplification (SourceQuantumPlurality) uses the sharper exponential-moment argument sum_prod_tail_le rather than a union bound.)
• sum_prod_majority_le — the majority tail: if each coordinate's wrong value carries probability at most ε ≤ 1, the product weight of the patterns with at least t wrong coordinates is at most 2^k·εᵗ. With per-run error 1/16 and t = ⌈k/2⌉ this is ≤ 2^{-k} — no Chernoff bound and no independence formalism: the product structure is supplied exactly by the bank-swap compiler, and the tail is one count over patterns.
• sum_prod_tail_le — the exponential-moment tail (moved here from SourceQuantumPlurality, so that circuit utilities can use it without the lower-bound development): the weight of the records with at least t wrong coordinates is at most (1 + ε)^k / 2^t. Unlike the majority tail it decays at base error 1/3: (4/3)^k / 2^{k/2} = (8/9)^{k/2}.

theorem QuantumQueryComplexity.sum_filter_ne_le_sum_coord {k : ℕ} (w : (Fin k → Bool) → ℝ) (hw : ∀ (y : Fin k → Bool), 0 ≤ w y) (b : Fin k → Bool) : ∑ y : Fin k → Bool with y ≠ b, w y ≤ ∑ j : Fin k, ∑ y : Fin k → Bool with y j ≠ b j, w y

The union bound over coordinates: every pattern different from b is wrong somewhere, so its weight is charged to some coordinate.

theorem QuantumQueryComplexity.sum_prod_majority_le {k t : ℕ} {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (p : Fin k → Bool → ℝ) (b : Fin k → Bool) (hp0 : ∀ (j : Fin k) (y : Bool), 0 ≤ p j y) (hp1 : ∀ (j : Fin k) (y : Bool), p j y ≤ 1) (hpe : ∀ (j : Fin k), (p j !b j) ≤ ε) : ∑ y : Fin k → Bool with t ≤ {j : Fin k | y j ≠ b j}.card, ∏ j : Fin k, p j (y j) ≤ 2 ^ k * ε ^ t

The majority tail: patterns with at least t wrong coordinates carry product weight at most 2^k·εᵗ.

The exponential-moment tail

def QuantumQueryComplexity.wrongCount {O : Type} [DecidableEq O] {k : ℕ} (y b : Fin k → O) : ℕ

The number of coordinates at which the record y differs from b.

Equations

• QuantumQueryComplexity.wrongCount y b = {j : Fin k | y j ≠ b j}.card

theorem QuantumQueryComplexity.prod_ite_eq_two_pow_wrongCount {O : Type} [DecidableEq O] {k : ℕ} (y b : Fin k → O) : (∏ j : Fin k, if y j ≠ b j then 2 else 1) = 2 ^ wrongCount y b

theorem QuantumQueryComplexity.sum_prod_tail_le {O : Type} [Fintype O] [DecidableEq O] {k t : ℕ} {ε : ℝ} (p : Fin k → O → ℝ) (b : Fin k → O) (hp0 : ∀ (j : Fin k) (o : O), 0 ≤ p j o) (hp1 : ∀ (j : Fin k), ∑ o : O, p j o ≤ 1) (hpe : ∀ (j : Fin k), ∑ o : O with o ≠ b j, p j o ≤ ε) : (∑ y : Fin k → O with t ≤ wrongCount y b, ∏ j : Fin k, p j (y j)) * 2 ^ t ≤ (1 + ε) ^ k

The exponential-moment tail. If each coordinate's wrong values carry probability at most ε, the product weight of the records with at least t wrong coordinates, times 2^t, is at most (1 + ε)^k: the weight of 2^{wrong} factorizes coordinatewise as ∏ (1 + Pr[wrong]) ≤ (1 + ε)^k, and 2^t ≤ 2^{wrong} on the tail.

Fidelity bounds for a unitary, against a fixed vector and against a far pair

The two generic Hilbert-space estimates behind the state-conversion measurement. The quantity a Hadamard test reads out is Re⟪ψ, Uψ⟫, and the detector U of SourceQuantumInputDetector is designed to make it large on one kind of input and small on the other. This section proves the two sides in the abstract, for an arbitrary unitary U on an arbitrary finite space:

• the positive side (le_mul_re_qInner_mulVec_of_fixed): if U fixes φ, then Re⟪ψ, Uψ⟫ ≥ 2|⟪φ,ψ⟫|²/‖φ‖² − ‖ψ‖² — stated multiplied out by ‖φ‖⁴, so φ = 0 needs no special case and no division appears;
• the negative side (re_qInner_mulVec_le_of_perp): if ψ = ψN + ψF orthogonally and ‖UψF + ψF‖ is small — U is close to −1 on the far part — then Re⟪ψ, Uψ⟫ ≤ ‖ψ‖‖ψN‖ + ‖ψ‖‖UψF + ψF‖ − ‖ψF‖².

No spectral decomposition of U occurs. The positive bound is one Cauchy–Schwarz application to the auxiliary vector χ = ‖φ‖²ψ − ⟪φ,ψ⟫φ, the component of ‖φ‖²ψ orthogonal to φ: since U and Uᴴ both fix φ, the plane spanned by φ and the pair χ, Uχ splits the form ⟪ψ, Uψ⟫ exactly, and Cauchy–Schwarz on the χ-part is the only estimate. The negative bound is Cauchy–Schwarz three times, with the orthogonality supplying the exact −‖ψF‖² term.

Also here: qInner_mulVec_one_sub_mulVec, the orthogonality of a projector's range and its complement's range on the same vector — the form in which the chord windows enter the negative side downstream.

theorem QuantumQueryComplexity.conjTranspose_mulVec_of_fixed {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) {φ : H → ℂ} (hφ : U.mulVec φ = φ) : U.conjTranspose.mulVec φ = φ

A unitary that fixes a vector: so does its adjoint.

theorem QuantumQueryComplexity.le_mul_re_qInner_mulVec_of_fixed {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) {φ : H → ℂ} (hφ : U.mulVec φ = φ) (ψ : H → ℂ) : 2 * Complex.normSq (qInner φ ψ) * qNormSq φ - qNormSq φ ^ 2 * qNormSq ψ ≤ qNormSq φ ^ 2 * (qInner ψ (U.mulVec ψ)).re

The fidelity lower bound. A unitary that fixes φ satisfies, on every ψ, Re⟪ψ, Uψ⟫ ≥ 2|⟪φ,ψ⟫|²/‖φ‖² − ‖ψ‖² — multiplied out by ‖φ‖⁴, so no positivity of ‖φ‖ is assumed and no division appears.

theorem QuantumQueryComplexity.re_qInner_mulVec_le_of_perp {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) {ψN ψF : H → ℂ} (horth : qInner ψN ψF = 0) : (qInner (ψN + ψF) (U.mulVec (ψN + ψF))).re ≤ √(qNormSq (ψN + ψF)) * √(qNormSq ψN) + √(qNormSq (ψN + ψF)) * √(qNormSq (U.mulVec ψF + ψF)) - qNormSq ψF

The fidelity upper bound. If ψ splits orthogonally into a near part ψN and a far part ψF on which the unitary is close to −1, then Re⟪ψ, Uψ⟫ ≤ ‖ψ‖‖ψN‖ + ‖ψ‖‖UψF + ψF‖ − ‖ψF‖².

theorem QuantumQueryComplexity.qInner_mulVec_one_sub_mulVec {H : Type} [Fintype H] [DecidableEq H] {P : Matrix H H ℂ} (hP : IsQProjector P) (x : H → ℂ) : qInner (P.mulVec x) ((1 - P).mulVec x) = 0

A projector's range is orthogonal to its complement's range, on the same vector. The form in which the chord-window decomposition enters the fidelity bound.

Computational-basis measurement

A measurement of the final state of a query algorithm is a projective measurement in the computational basis, coarse-grained by a readout map p : H → O that says which output each basis state announces. So the only definition needed is

qProb p ψ o = ∑ h with p h = o, ‖ψ h‖²,

the probability of announcing o. Deferring all measurements to the end is without loss of generality in the query model, and general POVMs are not needed for the characterization (see the plan, §"Design Decisions").

The companion definition qRestrict p o ψ is the unnormalized post-measurement state; it is what turns statements about probabilities into statements about inner products, which is how the adversary lower bound consumes the output condition (∑ o, qRestrict p o ψ = ψ, and distinct outcomes are orthogonal).

def QuantumQueryComplexity.qRestrict {H : Type u_1} {O : Type u_2} [DecidableEq O] (p : H → O) (o : O) (ψ : H → ℂ) : H → ℂ

The unnormalized part of ψ that announces the outcome o.

Equations

• QuantumQueryComplexity.qRestrict p o ψ h = if p h = o then ψ h else 0

def QuantumQueryComplexity.qProb {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) (ψ : H → ℂ) (o : O) : ℝ

The probability that measuring ψ announces the outcome o.

Equations

• QuantumQueryComplexity.qProb p ψ o = ∑ h : H, if p h = o then Complex.normSq (ψ h) else 0

theorem QuantumQueryComplexity.qProb_eq_qNormSq_qRestrict {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) (ψ : H → ℂ) (o : O) : qProb p ψ o = qNormSq (qRestrict p o ψ)

theorem QuantumQueryComplexity.qProb_nonneg {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) (ψ : H → ℂ) (o : O) : 0 ≤ qProb p ψ o

@[simp]

theorem QuantumQueryComplexity.qProb_qBasis {H : Type u_1} [Fintype H] [DecidableEq H] {O : Type u_2} [DecidableEq O] (p : H → O) (h : H) (o : O) : qProb p (qBasis h) o = if p h = o then 1 else 0

Measuring a basis state announces its readout with certainty.

The distance-to-success bridge

None of this needs [Fintype O] — the sums range over H alone — and the cardinality-free extraction depends on exactly that: the bridge from a conversion-distance bound to a success probability must not reintroduce an output-cardinality assumption.

theorem QuantumQueryComplexity.qNormSq_sub_qRestrict {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) (o : O) (ψ : H → ℂ) : qNormSq (ψ - qRestrict p o ψ) = qNormSq ψ - qProb p ψ o

The part of ψ that does not announce o.

theorem QuantumQueryComplexity.qNormSq_sub_qRestrict_le {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) (o : O) (ψ : H → ℂ) {φ : H → ℂ} (hφ : qRestrict p o φ = φ) : qNormSq (ψ - qRestrict p o ψ) ≤ qNormSq (ψ - φ)

Restriction is the best sector approximation: against any φ supported on the o-sector, the unannounced mass of ψ is dominated.

theorem QuantumQueryComplexity.le_qProb_of_qNormSq_sub_le {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) (o : O) {ψ φ : H → ℂ} (hφ : qRestrict p o φ = φ) {δ : ℝ} (h : qNormSq (ψ - φ) ≤ δ) : qNormSq ψ - δ ≤ qProb p ψ o

The distance-to-success bridge, output-cardinality-free: a state within squared distance δ of one supported on the o-sector announces o with probability at least qNormSq ψ − δ.

The outcomes partition the norm

theorem QuantumQueryComplexity.sum_qProb {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] [Fintype O] (p : H → O) (ψ : H → ℂ) : ∑ o : O, qProb p ψ o = qNormSq ψ

theorem QuantumQueryComplexity.sum_qProb_eq_one {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] [Fintype O] {ψ : H → ℂ} (hψ : IsQState ψ) (p : H → O) : ∑ o : O, qProb p ψ o = 1

On a state the outcome probabilities sum to one.

theorem QuantumQueryComplexity.qProb_le_qNormSq {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) (ψ : H → ℂ) (o : O) : qProb p ψ o ≤ qNormSq ψ

theorem QuantumQueryComplexity.qProb_le_one {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] {ψ : H → ℂ} (hψ : IsQState ψ) (p : H → O) (o : O) : qProb p ψ o ≤ 1

theorem QuantumQueryComplexity.qProb_add_qProb_le_qNormSq {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) (ψ : H → ℂ) {a b : O} (hab : a ≠ b) : qProb p ψ a + qProb p ψ b ≤ qNormSq ψ

Two distinct outcomes cannot both be likely. This is what forbids a single state from answering two different questions, and hence what makes the query model unable to compute an unobservable distinction.

theorem QuantumQueryComplexity.qProb_add_qProb_le_one {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] {ψ : H → ℂ} (hψ : IsQState ψ) (p : H → O) {a b : O} (hab : a ≠ b) : qProb p ψ a + qProb p ψ b ≤ 1

theorem QuantumQueryComplexity.sum_qProb_ne {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] [Fintype O] {ψ : H → ℂ} (hψ : IsQState ψ) (p : H → O) (o : O) : ∑ o' ∈ Finset.univ.erase o, qProb p ψ o' = 1 - qProb p ψ o

The probability of announcing anything other than o is 1 - qProb p ψ o.

The post-measurement decomposition

theorem QuantumQueryComplexity.sum_qRestrict {H : Type u_1} {O : Type u_2} [DecidableEq O] [Fintype O] (p : H → O) (ψ : H → ℂ) : ∑ o : O, qRestrict p o ψ = ψ

theorem QuantumQueryComplexity.qInner_eq_sum_qRestrict {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] [Fintype O] (p : H → O) (ψ φ : H → ℂ) : qInner ψ φ = ∑ o : O, qInner (qRestrict p o ψ) (qRestrict p o φ)

The inner product decomposes over the outcomes. This is the form the adversary lower bound uses, with the readout map taken to be the query-index register: it splits a state into the sectors the oracle acts on independently.

theorem QuantumQueryComplexity.qInner_qRestrict_of_ne {H : Type u_1} [Fintype H] {O : Type u_2} [DecidableEq O] (p : H → O) {a b : O} (hab : a ≠ b) (ψ φ : H → ℂ) : qInner (qRestrict p a ψ) (qRestrict p b φ) = 0

Distinct outcomes are orthogonal.

The value oracle

The basis of a query algorithm is

QBasis ι σ W = Option ι × Option σ × W

— a query-index register (none = idle, no query is made), an answer register (none = blank), and a workspace. On input a : ι → σ the oracle acts as the identity on the idle sector and, on the index some i, swaps the blank answer with the answer some (a i):

|i⟩|⊥⟩|w⟩ ↦ |i⟩|a i⟩|w⟩, |i⟩|a i⟩|w⟩ ↦ |i⟩|⊥⟩|w⟩,

leaving |i⟩|s⟩|w⟩ alone for every other answer s.

Why this oracle rather than |i⟩|s⟩ ↦ |i⟩|s ⊕ a i⟩:

• it is defined for any finite alphabet, with no group structure on σ;
• it is a permutation of the basis, hence unitary for free, and an involution, so query and unquery are literally the same matrix;
• the idle index gives controlled queries at no extra cost, which is what the phase-detection circuit of the upper bound will need;
• on a blank answer register it returns the value coherently, which is all the lower bound's query decomposition uses.

It is equivalent to the Boolean XOR oracle at two queries per query, in both directions: SourceQuantumXorOracle defines that oracle (with explicit idle-index and blank-answer sectors) and SourceQuantumSimulation proves the equivalence.

The two lemmas that carry the whole development are oracleMap_none and oracleMap_some: the oracle's action at a basis state with index some i depends on the input only through a i. That is the source of the adversary lower bound's query decomposition.

@[reducible, inline]

abbrev QuantumQueryComplexity.QBasis (ι : Type u_1) (σ : Type u_2) (W : Type u_3) : Type (max (max u_3 u_2) u_1)

The basis of a query algorithm: query index (none = idle), answer register (none = blank), and workspace.

Equations

• QuantumQueryComplexity.QBasis ι σ W = (Option ι × Option σ × W)

@[instance_reducible]

instance QuantumQueryComplexity.instQBasisDecidableEq {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] : DecidableEq (QBasis ι σ W)

Equations

• QuantumQueryComplexity.instQBasisDecidableEq a b = instDecidableEqProd a b

@[instance_reducible]

instance QuantumQueryComplexity.instQBasisFintype {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [Fintype ι] [Fintype σ] [Fintype W] : Fintype (QBasis ι σ W)

Equations

• QuantumQueryComplexity.instQBasisFintype = { elems := Finset.univ ×ˢ Finset.univ, complete := ⋯ }

def QuantumQueryComplexity.oracleMap {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) : QBasis ι σ W → QBasis ι σ W

The oracle's action on the computational basis.

Equations

• QuantumQueryComplexity.oracleMap a (none, t, w) = (none, t, w)
• QuantumQueryComplexity.oracleMap a (some i, t, w) = (some i, (Equiv.swap none (some (a i))) t, w)

@[simp]

theorem QuantumQueryComplexity.oracleMap_none {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) (t : Option σ) (w : W) : oracleMap a (none, t, w) = (none, t, w)

@[simp]

theorem QuantumQueryComplexity.oracleMap_some {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) (i : ι) (t : Option σ) (w : W) : oracleMap a (some i, t, w) = (some i, (Equiv.swap none (some (a i))) t, w)

The oracle reads the input only at the queried index.

theorem QuantumQueryComplexity.oracleMap_fst {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) (p : QBasis ι σ W) : (oracleMap a p).1 = p.1

The oracle never moves the index register.

theorem QuantumQueryComplexity.oracleMap_snd_of_fst_none {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] {a : ι → σ} {p : QBasis ι σ W} (h : p.1 = none) : (oracleMap a p).2.1 = p.2.1

theorem QuantumQueryComplexity.oracleMap_snd_of_fst_some {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] {a : ι → σ} {p : QBasis ι σ W} {i : ι} (h : p.1 = some i) : (oracleMap a p).2.1 = (Equiv.swap none (some (a i))) p.2.1

theorem QuantumQueryComplexity.oracleMap_blank {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) (i : ι) (w : W) : oracleMap a (some i, none, w) = (some i, some (a i), w)

theorem QuantumQueryComplexity.oracleMap_involutive {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) : Function.Involutive (oracleMap a)

def QuantumQueryComplexity.oraclePerm {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) : Equiv.Perm (QBasis ι σ W)

The oracle as a permutation of the basis.

Equations

• QuantumQueryComplexity.oraclePerm a = Function.Involutive.toPerm (QuantumQueryComplexity.oracleMap a) ⋯

@[simp]

theorem QuantumQueryComplexity.oraclePerm_apply {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) (p : QBasis ι σ W) : (oraclePerm a) p = oracleMap a p

theorem QuantumQueryComplexity.oraclePerm_involutive {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq σ] (a : ι → σ) : Function.Involutive ⇑(oraclePerm a)

def QuantumQueryComplexity.oracleMat {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] (a : ι → σ) : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ

The oracle unitary.

Equations

• QuantumQueryComplexity.oracleMat a = QuantumQueryComplexity.qPerm (QuantumQueryComplexity.oraclePerm a)

theorem QuantumQueryComplexity.oracleMat_mem_unitaryGroup {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) : oracleMat a ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ

theorem QuantumQueryComplexity.oracleMat_mul_self {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) : oracleMat a * oracleMat a = 1

Query = unquery.

theorem QuantumQueryComplexity.oracleMat_mulVec_apply {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (ψ : QBasis ι σ W → ℂ) (p : QBasis ι σ W) : (oracleMat a).mulVec ψ p = ψ (oracleMap a p)

@[simp]

theorem QuantumQueryComplexity.oracleMat_mulVec_apply_none {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (ψ : QBasis ι σ W → ℂ) (t : Option σ) (w : W) : (oracleMat a).mulVec ψ (none, t, w) = ψ (none, t, w)

On the idle sector the oracle does nothing: this is what makes a query controlled.

@[simp]

theorem QuantumQueryComplexity.oracleMat_mulVec_apply_some {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (ψ : QBasis ι σ W → ℂ) (i : ι) (t : Option σ) (w : W) : (oracleMat a).mulVec ψ (some i, t, w) = ψ (some i, (Equiv.swap none (some (a i))) t, w)

The query decomposition. At a basis state with query index some i the queried state depends on the input only through a i.

theorem QuantumQueryComplexity.oracleMat_mulVec_congr {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {a b : ι → σ} (ψ : QBasis ι σ W → ℂ) {p : QBasis ι σ W} (hp : ∀ (i : ι), p.1 = some i → a i = b i) : (oracleMat a).mulVec ψ p = (oracleMat b).mulVec ψ p

Two inputs that agree at the index i give the same amplitude at every basis state querying i; two inputs always agree on the idle sector.

theorem QuantumQueryComplexity.oracleMat_mulVec_qBasis {ι : Type u_1} {σ : Type u_2} {W : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (p : QBasis ι σ W) : (oracleMat a).mulVec (qBasis p) = qBasis (oracleMap a p)

Quantum query algorithms

A quantum query algorithm is an initial unit state on QBasis ι σ Work, a sequence of input-independent unitaries, and a readout map for the final computational-basis measurement. On input a : ι → σ it evolves as

ψ₀ = U₀ |init⟩, ψ_{t+1} = U_{t+1} O_a ψ_t,

so A.state a t is the state after t queries; A.prob a t o is the probability that measuring it announces o. This is the standard deferred-measurement form of the model.

Design notes

• The unitaries are indexed by all of ℕ. An algorithm is not tied to a query count: the query count is the time t at which one reads off the answer. This removes every Fin (q+1) cast from the development, and makes "the same algorithm run longer" a statement about t, not a new structure.
• The workspace W is a parameter, not a field. Bundling it inside the structure makes A.Work appear in the index type of every matrix, and then rw and instance search fail on goals that are true by rfl (the type QBasis ι σ A.Work is only definitionally the concrete workspace a construction used). Quantifying over W is deferred to QueryCounts in SourceQuantumComplexity, which is the one place it costs anything. Everything lives in Type (universe 0): every index type, alphabet and workspace in this project is concrete.
• Correctness is stated promise-natively, through read : X → ι → σ. The total case is X = (ι → σ) with read = id.

Main results

• QAlg.state_isQState — the algorithm's state is a unit vector at all times.
• computesWithErrorOn_const — a constant function needs no queries.
• computesWithErrorOn_proj — one query reads one coordinate exactly.

structure QuantumQueryComplexity.QAlg (ι σ O W : Type) [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : Type

A quantum query algorithm with output type O and workspace W.

• init : QBasis ι σ W → ℂ

  The initial state.

• init_isQState : IsQState self.init

  The initial state is a unit vector.

• step : ℕ → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ

  The input-independent unitaries; step t is applied after the t-th query (and step 0 before the first).

• step_unitary (t : ℕ) : self.step t ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ

  Each step is unitary.

• readout : QBasis ι σ W → O

  The final measurement's readout map.

def QuantumQueryComplexity.QAlg.state {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (a : ι → σ) : ℕ → QBasis ι σ W → ℂ

The state of A on input a after t queries.

Equations

• A.state a 0 = (A.step 0).mulVec A.init
• A.state a t.succ = (A.step (t + 1)).mulVec ((QuantumQueryComplexity.oracleMat a).mulVec (A.state a t))

@[simp]

theorem QuantumQueryComplexity.QAlg.state_zero {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (a : ι → σ) : A.state a 0 = (A.step 0).mulVec A.init

@[simp]

theorem QuantumQueryComplexity.QAlg.state_succ {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (a : ι → σ) (t : ℕ) : A.state a (t + 1) = (A.step (t + 1)).mulVec ((oracleMat a).mulVec (A.state a t))

theorem QuantumQueryComplexity.QAlg.state_isQState {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (a : ι → σ) (t : ℕ) : IsQState (A.state a t)

The state stays a unit vector.

def QuantumQueryComplexity.QAlg.prob {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] [DecidableEq O] (A : QAlg ι σ O W) (a : ι → σ) (t : ℕ) (o : O) : ℝ

The probability that A, run for t queries on input a, announces o.

Equations

• A.prob a t o = QuantumQueryComplexity.qProb A.readout (A.state a t) o

theorem QuantumQueryComplexity.QAlg.prob_nonneg {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] [DecidableEq O] (A : QAlg ι σ O W) (a : ι → σ) (t : ℕ) (o : O) : 0 ≤ A.prob a t o

theorem QuantumQueryComplexity.QAlg.prob_le_one {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] [DecidableEq O] (A : QAlg ι σ O W) (a : ι → σ) (t : ℕ) (o : O) : A.prob a t o ≤ 1

Bounded-error correctness

def QuantumQueryComplexity.ComputesWithErrorOn {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] {X : Type} [DecidableEq O] (A : QAlg ι σ O W) (q : ℕ) (read : X → ι → σ) (f : X → O) (ε : ℝ) : Prop

A computes f on the promise read with error at most ε in q queries.

Equations

• QuantumQueryComplexity.ComputesWithErrorOn A q read f ε = ∀ (x : X), 1 - ε ≤ A.prob (read x) q (f x)

theorem QuantumQueryComplexity.ComputesWithErrorOn.mono {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] {X : Type} [DecidableEq O] {A : QAlg ι σ O W} {q : ℕ} {read : X → ι → σ} {f : X → O} {ε ε' : ℝ} (h : ComputesWithErrorOn A q read f ε) (hε : ε ≤ ε') : ComputesWithErrorOn A q read f ε'

Two sanity constructions

These are the smallest end-to-end uses of the model: they exercise the oracle's action on a basis state and the measurement rule, and they are the base cases of every later construction.

def QuantumQueryComplexity.constAlg {O : Type} (ι σ : Type) [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] (c : O) : QAlg ι σ O Unit

The zero-query algorithm that always announces c.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumQueryComplexity.computesWithErrorOn_const {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} [DecidableEq O] (read : X → ι → σ) (c : O) {f : X → O} (hf : ∀ (x : X), f x = c) {ε : ℝ} (hε : 0 ≤ ε) : ComputesWithErrorOn (constAlg ι σ c) 0 read f ε

A constant function needs no queries.

def QuantumQueryComplexity.projAlg (σ : Type) [Fintype σ] [DecidableEq σ] {ι : Type} [Fintype ι] [DecidableEq ι] (i : ι) : QAlg ι σ (Option σ) Unit

The one-query algorithm that queries the coordinate i and announces the answer register.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumQueryComplexity.computesWithErrorOn_proj {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} (read : X → ι → σ) (i : ι) {ε : ℝ} (hε : 0 ≤ ε) : ComputesWithErrorOn (projAlg σ i) 1 read (fun (x : X) => some (read x i)) ε

One query reads one coordinate, exactly.

Workspace extension and register-indexed families

Extending a workspace by a register V and acting block-diagonally on it is the single primitive behind two things the circuit layer needs: lifting an operator to a larger workspace (a constant family) and controlling it on a register value (a family that is the identity elsewhere).

blockFam fam applies fam v on the sector where the extra register holds v.

It is defined as Mathlib's Matrix.blockDiagonal read through the reindexing regEquiv : QBasis ι σ (V × W) ≃ QBasis ι σ W × V, so the algebra — multiplicativity, unit, adjoint — is inherited rather than re-proved.

Acceptance contracts

• blockFam_mul, blockFam_one, blockFam_conjTranspose, blockFam_mem_unitaryGroup — it is a monoid map into the unitaries.
• blockFam_mulVec_embed — its action on the encoded subspace embedReg v ψ, the sector where the register holds v. This is the only form in which blockFam gets used: statements about a controlled operator are statements about encoded states, never global matrix identities.
• blockFam_oracle — the oracle ignores the workspace, so on an extended workspace it is a constant block family. This is what lets a query pass through a workspace extension unchanged.

theorem QuantumQueryComplexity.matrix_ext_of_mulVec_qBasis {H : Type} [Fintype H] [DecidableEq H] {M N : Matrix H H ℂ} (h : ∀ (r : H), M.mulVec (qBasis r) = N.mulVec (qBasis r)) : M = N

Two matrices agreeing on every basis vector are equal.

def QuantumQueryComplexity.regEquiv {ι σ V W : Type} : QBasis ι σ (V × W) ≃ QBasis ι σ W × V

The extended basis, split as (rest, extra register).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumQueryComplexity.regEquiv_apply {ι σ V W : Type} (p : QBasis ι σ (V × W)) : regEquiv p = ((p.1, p.2.1, p.2.2.2), p.2.2.1)

@[simp]

theorem QuantumQueryComplexity.regEquiv_symm_apply {ι σ V W : Type} (x : QBasis ι σ W × V) : regEquiv.symm x = (x.1.1, x.1.2.1, x.2, x.1.2.2)

def QuantumQueryComplexity.blockFam {ι σ V W : Type} [DecidableEq V] (fam : V → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) : Matrix (QBasis ι σ (V × W)) (QBasis ι σ (V × W)) ℂ

A register-indexed family of operators, acting block-diagonally on the extra register.

Equations

• QuantumQueryComplexity.blockFam fam = (Matrix.blockDiagonal fam).submatrix ⇑QuantumQueryComplexity.regEquiv ⇑QuantumQueryComplexity.regEquiv

def QuantumQueryComplexity.liftReg {ι σ W : Type} (V : Type) [DecidableEq V] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) : Matrix (QBasis ι σ (V × W)) (QBasis ι σ (V × W)) ℂ

Lift an operator to an extended workspace: the constant family.

Equations

• QuantumQueryComplexity.liftReg V U = QuantumQueryComplexity.blockFam fun (x : V) => U

The algebra

theorem QuantumQueryComplexity.blockFam_mul {ι σ V W : Type} [Fintype ι] [Fintype σ] [Fintype V] [DecidableEq V] [Fintype W] (f g : V → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) : blockFam f * blockFam g = blockFam fun (v : V) => f v * g v

theorem QuantumQueryComplexity.blockFam_one {ι σ V W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq V] [DecidableEq W] : (blockFam fun (x : V) => 1) = 1

theorem QuantumQueryComplexity.blockFam_conjTranspose {ι σ V W : Type} [DecidableEq V] (f : V → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) : (blockFam f).conjTranspose = blockFam fun (v : V) => (f v).conjTranspose

theorem QuantumQueryComplexity.blockFam_mem_unitaryGroup {ι σ V W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] {f : V → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} (hf : ∀ (v : V), f v ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) : blockFam f ∈ Matrix.unitaryGroup (QBasis ι σ (V × W)) ℂ

theorem QuantumQueryComplexity.liftReg_mem_unitaryGroup {ι σ V W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] {U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) : liftReg V U ∈ Matrix.unitaryGroup (QBasis ι σ (V × W)) ℂ

The encoded subspace

def QuantumQueryComplexity.embedReg {ι σ V W : Type} [DecidableEq V] (v : V) (ψ : QBasis ι σ W → ℂ) : QBasis ι σ (V × W) → ℂ

The encoded subspace: ψ, placed in the sector where the extra register holds v.

Equations

• QuantumQueryComplexity.embedReg v ψ p = if p.2.2.1 = v then ψ (p.1, p.2.1, p.2.2.2) else 0

theorem QuantumQueryComplexity.embedReg_apply {ι σ V W : Type} [DecidableEq V] (v : V) (ψ : QBasis ι σ W → ℂ) (p : QBasis ι σ (V × W)) : embedReg v ψ p = if p.2.2.1 = v then ψ (p.1, p.2.1, p.2.2.2) else 0

theorem QuantumQueryComplexity.blockFam_mulVec_embed {ι σ V W : Type} [Fintype ι] [Fintype σ] [Fintype V] [DecidableEq V] [Fintype W] (fam : V → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (v : V) (ψ : QBasis ι σ W → ℂ) : (blockFam fam).mulVec (embedReg v ψ) = embedReg v ((fam v).mulVec ψ)

The action on the encoded subspace.

theorem QuantumQueryComplexity.liftReg_mul {ι σ V W : Type} [Fintype ι] [Fintype σ] [Fintype V] [DecidableEq V] [Fintype W] (U U' : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) : liftReg V U * liftReg V U' = liftReg V (U * U')

theorem QuantumQueryComplexity.liftReg_mulVec_embed {ι σ V W : Type} [Fintype ι] [Fintype σ] [Fintype V] [DecidableEq V] [Fintype W] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (v : V) (ψ : QBasis ι σ W → ℂ) : (liftReg V U).mulVec (embedReg v ψ) = embedReg v (U.mulVec ψ)

theorem QuantumQueryComplexity.liftReg_conjTranspose {ι σ V W : Type} [DecidableEq V] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) : (liftReg V U).conjTranspose = liftReg V U.conjTranspose

theorem QuantumQueryComplexity.isQProjector_liftReg {ι σ V W : Type} [Fintype ι] [Fintype σ] [Fintype V] [DecidableEq V] [Fintype W] {P : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} (hP : IsQProjector P) : IsQProjector (liftReg V P)

The sectors are orthogonal

The embedding is linear and isometric onto its own sector, and distinct register values give orthogonal sectors. Everything a superposition over the register needs — Pythagoras for a packed family, in particular — comes from these.

theorem QuantumQueryComplexity.sum_reg {ι σ V W : Type} [Fintype ι] [Fintype σ] [Fintype V] [Fintype W] {M : Type u_1} [AddCommMonoid M] (F : QBasis ι σ (V × W) → M) : ∑ r : QBasis ι σ (V × W), F r = ∑ s : QBasis ι σ W, ∑ u : V, F (regEquiv.symm (s, u))

Split a sum over the extended basis as (rest, extra register).

theorem QuantumQueryComplexity.embedReg_regEquiv_symm {ι σ V W : Type} [DecidableEq V] (v : V) (ψ : QBasis ι σ W → ℂ) (s : QBasis ι σ W) (u : V) : embedReg v ψ (regEquiv.symm (s, u)) = if u = v then ψ s else 0

theorem QuantumQueryComplexity.embedReg_smul {ι σ V W : Type} [DecidableEq V] (v : V) (a : ℂ) (ψ : QBasis ι σ W → ℂ) : embedReg v (a • ψ) = a • embedReg v ψ

theorem QuantumQueryComplexity.embedReg_sum {ι σ V W : Type} [DecidableEq V] {α : Type u_1} (v : V) (s : Finset α) (f : α → QBasis ι σ W → ℂ) : embedReg v (∑ i ∈ s, f i) = ∑ i ∈ s, embedReg v (f i)

theorem QuantumQueryComplexity.qInner_embedReg {ι σ V W : Type} [Fintype ι] [Fintype σ] [Fintype V] [DecidableEq V] [Fintype W] (v v' : V) (ψ φ : QBasis ι σ W → ℂ) : qInner (embedReg v ψ) (embedReg v' φ) = if v = v' then qInner ψ φ else 0

Distinct register values give orthogonal sectors, and the embedding preserves the inner product on its own.

theorem QuantumQueryComplexity.qNormSq_embedReg {ι σ V W : Type} [Fintype ι] [Fintype σ] [Fintype V] [DecidableEq V] [Fintype W] (v : V) (ψ : QBasis ι σ W → ℂ) : qNormSq (embedReg v ψ) = qNormSq ψ

Operators on the extra register itself

blockFam acts on the workspace, indexed by the register. Its transpose — acting on the register, trivially on the workspace — is the other primitive a clocked construction needs, and it is Mathlib's Kronecker product with the identity, so again the algebra is inherited rather than re-proved.

def QuantumQueryComplexity.regOp {ι σ V W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] (A : Matrix V V ℂ) : Matrix (QBasis ι σ (V × W)) (QBasis ι σ (V × W)) ℂ

An operator acting on the extra register alone, as the identity elsewhere.

Equations

• QuantumQueryComplexity.regOp A = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 A).submatrix ⇑QuantumQueryComplexity.regEquiv ⇑QuantumQueryComplexity.regEquiv

theorem QuantumQueryComplexity.regOp_mul {ι σ V W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype V] [Fintype W] [DecidableEq W] (A B : Matrix V V ℂ) : regOp A * regOp B = regOp (A * B)

theorem QuantumQueryComplexity.regOp_one {ι σ V W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq V] [DecidableEq W] : regOp 1 = 1

theorem QuantumQueryComplexity.regOp_conjTranspose {ι σ V W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] (A : Matrix V V ℂ) : (regOp A).conjTranspose = regOp A.conjTranspose

theorem QuantumQueryComplexity.isQProjector_regOp {ι σ V W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype V] [Fintype W] [DecidableEq W] {A : Matrix V V ℂ} (hA : IsQProjector A) : IsQProjector (regOp A)

theorem QuantumQueryComplexity.regOp_mulVec_embedReg {ι σ V W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (A : Matrix V V ℂ) (v : V) (ψ : QBasis ι σ W → ℂ) : (regOp A).mulVec (embedReg v ψ) = ∑ v' : V, A v' v • embedReg v' ψ

The action on the encoded subspace: A moves the register, leaving the workspace vector alone.

The oracle passes through a workspace extension

theorem QuantumQueryComplexity.oracleMap_reg_fst {ι σ V W : Type} [DecidableEq σ] (a : ι → σ) (p : QBasis ι σ (V × W)) : (oracleMap a p).2.2.1 = p.2.2.1

The oracle leaves the extra register alone.

theorem QuantumQueryComplexity.oracleMap_reg_drop {ι σ V W : Type} [DecidableEq σ] (a : ι → σ) (p : QBasis ι σ (V × W)) : ((oracleMap a p).1, (oracleMap a p).2.1, (oracleMap a p).2.2.2) = oracleMap a (p.1, p.2.1, p.2.2.2)

The oracle commutes with dropping the extra register.

theorem QuantumQueryComplexity.qBasis_eq_embedReg {ι σ V W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq V] [DecidableEq W] (r : QBasis ι σ (V × W)) : qBasis r = embedReg r.2.2.1 (qBasis (r.1, r.2.1, r.2.2.2))

theorem QuantumQueryComplexity.blockFam_oracle {ι σ V W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq V] [DecidableEq W] (a : ι → σ) [Finite W] [Finite ι] [Finite σ] [Finite V] : oracleMat a = liftReg V (oracleMat a)

The oracle ignores the workspace, so on an extended workspace it is a constant block family.

Bounded-error quantum query complexity

qQueryOn read f ε is the least number of queries with which some algorithm computes f on the promise read with error at most ε, and boundedErrorQQueryOn fixes the conventional ε = 1/3.

Two API shapes matter downstream and they are not symmetric:

• Upper bounds (qQueryOn_le) are unconditional: exhibiting one algorithm bounds the infimum.
• Lower bounds (le_qQueryOn) need the achievable set to be nonempty, because sInf ∅ = 0 in ℕ. The hypothesis is discharged once and for all by an exact algorithm for every observationally determined problem; until that is in place every lower bound carries hne explicitly rather than hiding the gap.

def QuantumQueryComplexity.QueryCounts {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} (read : X → ι → σ) (f : X → O) (ε : ℝ) : Set ℕ

The set of query counts at which f is computable with error ≤ ε. The workspace is existentially quantified here — this is the one place where that costs anything, and it keeps QAlg free of a bundled type field.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumQueryComplexity.qQueryOn {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} (read : X → ι → σ) (f : X → O) (ε : ℝ) : ℕ

Bounded-error quantum query complexity on a promise.

Equations

• QuantumQueryComplexity.qQueryOn read f ε = sInf (QuantumQueryComplexity.QueryCounts read f ε)

@[reducible, inline]

noncomputable abbrev QuantumQueryComplexity.boundedErrorQQueryOn {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} (read : X → ι → σ) (f : X → O) : ℕ

The conventional error convention.

Equations

• QuantumQueryComplexity.boundedErrorQQueryOn read f = QuantumQueryComplexity.qQueryOn read f (1 / 3)

@[reducible, inline]

noncomputable abbrev QuantumQueryComplexity.qQuery {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] (f : (ι → σ) → O) (ε : ℝ) : ℕ

Quantum query complexity of a total function.

Equations

• QuantumQueryComplexity.qQuery f ε = QuantumQueryComplexity.qQueryOn id f ε

@[reducible, inline]

noncomputable abbrev QuantumQueryComplexity.boundedErrorQQuery {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] (f : (ι → σ) → O) : ℕ

The conventional error convention, for a total function.

Equations

• QuantumQueryComplexity.boundedErrorQQuery f = QuantumQueryComplexity.qQuery f (1 / 3)

Upper bounds

Trap: in the existential above the two instance components must be supplied with inferInstance. Writing ⟨W, _, _, A, h⟩ and letting unification solve them from A's type sends isDefEq into a loop (it does not terminate even at 2·10⁶ heartbeats).

theorem QuantumQueryComplexity.mem_queryCounts {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} {read : X → ι → σ} {f : X → O} {ε : ℝ} {q : ℕ} {W : Type} [Fintype W] [DecidableEq W] {A : QAlg ι σ O W} (h : ComputesWithErrorOn A q read f ε) : q ∈ QueryCounts read f ε

theorem QuantumQueryComplexity.qQueryOn_le {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} {read : X → ι → σ} {f : X → O} {ε : ℝ} {q : ℕ} {W : Type} [Fintype W] [DecidableEq W] {A : QAlg ι σ O W} (h : ComputesWithErrorOn A q read f ε) : qQueryOn read f ε ≤ q

One algorithm bounds the complexity.

Lower bounds and the optimal witness

theorem QuantumQueryComplexity.exists_computes_qQueryOn {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} {read : X → ι → σ} {f : X → O} {ε : ℝ} (hne : (QueryCounts read f ε).Nonempty) : ∃ (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (A : QAlg ι σ O W), ComputesWithErrorOn A (qQueryOn read f ε) read f ε

The infimum is attained: an optimal algorithm exists as soon as any algorithm does.

theorem QuantumQueryComplexity.le_qQueryOn {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} {read : X → ι → σ} {f : X → O} {ε : ℝ} {c : ℕ} (hne : (QueryCounts read f ε).Nonempty) (h : ∀ (q : ℕ) (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (A : QAlg ι σ O W), ComputesWithErrorOn A q read f ε → c ≤ q) : c ≤ qQueryOn read f ε

A bound valid for every algorithm bounds the complexity from below.

theorem QuantumQueryComplexity.le_qQueryOn_real {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} {read : X → ι → σ} {f : X → O} {ε c : ℝ} (hne : (QueryCounts read f ε).Nonempty) (h : ∀ (q : ℕ) (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (A : QAlg ι σ O W), ComputesWithErrorOn A q read f ε → c ≤ ↑q) : c ≤ ↑(qQueryOn read f ε)

The real-valued form, which is what the adversary lower bound produces.

Monotonicity in the error

theorem QuantumQueryComplexity.queryCounts_mono {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} {read : X → ι → σ} {f : X → O} {ε ε' : ℝ} (hε : ε ≤ ε') : QueryCounts read f ε ⊆ QueryCounts read f ε'

theorem QuantumQueryComplexity.qQueryOn_mono {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} {read : X → ι → σ} {f : X → O} {ε ε' : ℝ} (hε : ε ≤ ε') (hne : (QueryCounts read f ε).Nonempty) : qQueryOn read f ε' ≤ qQueryOn read f ε

Restriction to a promise

A promise problem whose output is a function of the observations is no harder than the total problem: run the total algorithm on the promised observations. No injectivity and no structure on read are needed.

theorem QuantumQueryComplexity.computesWithErrorOn_comp_read {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X W : Type} [Fintype W] [DecidableEq W] {A : QAlg ι σ O W} {q : ℕ} {f : (ι → σ) → O} {ε : ℝ} (h : ComputesWithErrorOn A q id f ε) (read : X → ι → σ) : ComputesWithErrorOn A q read (fun (x : X) => f (read x)) ε

A total algorithm, run on the promised observations.

theorem QuantumQueryComplexity.queryCounts_subset_of_read {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} (read : X → ι → σ) (f : (ι → σ) → O) (ε : ℝ) : QueryCounts id f ε ⊆ QueryCounts read (fun (x : X) => f (read x)) ε

theorem QuantumQueryComplexity.qQueryOn_comp_read_le_qQuery {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} (read : X → ι → σ) (f : (ι → σ) → O) {ε : ℝ} (hne : (QueryCounts id f ε).Nonempty) : qQueryOn read (fun (x : X) => f (read x)) ε ≤ qQuery f ε

The restriction bound: Q_ε(f ∘ read on the promise) ≤ Q_ε(f). This is what turns a promise lower bound into a lower bound on the honest total function.

The constant case

theorem QuantumQueryComplexity.qQueryOn_const_eq_zero {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [DecidableEq O] {X : Type} (read : X → ι → σ) {f : X → O} {c : O} (hf : ∀ (x : X), f x = c) {ε : ℝ} (hε : 0 ≤ ε) : qQueryOn read f ε = 0

A constant function has quantum query complexity zero.

Query routines: a composable layer above QAlg

QAlg is a whole algorithm — an initial state, a schedule, and a readout — and its schedule has an exact length. Circuit constructions need something smaller and composable: an operator built from queries, which can be sequenced, inverted, and controlled, and whose query count is tracked exactly. That is a QRoutine:

R.run a = U_len · O_a · U_{len-1} · ⋯ · O_a · U_0, exactly R.len queries.

A routine carries no initial state and no readout, so it composes; R.toAlg turns one into a QAlg at the end, and toAlg_state says the algorithm's state after R.len queries is R.run a applied to the initial state. So everything proved about QAlg — in particular the operational lower bound — applies to whatever the routine layer builds, with no change to the pinned statements.

Main results

• run_mem_unitaryGroup — a routine is a unitary for every input.
• toAlg_state — the bridge to QAlg.
• comp_run — sequencing: (R.comp S).run a = S.run a * R.run a with (R.comp S).len = R.len + S.len. Query counts add exactly; the boundary unitaries S.step 0 and R.step R.len are merged into one, which is why no query is wasted at the junction.
• exists_inv — inversion: every routine has an inverse routine of the same length. This is where the oracle being an involution pays: Oᴴ = O, so reversing a schedule costs no extra queries.
• runUpto_congr — routines agreeing on steps 0 … len have the same run, which is what lets constructions specify a schedule only where it matters.

structure QuantumQueryComplexity.QRoutine (ι σ W : Type) [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : Type

A query routine: len oracle calls interleaved with input-independent unitaries.

• len : ℕ

  The number of queries.

• step : ℕ → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ

  The input-independent unitaries; step t is applied after the t-th query, and step 0 before the first.

• step_unitary (t : ℕ) : self.step t ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ

  Each step is unitary.

theorem QuantumQueryComplexity.conjTranspose_mem_qUnitary {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) : U.conjTranspose ∈ Matrix.unitaryGroup H ℂ

The adjoint of a unitary is unitary.

def QuantumQueryComplexity.QRoutine.runWith {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (R : QRoutine ι σ W) : ℕ → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ

The operator implemented by the first t queries of R, with the opaque oracle matrix Q in place of the transposition oracle.

Equations

• QuantumQueryComplexity.QRoutine.runWith Q R 0 = R.step 0
• QuantumQueryComplexity.QRoutine.runWith Q R t.succ = R.step (t + 1) * (Q * QuantumQueryComplexity.QRoutine.runWith Q R t)

@[simp]

theorem QuantumQueryComplexity.QRoutine.runWith_zero {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (R : QRoutine ι σ W) : runWith Q R 0 = R.step 0

@[simp]

theorem QuantumQueryComplexity.QRoutine.runWith_succ {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (R : QRoutine ι σ W) (t : ℕ) : runWith Q R (t + 1) = R.step (t + 1) * (Q * runWith Q R t)

theorem QuantumQueryComplexity.QRoutine.runWith_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (R : QRoutine ι σ W) (hQ : Q ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) (t : ℕ) : runWith Q R t ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ

theorem QuantumQueryComplexity.QRoutine.runWith_congr {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) {R S : QRoutine ι σ W} {t : ℕ} (h : ∀ k ≤ t, R.step k = S.step k) : runWith Q R t = runWith Q S t

Only the steps up to t matter.

def QuantumQueryComplexity.QRoutine.runUpto {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) : ℕ → Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ

The operator implemented by the first t queries of R.

Equations

• R.runUpto a = QuantumQueryComplexity.QRoutine.runWith (QuantumQueryComplexity.oracleMat a) R

@[simp]

theorem QuantumQueryComplexity.QRoutine.runUpto_zero {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) : R.runUpto a 0 = R.step 0

@[simp]

theorem QuantumQueryComplexity.QRoutine.runUpto_succ {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (t : ℕ) : R.runUpto a (t + 1) = R.step (t + 1) * (oracleMat a * R.runUpto a t)

def QuantumQueryComplexity.QRoutine.run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ

The operator implemented by R, using exactly R.len queries.

Equations

• R.run a = R.runUpto a R.len

theorem QuantumQueryComplexity.QRoutine.runUpto_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (t : ℕ) : R.runUpto a t ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ

theorem QuantumQueryComplexity.QRoutine.run_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) : R.run a ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ

theorem QuantumQueryComplexity.QRoutine.runUpto_congr {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {R S : QRoutine ι σ W} (a : ι → σ) {t : ℕ} (h : ∀ k ≤ t, R.step k = S.step k) : R.runUpto a t = S.runUpto a t

Only the steps up to t matter for the first t queries.

The bridge to QAlg

def QuantumQueryComplexity.QRoutine.toAlg {ι σ O W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (init : QBasis ι σ W → ℂ) (hinit : IsQState init) (readout : QBasis ι σ W → O) : QAlg ι σ O W

Turn a routine into an algorithm by supplying an initial state and a readout.

Equations

• R.toAlg init hinit readout = { init := init, init_isQState := hinit, step := R.step, step_unitary := ⋯, readout := readout }

theorem QuantumQueryComplexity.QRoutine.toAlg_state {ι σ O W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (init : QBasis ι σ W → ℂ) (hinit : IsQState init) (readout : QBasis ι σ W → O) (a : ι → σ) (t : ℕ) : (R.toAlg init hinit readout).state a t = (R.runUpto a t).mulVec init

The bridge. The algorithm's state after t queries is the routine's operator applied to the initial state.

theorem QuantumQueryComplexity.QRoutine.toAlg_state_len {ι σ O W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (init : QBasis ι σ W → ℂ) (hinit : IsQState init) (readout : QBasis ι σ W → O) (a : ι → σ) : (R.toAlg init hinit readout).state a R.len = (R.run a).mulVec init

Sequencing

def QuantumQueryComplexity.QRoutine.comp {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) : QRoutine ι σ W

Sequencing: run R, then S. The two boundary unitaries are merged, so the query count is exactly R.len + S.len.

Equations

• R.comp S = { len := R.len + S.len, step := fun (t : ℕ) => if t < R.len then R.step t else if t = R.len then S.step 0 * R.step R.len else S.step (t - R.len), step_unitary := ⋯ }

@[simp]

theorem QuantumQueryComplexity.QRoutine.comp_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) : (R.comp S).len = R.len + S.len

theorem QuantumQueryComplexity.QRoutine.comp_step_of_lt {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) {t : ℕ} (h : t < R.len) : (R.comp S).step t = R.step t

theorem QuantumQueryComplexity.QRoutine.comp_step_self {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) : (R.comp S).step R.len = S.step 0 * R.step R.len

theorem QuantumQueryComplexity.QRoutine.comp_step_of_gt {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) {t : ℕ} (h : R.len < t) : (R.comp S).step t = S.step (t - R.len)

theorem QuantumQueryComplexity.QRoutine.runUpto_eq_runWith {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (t : ℕ) : R.runUpto a t = runWith (oracleMat a) R t

The standard semantics is the transposition-oracle instance.

theorem QuantumQueryComplexity.QRoutine.run_eq_runWith {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) : R.run a = runWith (oracleMat a) R R.len

Sequencing, parametrically

theorem QuantumQueryComplexity.QRoutine.comp_runWith_of_lt {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (R S : QRoutine ι σ W) {t : ℕ} (ht : t < R.len) : runWith Q (R.comp S) t = runWith Q R t

theorem QuantumQueryComplexity.QRoutine.comp_runWith_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (R S : QRoutine ι σ W) : runWith Q (R.comp S) R.len = S.step 0 * runWith Q R R.len

theorem QuantumQueryComplexity.QRoutine.comp_runWith_add {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (R S : QRoutine ι σ W) (k : ℕ) : runWith Q (R.comp S) (R.len + k) = runWith Q S k * runWith Q R R.len

theorem QuantumQueryComplexity.QRoutine.comp_runWith_full {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (R S : QRoutine ι σ W) : runWith Q (R.comp S) (R.len + S.len) = runWith Q S S.len * runWith Q R R.len

Sequencing against any oracle: the mirror of comp_run.

theorem QuantumQueryComplexity.QRoutine.comp_runUpto_of_lt {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) (a : ι → σ) {t : ℕ} (ht : t < R.len) : (R.comp S).runUpto a t = R.runUpto a t

theorem QuantumQueryComplexity.QRoutine.comp_runUpto_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) (a : ι → σ) : (R.comp S).runUpto a R.len = S.step 0 * R.runUpto a R.len

theorem QuantumQueryComplexity.QRoutine.comp_runUpto_add {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) (a : ι → σ) (k : ℕ) : (R.comp S).runUpto a (R.len + k) = S.runUpto a k * R.run a

theorem QuantumQueryComplexity.QRoutine.comp_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R S : QRoutine ι σ W) (a : ι → σ) : (R.comp S).run a = S.run a * R.run a

Sequencing, at the level of operators.

Padding by two

Padding by an even number of queries is free and needs no extra workspace: the oracle is an involution, so a query immediately followed by a query is the identity. Padding by one is a different matter — it needs somewhere to park the query index so that the extra query idles — and lives in SourceQuantumControl.

def QuantumQueryComplexity.QRoutine.padTwo {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : QRoutine ι σ W

Append two queries that cancel.

Equations

• R.padTwo = { len := R.len + 2, step := fun (t : ℕ) => if t ≤ R.len then R.step t else 1, step_unitary := ⋯ }

@[simp]

theorem QuantumQueryComplexity.QRoutine.padTwo_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : R.padTwo.len = R.len + 2

theorem QuantumQueryComplexity.QRoutine.padTwo_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) : R.padTwo.run a = R.run a

Padding by two changes nothing.

Inversion

The oracle is an involution with real entries, so it is self-adjoint; reversing a schedule therefore costs no extra queries. That is the content of the Oᴴ = O step below, and it is the reason the value oracle was chosen to be a transposition in the first place.

theorem QuantumQueryComplexity.QRoutine.oracleMat_conjTranspose {ι σ W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] (a : ι → σ) [Finite W] [Finite ι] [Finite σ] : (oracleMat a).conjTranspose = oracleMat a

theorem QuantumQueryComplexity.QRoutine.exists_inv {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : ∃ (R' : QRoutine ι σ W), R'.len = R.len ∧ ∀ (a : ι → σ), R'.run a = (R.run a).conjTranspose

Inversion. Every routine has an inverse routine of the same length.

Zero-query constructors, and an explicit inverse

def QuantumQueryComplexity.QRoutine.ofUnitary {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) : QRoutine ι σ W

A zero-query routine: just a unitary.

Equations

• QuantumQueryComplexity.QRoutine.ofUnitary U hU = { len := 0, step := fun (x : ℕ) => U, step_unitary := ⋯ }

@[simp]

theorem QuantumQueryComplexity.QRoutine.ofUnitary_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) : (ofUnitary U hU).len = 0

@[simp]

theorem QuantumQueryComplexity.QRoutine.ofUnitary_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) (a : ι → σ) : (ofUnitary U hU).run a = U

theorem QuantumQueryComplexity.QRoutine.ofUnitary_runWith {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (Q U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) : runWith Q (ofUnitary U hU) 0 = U

def QuantumQueryComplexity.QRoutine.identity {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : QRoutine ι σ W

The zero-query identity routine.

Equations

• QuantumQueryComplexity.QRoutine.identity = QuantumQueryComplexity.QRoutine.ofUnitary 1 ⋯

@[simp]

theorem QuantumQueryComplexity.QRoutine.identity_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : identity.len = 0

@[simp]

theorem QuantumQueryComplexity.QRoutine.identity_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) : identity.run a = 1

def QuantumQueryComplexity.QRoutine.query {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : QRoutine ι σ W

The one-query routine: a single bare oracle call.

Equations

• QuantumQueryComplexity.QRoutine.query = { len := 1, step := fun (x : ℕ) => 1, step_unitary := ⋯ }

@[simp]

theorem QuantumQueryComplexity.QRoutine.query_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : query.len = 1

@[simp]

theorem QuantumQueryComplexity.QRoutine.query_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) : query.run a = oracleMat a

noncomputable def QuantumQueryComplexity.QRoutine.inv {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : QRoutine ι σ W

An explicit inverse routine, chosen once from exists_inv.

Equations

• R.inv = ⋯.choose

@[simp]

theorem QuantumQueryComplexity.QRoutine.inv_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : R.inv.len = R.len

@[simp]

theorem QuantumQueryComplexity.QRoutine.inv_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) : R.inv.run a = (R.run a).conjTranspose

Conjugation and iteration

noncomputable def QuantumQueryComplexity.QRoutine.conjFixed {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) : QRoutine ι σ W

Conjugate a fixed unitary by a routine: run R, apply U, run R backwards. Costs 2 · R.len queries — no more, because inversion is free.

Equations

• R.conjFixed U hU = (R.comp (QuantumQueryComplexity.QRoutine.ofUnitary U hU)).comp R.inv

@[simp]

theorem QuantumQueryComplexity.QRoutine.conjFixed_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) : (R.conjFixed U hU).len = 2 * R.len

theorem QuantumQueryComplexity.QRoutine.conjFixed_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) (a : ι → σ) : (R.conjFixed U hU).run a = (R.run a).conjTranspose * (U * R.run a)

def QuantumQueryComplexity.QRoutine.iterate {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : ℕ → QRoutine ι σ W

Run R n times in sequence.

Equations

• R.iterate 0 = QuantumQueryComplexity.QRoutine.identity
• R.iterate t.succ = (R.iterate t).comp R

@[simp]

theorem QuantumQueryComplexity.QRoutine.iterate_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (n : ℕ) : (R.iterate n).len = n * R.len

theorem QuantumQueryComplexity.QRoutine.iterate_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (n : ℕ) : (R.iterate n).run a = R.run a ^ n

theorem QuantumQueryComplexity.state_eq_runUpto2 {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (n : ℕ) (a : ι → σ) (t : ℕ) : A.state a t = ({ len := n, step := A.step, step_unitary := ⋯ }.runUpto a t).mulVec A.init

The same bridge read backwards: an algorithm's state is the run of the routine formed from its own steps.

The controlled query, and idling

The value oracle has an idle index none, and SourceQuantumOracle records that it does nothing there. That is only half of what a circuit needs: to use the idle sector one must be able to move the query index into it and back, and "assign none to the index register" is not injective, hence not unitary.

The fix is the same one SourceQuantumReadAll used for copying: swap, don't assign. Extend the workspace with a control bit and a parking slot,

CtrlWork ι W = Bool × Option ι × W,

and let parkMat swap the index register with the parking slot exactly when the control bit is false. Then

ctrlQuery a = parkMat · O_a · parkMat

contains exactly one oracle factor and satisfies

• ctrlQuery_qBasis_true — on control true it is the query;
• ctrlQuery_qBasis_false — on control false with a blank slot it is the identity: the physical query is spent on the idle index.

So one physical query implements the controlled logical query, which is what phase detection will need, and what makes an idle query available for padding a schedule by one (padOne; padding by two needs no workspace at all, see QRoutine.padTwo).

IsParked names the sector this all happens in — control false, slot blank — and ctrlQuery_mulVec_of_parked upgrades the basis-state statement to states supported there, which is the form a padding argument consumes.

@[reducible, inline]

abbrev QuantumQueryComplexity.CtrlWork (ι W : Type) : Type

The workspace of a controlled routine: a control bit, a parking slot for the query index, and the original workspace.

Equations

• QuantumQueryComplexity.CtrlWork ι W = (Bool × Option ι × W)

@[instance_reducible]

instance QuantumQueryComplexity.instCtrlWorkDecidableEq {ι W : Type} [DecidableEq ι] [DecidableEq W] : DecidableEq (CtrlWork ι W)

Equations

• QuantumQueryComplexity.instCtrlWorkDecidableEq a b = instDecidableEqProd a b

@[instance_reducible]

instance QuantumQueryComplexity.instCtrlWorkFintype {ι W : Type} [Fintype ι] [Fintype W] : Fintype (CtrlWork ι W)

Equations

• QuantumQueryComplexity.instCtrlWorkFintype = { elems := Finset.univ ×ˢ Finset.univ, complete := ⋯ }

Parking

def QuantumQueryComplexity.parkMap {ι σ W : Type} : QBasis ι σ (CtrlWork ι W) → QBasis ι σ (CtrlWork ι W)

Swap the query-index register with the parking slot, unless the control bit says otherwise.

Equations

• QuantumQueryComplexity.parkMap (k, t, true, s, w) = (k, t, true, s, w)
• QuantumQueryComplexity.parkMap (k, t, false, s, w) = (s, t, false, k, w)

@[simp]

theorem QuantumQueryComplexity.parkMap_true {ι σ W : Type} (k : Option ι) (t : Option σ) (s : Option ι) (w : W) : parkMap (k, t, true, s, w) = (k, t, true, s, w)

@[simp]

theorem QuantumQueryComplexity.parkMap_false {ι σ W : Type} (k : Option ι) (t : Option σ) (s : Option ι) (w : W) : parkMap (k, t, false, s, w) = (s, t, false, k, w)

theorem QuantumQueryComplexity.parkMap_involutive {ι σ W : Type} : Function.Involutive parkMap

def QuantumQueryComplexity.parkPerm {ι σ W : Type} : Equiv.Perm (QBasis ι σ (CtrlWork ι W))

Parking, as a permutation of the basis.

Equations

• QuantumQueryComplexity.parkPerm = Function.Involutive.toPerm QuantumQueryComplexity.parkMap ⋯

def QuantumQueryComplexity.parkMat {ι σ W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] : Matrix (QBasis ι σ (CtrlWork ι W)) (QBasis ι σ (CtrlWork ι W)) ℂ

Parking, as a unitary.

Equations

• QuantumQueryComplexity.parkMat = QuantumQueryComplexity.qPerm QuantumQueryComplexity.parkPerm

theorem QuantumQueryComplexity.parkMat_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : parkMat ∈ Matrix.unitaryGroup (QBasis ι σ (CtrlWork ι W)) ℂ

theorem QuantumQueryComplexity.parkMat_mulVec_apply {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (ψ : QBasis ι σ (CtrlWork ι W) → ℂ) (p : QBasis ι σ (CtrlWork ι W)) : parkMat.mulVec ψ p = ψ (parkMap p)

The controlled query

def QuantumQueryComplexity.ctrlQuery {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) : Matrix (QBasis ι σ (CtrlWork ι W)) (QBasis ι σ (CtrlWork ι W)) ℂ

The controlled query: park, query, unpark. Note the single oracleMat factor — this costs exactly one physical query.

Equations

• QuantumQueryComplexity.ctrlQuery a = QuantumQueryComplexity.parkMat * (QuantumQueryComplexity.oracleMat a * QuantumQueryComplexity.parkMat)

theorem QuantumQueryComplexity.ctrlQuery_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) : ctrlQuery a ∈ Matrix.unitaryGroup (QBasis ι σ (CtrlWork ι W)) ℂ

def QuantumQueryComplexity.ctrlMap {ι σ W : Type} [DecidableEq σ] (a : ι → σ) : QBasis ι σ (CtrlWork ι W) → QBasis ι σ (CtrlWork ι W)

The basis action of the controlled query.

Equations

• QuantumQueryComplexity.ctrlMap a p = QuantumQueryComplexity.parkMap (QuantumQueryComplexity.oracleMap a (QuantumQueryComplexity.parkMap p))

theorem QuantumQueryComplexity.ctrlQuery_mulVec_apply {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (ψ : QBasis ι σ (CtrlWork ι W) → ℂ) (p : QBasis ι σ (CtrlWork ι W)) : (ctrlQuery a).mulVec ψ p = ψ (ctrlMap a p)

theorem QuantumQueryComplexity.ctrlMap_involutive {ι σ W : Type} [DecidableEq σ] (a : ι → σ) : Function.Involutive (ctrlMap a)

theorem QuantumQueryComplexity.ctrlQuery_mulVec_qBasis {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (r : QBasis ι σ (CtrlWork ι W)) : (ctrlQuery a).mulVec (qBasis r) = qBasis (ctrlMap a r)

theorem QuantumQueryComplexity.ctrlMap_true {ι σ W : Type} [DecidableEq σ] (a : ι → σ) (k : Option ι) (t : Option σ) (s : Option ι) (w : W) : ctrlMap a (k, t, true, s, w) = oracleMap a (k, t, true, s, w)

theorem QuantumQueryComplexity.ctrlMap_false_blank {ι σ W : Type} [DecidableEq σ] (a : ι → σ) (k : Option ι) (t : Option σ) (w : W) : ctrlMap a (k, t, false, none, w) = (k, t, false, none, w)

theorem QuantumQueryComplexity.ctrlQuery_qBasis_true {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (k : Option ι) (t : Option σ) (s : Option ι) (w : W) : (ctrlQuery a).mulVec (qBasis (k, t, true, s, w)) = (oracleMat a).mulVec (qBasis (k, t, true, s, w))

On the control-true sector the controlled query is the query.

theorem QuantumQueryComplexity.ctrlQuery_qBasis_false {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (k : Option ι) (t : Option σ) (w : W) : (ctrlQuery a).mulVec (qBasis (k, t, false, none, w)) = qBasis (k, t, false, none, w)

On the control-false sector with a blank slot the controlled query is the identity: the physical query is spent on the idle index.

The parked sector

def QuantumQueryComplexity.IsParked {ι σ W : Type} (ψ : QBasis ι σ (CtrlWork ι W) → ℂ) : Prop

A state is parked if it lives where the control bit is false and the parking slot is blank — the sector on which a query idles.

Equations

• QuantumQueryComplexity.IsParked ψ = ∀ (p : QuantumQueryComplexity.QBasis ι σ (QuantumQueryComplexity.CtrlWork ι W)), ψ p ≠ 0 → p.2.2.1 = false ∧ p.2.2.2.1 = none

theorem QuantumQueryComplexity.ctrlMap_eq_self {ι σ W : Type} [DecidableEq σ] {a : ι → σ} {p : QBasis ι σ (CtrlWork ι W)} (h1 : p.2.2.1 = false) (h2 : p.2.2.2.1 = none) : ctrlMap a p = p

theorem QuantumQueryComplexity.ctrlMap_not_parked {ι σ W : Type} [DecidableEq σ] {a : ι → σ} {p : QBasis ι σ (CtrlWork ι W)} (h : ¬(p.2.2.1 = false ∧ p.2.2.2.1 = none)) : ¬((ctrlMap a p).2.2.1 = false ∧ (ctrlMap a p).2.2.2.1 = none)

theorem QuantumQueryComplexity.ctrlQuery_mulVec_of_parked {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) {ψ : QBasis ι σ (CtrlWork ι W) → ℂ} (hψ : IsParked ψ) : (ctrlQuery a).mulVec ψ = ψ

A parked state does not notice a query. This is the form a padding argument consumes.

Idling and padding by one

def QuantumQueryComplexity.ctrlQueryRoutine {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : QRoutine ι σ (CtrlWork ι W)

The controlled query as a one-query routine.

Equations

• QuantumQueryComplexity.ctrlQueryRoutine = { len := 1, step := fun (x : ℕ) => QuantumQueryComplexity.parkMat, step_unitary := ⋯ }

@[simp]

theorem QuantumQueryComplexity.ctrlQueryRoutine_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : ctrlQueryRoutine.len = 1

theorem QuantumQueryComplexity.ctrlQueryRoutine_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) : ctrlQueryRoutine.run a = ctrlQuery a

def QuantumQueryComplexity.padOne {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ (CtrlWork ι W)) : QRoutine ι σ (CtrlWork ι W)

Padding by one query.

Equations

• QuantumQueryComplexity.padOne R = R.comp QuantumQueryComplexity.ctrlQueryRoutine

@[simp]

theorem QuantumQueryComplexity.padOne_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ (CtrlWork ι W)) : (padOne R).len = R.len + 1

theorem QuantumQueryComplexity.padOne_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ (CtrlWork ι W)) (a : ι → σ) : (padOne R).run a = ctrlQuery a * R.run a

theorem QuantumQueryComplexity.padOne_run_mulVec {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ (CtrlWork ι W)) (a : ι → σ) (ψ : QBasis ι σ (CtrlWork ι W) → ℂ) (h : IsParked ((R.run a).mulVec ψ)) : ((padOne R).run a).mulVec ψ = (R.run a).mulVec ψ

Padding by one is free on the parked sector.

Controlled execution of a whole routine

A fixed step is controlled by lifting it to the parked workspace and conditioning on the control bit — both instances of blockFam. A query is controlled by ctrlQuery. Neither adds a query, so control_len is an equality.

The statements are about the encoded subspace embedCtrl b ψ — control bit b, parking slot blank — and not global matrix identities, which would be false: off that subspace ctrlQuery swaps a parked index back in and queries it.

def QuantumQueryComplexity.embedCtrl {ι σ W : Type} [DecidableEq ι] (b : Bool) (ψ : QBasis ι σ W → ℂ) : QBasis ι σ (CtrlWork ι W) → ℂ

The blank-slot embedding: ψ in the sector with control bit b and an empty parking slot.

Equations

• QuantumQueryComplexity.embedCtrl b ψ = QuantumQueryComplexity.embedReg b (QuantumQueryComplexity.embedReg none ψ)

theorem QuantumQueryComplexity.embedCtrl_apply {ι σ W : Type} [DecidableEq ι] (b : Bool) (ψ : QBasis ι σ W → ℂ) (p : QBasis ι σ (CtrlWork ι W)) : embedCtrl b ψ p = if p.2.2.1 = b ∧ p.2.2.2.1 = none then ψ (p.1, p.2.1, p.2.2.2.2) else 0

theorem QuantumQueryComplexity.isParked_embedCtrl_false {ι σ W : Type} [DecidableEq ι] (ψ : QBasis ι σ W → ℂ) : IsParked (embedCtrl false ψ)

def QuantumQueryComplexity.ctrlStep {ι σ W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) : Matrix (QBasis ι σ (CtrlWork ι W)) (QBasis ι σ (CtrlWork ι W)) ℂ

A fixed step, lifted to the parked workspace and conditioned on the control bit.

Equations

• QuantumQueryComplexity.ctrlStep U = QuantumQueryComplexity.blockFam fun (b : Bool) => bif b then QuantumQueryComplexity.liftReg (Option ι) U else 1

theorem QuantumQueryComplexity.ctrlStep_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} (hU : U ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ) : ctrlStep U ∈ Matrix.unitaryGroup (QBasis ι σ (CtrlWork ι W)) ℂ

theorem QuantumQueryComplexity.ctrlStep_mulVec_embed_true {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (ψ : QBasis ι σ W → ℂ) : (ctrlStep U).mulVec (embedCtrl true ψ) = embedCtrl true (U.mulVec ψ)

theorem QuantumQueryComplexity.ctrlStep_mulVec_embed_false {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (ψ : QBasis ι σ W → ℂ) : (ctrlStep U).mulVec (embedCtrl false ψ) = embedCtrl false ψ

theorem QuantumQueryComplexity.parkMat_mulVec_embed_true {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (ψ : QBasis ι σ W → ℂ) : parkMat.mulVec (embedCtrl true ψ) = embedCtrl true ψ

theorem QuantumQueryComplexity.oracleMat_mulVec_embedCtrl {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (b : Bool) (ψ : QBasis ι σ W → ℂ) : (oracleMat a).mulVec (embedCtrl b ψ) = embedCtrl b ((oracleMat a).mulVec ψ)

theorem QuantumQueryComplexity.ctrlQuery_mulVec_embed_true {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (ψ : QBasis ι σ W → ℂ) : (ctrlQuery a).mulVec (embedCtrl true ψ) = embedCtrl true ((oracleMat a).mulVec ψ)

theorem QuantumQueryComplexity.ctrlQuery_mulVec_embed_false {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (a : ι → σ) (ψ : QBasis ι σ W → ℂ) : (ctrlQuery a).mulVec (embedCtrl false ψ) = embedCtrl false ψ

def QuantumQueryComplexity.controlUpto {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : ℕ → QRoutine ι σ (CtrlWork ι W)

The controlled routine, built one query at a time.

Equations

• One or more equations did not get rendered due to their size.
• QuantumQueryComplexity.controlUpto R 0 = QuantumQueryComplexity.QRoutine.ofUnitary (QuantumQueryComplexity.ctrlStep (R.step 0)) ⋯

def QuantumQueryComplexity.QRoutine.control {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : QRoutine ι σ (CtrlWork ι W)

Controlled execution of a routine.

Equations

• R.control = QuantumQueryComplexity.controlUpto R R.len

theorem QuantumQueryComplexity.controlUpto_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (t : ℕ) : (controlUpto R t).len = t

theorem QuantumQueryComplexity.control_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) : R.control.len = R.len

Controlling a routine costs no extra queries.

theorem QuantumQueryComplexity.controlUpto_run_true {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (t : ℕ) (ψ : QBasis ι σ W → ℂ) : ((controlUpto R t).run a).mulVec (embedCtrl true ψ) = embedCtrl true ((R.runUpto a t).mulVec ψ)

theorem QuantumQueryComplexity.controlUpto_run_false {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (t : ℕ) (ψ : QBasis ι σ W → ℂ) : ((controlUpto R t).run a).mulVec (embedCtrl false ψ) = embedCtrl false ψ

theorem QuantumQueryComplexity.control_run_true {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (ψ : QBasis ι σ W → ℂ) : (R.control.run a).mulVec (embedCtrl true ψ) = embedCtrl true ((R.run a).mulVec ψ)

On the control-true sector the controlled routine runs.

theorem QuantumQueryComplexity.control_run_false {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (ψ : QBasis ι σ W → ℂ) : (R.control.run a).mulVec (embedCtrl false ψ) = embedCtrl false ψ

On the control-false sector it does nothing — and still spends exactly R.len physical queries.

Lifting an operator along a factorizing equivalence

The generic tool of the independent-run compiler. A basis equivalence e : β ≃ γ × δ splits a space into a system and an environment; kronLift e M is M ⊗ 1 read through e, so its algebra is inherited from Mathlib's Kronecker product exactly as blockFam's came from blockDiagonal. The two working lemmas:

• kronLift_mulVec_splitVec — on a split state splitVec e φ ξ = φ((e·).1)·ξ((e·).2) the lift acts on the system factor alone;
• kronLiftRoutine_runUpto_splitVec — a routine's steps lifted along an oracle-compatible equivalence (one that carries the global query registers into the system factor: e (oracleMap a p) = (oracleMap a (e p).1, (e p).2)) run, against the real oracle, as the original routine on the system factor. The compatibility is stated at the map level, so no matrix identity for the oracle is ever needed.

def QuantumQueryComplexity.kronLift {β γ δ : Type} [DecidableEq δ] (e : β ≃ γ × δ) (M : Matrix γ γ ℂ) : Matrix β β ℂ

M ⊗ 1, read through the factorizing equivalence e.

Equations

• QuantumQueryComplexity.kronLift e M = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1).submatrix ⇑e ⇑e

theorem QuantumQueryComplexity.kronLift_mul {β γ δ : Type} [Fintype β] [Fintype γ] [DecidableEq δ] (e : β ≃ γ × δ) (M N : Matrix γ γ ℂ) [Finite δ] : kronLift e M * kronLift e N = kronLift e (M * N)

theorem QuantumQueryComplexity.kronLift_one {β γ δ : Type} [DecidableEq β] [DecidableEq γ] [DecidableEq δ] (e : β ≃ γ × δ) : kronLift e 1 = 1

theorem QuantumQueryComplexity.kronLift_conjTranspose {β γ δ : Type} [DecidableEq δ] (e : β ≃ γ × δ) (M : Matrix γ γ ℂ) : (kronLift e M).conjTranspose = kronLift e M.conjTranspose

theorem QuantumQueryComplexity.kronLift_mem_unitaryGroup {β γ δ : Type} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] [DecidableEq δ] (e : β ≃ γ × δ) {M : Matrix γ γ ℂ} (hM : M ∈ Matrix.unitaryGroup γ ℂ) [Finite δ] : kronLift e M ∈ Matrix.unitaryGroup β ℂ

def QuantumQueryComplexity.splitVec {β γ δ : Type} (e : β ≃ γ × δ) (φ : γ → ℂ) (ξ : δ → ℂ) : β → ℂ

A state of split form: φ on the system factor, ξ on the environment.

Equations

• QuantumQueryComplexity.splitVec e φ ξ b = φ (e b).1 * ξ (e b).2

@[simp]

theorem QuantumQueryComplexity.splitVec_apply {β γ δ : Type} (e : β ≃ γ × δ) (φ : γ → ℂ) (ξ : δ → ℂ) (b : β) : splitVec e φ ξ b = φ (e b).1 * ξ (e b).2

theorem QuantumQueryComplexity.kronLift_mulVec_splitVec {β γ δ : Type} [Fintype β] [Fintype γ] [DecidableEq δ] (e : β ≃ γ × δ) (M : Matrix γ γ ℂ) (φ : γ → ℂ) (ξ : δ → ℂ) [Finite δ] : (kronLift e M).mulVec (splitVec e φ ξ) = splitVec e (M.mulVec φ) ξ

The lift acts on the system factor of a split state.

theorem QuantumQueryComplexity.qNormSq_splitVec {β γ δ : Type} [Fintype β] [Fintype γ] [Fintype δ] (e : β ≃ γ × δ) (φ : γ → ℂ) (ξ : δ → ℂ) : qNormSq (splitVec e φ ξ) = qNormSq φ * qNormSq ξ

The squared norm of a split state is the product of the factors'.

The lifted routine

def QuantumQueryComplexity.OracleCompat {ι σ W W' D : Type} [DecidableEq σ] (e : QBasis ι σ W' ≃ QBasis ι σ W × D) : Prop

e is oracle-compatible when it carries the global query registers into the system factor and the environment rides along.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumQueryComplexity.oracleMat_mulVec_splitVec {ι σ W W' D : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] [Fintype W'] [DecidableEq W'] {e : QBasis ι σ W' ≃ QBasis ι σ W × D} (he : OracleCompat e) (a : ι → σ) (φ : QBasis ι σ W → ℂ) (ξ : D → ℂ) : (oracleMat a).mulVec (splitVec e φ ξ) = splitVec e ((oracleMat a).mulVec φ) ξ

The oracle preserves split states along an oracle-compatible equivalence, acting on the system factor.

def QuantumQueryComplexity.QRoutine.kronLift {ι σ W W' D : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] [Fintype W'] [DecidableEq W'] [Fintype D] [DecidableEq D] (e : QBasis ι σ W' ≃ QBasis ι σ W × D) (R : QRoutine ι σ W) : QRoutine ι σ W'

A routine's steps, lifted along e.

Equations

• QuantumQueryComplexity.QRoutine.kronLift e R = { len := R.len, step := fun (t : ℕ) => QuantumQueryComplexity.kronLift e (R.step t), step_unitary := ⋯ }

@[simp]

theorem QuantumQueryComplexity.QRoutine.kronLift_len {ι σ W W' D : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] [Fintype W'] [DecidableEq W'] [Fintype D] [DecidableEq D] (e : QBasis ι σ W' ≃ QBasis ι σ W × D) (R : QRoutine ι σ W) : (kronLift e R).len = R.len

theorem QuantumQueryComplexity.QRoutine.kronLift_runUpto_splitVec {ι σ W W' D : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] [Fintype W'] [DecidableEq W'] [Fintype D] [DecidableEq D] {e : QBasis ι σ W' ≃ QBasis ι σ W × D} (he : OracleCompat e) (R : QRoutine ι σ W) (a : ι → σ) (t : ℕ) (φ : QBasis ι σ W → ℂ) (ξ : D → ℂ) : ((kronLift e R).runUpto a t).mulVec (splitVec e φ ξ) = splitVec e ((R.runUpto a t).mulVec φ) ξ

The lifted routine runs as the original on the system factor.

Classical postprocessing of the readout

Relabelling an algorithm's measurement outcome costs nothing: QAlg.postcomp changes only the readout field, so the state — which is built from init and step alone — is literally unchanged, and the fibre sum can only grow the correct outcome's probability (qProb_comp_ge).

At the complexity level this is qQueryOn_postcomp_le : Q_ε(g ∘ f) ≤ Q_ε(f), the workhorse for reading a Boolean test off a large-valued output: it is how a lower bound proved for a Boolean postprocessing transfers to the function itself, and it is what makes lower bounds available for outputs whose type is too big (or infinite) for the Fintype-output machinery.

theorem QuantumQueryComplexity.qProb_comp_ge {H O O' : Type} [Fintype H] [DecidableEq O] [DecidableEq O'] (g : O → O') (r : H → O) (ψ : H → ℂ) (o : O) : qProb r ψ o ≤ qProb (fun (h : H) => g (r h)) ψ (g o)

Post-composing the readout can only increase the probability of the image outcome.

def QuantumQueryComplexity.QAlg.postcomp {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {O O' W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (g : O → O') : QAlg ι σ O' W

Relabelling the readout: same initial state, same steps, composed output map.

Equations

• A.postcomp g = { init := A.init, init_isQState := ⋯, step := A.step, step_unitary := ⋯, readout := fun (p : QuantumQueryComplexity.QBasis ι σ W) => g (A.readout p) }

@[simp]

theorem QuantumQueryComplexity.QAlg.postcomp_step {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {O O' W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (g : O → O') : (A.postcomp g).step = A.step

@[simp]

theorem QuantumQueryComplexity.QAlg.postcomp_init {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {O O' W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (g : O → O') : (A.postcomp g).init = A.init

@[simp]

theorem QuantumQueryComplexity.QAlg.postcomp_state {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {O O' W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (g : O → O') (a : ι → σ) (t : ℕ) : (A.postcomp g).state a t = A.state a t

@[simp]

theorem QuantumQueryComplexity.QAlg.postcomp_readout {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {O O' W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (g : O → O') : (A.postcomp g).readout = fun (p : QBasis ι σ W) => g (A.readout p)

theorem QuantumQueryComplexity.ComputesWithErrorOn.postcomp {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O O' W : Type} [DecidableEq O] [DecidableEq O'] [Fintype W] [DecidableEq W] {A : QAlg ι σ O W} {q : ℕ} {read : X → ι → σ} {F : X → O} {ε : ℝ} (h : ComputesWithErrorOn A q read F ε) (g : O → O') : ComputesWithErrorOn (A.postcomp g) q read (fun (x : X) => g (F x)) ε

Post-composition at the algorithm level: same cost, same error, the composed function.

theorem QuantumQueryComplexity.ComputesWithErrorOn.exists_postcomp {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O O' W : Type} [DecidableEq O] [DecidableEq O'] [Fintype W] [DecidableEq W] {A : QAlg ι σ O W} {q : ℕ} {read : X → ι → σ} {F : X → O} {ε : ℝ} (h : ComputesWithErrorOn A q read F ε) (g : O → O') : ∃ (W' : Type) (x : Fintype W') (x_1 : DecidableEq W') (A' : QAlg ι σ O' W'), ComputesWithErrorOn A' q read (fun (x : X) => g (F x)) ε

The workspace-existential form, for callers that quantify it away.

theorem QuantumQueryComplexity.queryCounts_postcomp {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O O' : Type} [DecidableEq O] [DecidableEq O'] (g : O → O') (read : X → ι → σ) (f : X → O) (ε : ℝ) : QueryCounts read f ε ⊆ QueryCounts read (fun (x : X) => g (f x)) ε

Every achievable query count survives postprocessing — the mirror of queryCounts_subset_of_read.

theorem QuantumQueryComplexity.qQueryOn_postcomp_le {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O O' : Type} [DecidableEq O] [DecidableEq O'] {read : X → ι → σ} {f : X → O} {ε : ℝ} (g : O → O') (hne : (QueryCounts read f ε).Nonempty) : qQueryOn read (fun (x : X) => g (f x)) ε ≤ qQueryOn read f ε

Classical postprocessing of the readout is free: post-composing the output function can only lower the quantum query complexity.

Reading the whole input exactly

Every observationally determined problem has an exact algorithm making |ι| queries. This is the theorem that makes qQueryOn a genuine minimum rather than sInf ∅ = 0, and it is the base case of the query model: it says the model can do at least what a classical algorithm can.

The construction records the answers in a workspace QRec ι σ = ι → Option σ and never leaves the computational basis. Two families of basis permutations do all the work:

• idxSwapPerm u v — transpose the two index-register values u and v. Since the index register's content is known at each time (it is idxAt t), a transposition suffices to move it to the next index; "assign the index register" would not be unitary, but "transpose the value it holds with the one it should hold next" is.
• slotSwapPerm j — swap the answer register with the workspace slot j. A swap, not a copy: copying is not injective, but the slot is blank when the swap happens, so the swap has the effect of a copy and clears the answer register for the next query.

The step unitary at time t is idxSwapPerm (prevIdx t) (idxAt t) after slotSwapPerm (prevIdx t), and the invariant carried by the induction is

state a t = |idxAt t⟩ |⊥⟩ |recAt a t⟩,

with recAt a t the record holding the answers of the first t indices. It holds for every t, with no side condition: past |ι| the index register is idle, the oracle acts trivially and the state stops moving, so the algorithm pads for free.

Two families of basis permutations

def QuantumQueryComplexity.idxSwapMap {ι σ : Type} [DecidableEq ι] {W : Type} (u v : Option ι) : QBasis ι σ W → QBasis ι σ W

Transpose two values of the query-index register.

Equations

• QuantumQueryComplexity.idxSwapMap u v p = ((Equiv.swap u v) p.1, p.2)

theorem QuantumQueryComplexity.idxSwapMap_involutive {ι σ : Type} [DecidableEq ι] {W : Type} (u v : Option ι) : Function.Involutive (idxSwapMap u v)

def QuantumQueryComplexity.idxSwapPerm {ι σ : Type} [DecidableEq ι] {W : Type} (u v : Option ι) : Equiv.Perm (QBasis ι σ W)

The index-register transposition, as a permutation of the basis.

Equations

• QuantumQueryComplexity.idxSwapPerm u v = Function.Involutive.toPerm (QuantumQueryComplexity.idxSwapMap u v) ⋯

@[simp]

theorem QuantumQueryComplexity.idxSwapPerm_apply {ι σ : Type} [DecidableEq ι] {W : Type} (u v : Option ι) (p : QBasis ι σ W) : (idxSwapPerm u v) p = ((Equiv.swap u v) p.1, p.2)

@[reducible, inline]

abbrev QuantumQueryComplexity.QRec (ι σ : Type) : Type

The workspace of the exact algorithm: a record of the answers seen so far.

Equations

• QuantumQueryComplexity.QRec ι σ = (ι → Option σ)

def QuantumQueryComplexity.slotSwapMap {ι σ : Type} [DecidableEq ι] (j : ι) : QBasis ι σ (QRec ι σ) → QBasis ι σ (QRec ι σ)

Swap the answer register with the workspace slot j.

Equations

• QuantumQueryComplexity.slotSwapMap j p = (p.1, p.2.2 j, Function.update p.2.2 j p.2.1)

theorem QuantumQueryComplexity.slotSwapMap_involutive {ι σ : Type} [DecidableEq ι] (j : ι) : Function.Involutive (slotSwapMap j)

def QuantumQueryComplexity.slotSwapPerm {ι σ : Type} [DecidableEq ι] : Option ι → Equiv.Perm (QBasis ι σ (QRec ι σ))

The slot swap at an optional index: at none there is nothing to store, so the algorithm idles. This is what lets one formula describe every step.

Equations

• QuantumQueryComplexity.slotSwapPerm none = 1
• QuantumQueryComplexity.slotSwapPerm (some j) = Function.Involutive.toPerm (QuantumQueryComplexity.slotSwapMap j) ⋯

@[simp]

theorem QuantumQueryComplexity.slotSwapPerm_none {ι σ : Type} [DecidableEq ι] : slotSwapPerm none = 1

@[simp]

theorem QuantumQueryComplexity.slotSwapPerm_some {ι σ : Type} [DecidableEq ι] (j : ι) (p : QBasis ι σ (QRec ι σ)) : (slotSwapPerm (some j)) p = (p.1, p.2.2 j, Function.update p.2.2 j p.2.1)

The schedule

noncomputable def QuantumQueryComplexity.idxAt (ι : Type) [Fintype ι] (t : ℕ) : Option ι

The index queried at time t; none once every index has been read.

Equations

• QuantumQueryComplexity.idxAt ι t = if h : t < Fintype.card ι then some ((Fintype.equivFin ι).symm ⟨t, h⟩) else none

noncomputable def QuantumQueryComplexity.prevIdx (ι : Type) [Fintype ι] : ℕ → Option ι

The index queried at time t - 1, i.e. the one whose answer the step at time t has to store.

Equations

• QuantumQueryComplexity.prevIdx ι 0 = none
• QuantumQueryComplexity.prevIdx ι t.succ = QuantumQueryComplexity.idxAt ι t

theorem QuantumQueryComplexity.idxAt_of_lt {ι : Type} [Fintype ι] {t : ℕ} (h : t < Fintype.card ι) : idxAt ι t = some ((Fintype.equivFin ι).symm ⟨t, h⟩)

theorem QuantumQueryComplexity.idxAt_eq_none_iff {ι : Type} [Fintype ι] (t : ℕ) : idxAt ι t = none ↔ Fintype.card ι ≤ t

theorem QuantumQueryComplexity.equivFin_of_idxAt {ι : Type} [Fintype ι] {t : ℕ} {j : ι} (h : idxAt ι t = some j) : ↑((Fintype.equivFin ι) j) = t

The record

noncomputable def QuantumQueryComplexity.recAt {ι σ : Type} [Fintype ι] (a : ι → σ) (t : ℕ) : QRec ι σ

The workspace after t queries: the answers at the first t indices.

Equations

• QuantumQueryComplexity.recAt a t i = if ↑((Fintype.equivFin ι) i) < t then some (a i) else none

theorem QuantumQueryComplexity.recAt_apply {ι σ : Type} [Fintype ι] (a : ι → σ) (t : ℕ) (i : ι) : recAt a t i = if ↑((Fintype.equivFin ι) i) < t then some (a i) else none

theorem QuantumQueryComplexity.recAt_zero {ι σ : Type} [Fintype ι] (a : ι → σ) : recAt a 0 = fun (x : ι) => none

theorem QuantumQueryComplexity.recAt_of_card_le {ι σ : Type} [Fintype ι] (a : ι → σ) {t : ℕ} (h : Fintype.card ι ≤ t) : recAt a t = fun (i : ι) => some (a i)

Once every index has been read the record is complete.

theorem QuantumQueryComplexity.update_recAt {ι σ : Type} [Fintype ι] [DecidableEq ι] (a : ι → σ) {t : ℕ} {j : ι} (hj : ↑((Fintype.equivFin ι) j) = t) : Function.update (recAt a t) j (some (a j)) = recAt a (t + 1)

Storing the answer at the index read at time t advances the record.

theorem QuantumQueryComplexity.recAt_self_eq_none {ι σ : Type} [Fintype ι] (a : ι → σ) {t : ℕ} {j : ι} (hj : ↑((Fintype.equivFin ι) j) = t) : recAt a t j = none

The slot the algorithm is about to write to is blank.

The algorithm

noncomputable def QuantumQueryComplexity.readAllAlg {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] (dec : QRec ι σ → O) : QAlg ι σ O (QRec ι σ)

The algorithm that reads every coordinate, announcing dec of the completed record.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumQueryComplexity.readAllAlg_readout {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] (dec : QRec ι σ → O) (p : QBasis ι σ (QRec ι σ)) : (readAllAlg dec).readout p = dec p.2.2

theorem QuantumQueryComplexity.readAllAlg_step_qBasis {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] (dec : QRec ι σ → O) (t : ℕ) (p : QBasis ι σ (QRec ι σ)) : ((readAllAlg dec).step t).mulVec (qBasis p) = qBasis ((idxSwapPerm (prevIdx ι t) (idxAt ι t)) ((slotSwapPerm (prevIdx ι t)) p))

theorem QuantumQueryComplexity.readAllAlg_state {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] (dec : QRec ι σ → O) (a : ι → σ) (t : ℕ) : (readAllAlg dec).state a t = qBasis (idxAt ι t, none, recAt a t)

The invariant. After t queries the algorithm holds the record of the first t answers, with the index register pointing at the next index and the answer register blank.

theorem QuantumQueryComplexity.readAllAlg_prob {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] (dec : QRec ι σ → O) [DecidableEq O] (a : ι → σ) : (readAllAlg dec).prob a (Fintype.card ι) (dec fun (i : ι) => some (a i)) = 1

The algorithm announces dec of the full input after |ι| queries.

Every observationally determined problem is exactly solvable

noncomputable def QuantumQueryComplexity.recDecode {ι σ O : Type} [Fintype ι] [DecidableEq σ] {X : Type} [Fintype X] [Nonempty O] (read : X → ι → σ) (f : X → O) (w : QRec ι σ) : O

The readout: decode a completed record into the value of f. Well defined by observational determinacy — two promise inputs with the same record are indistinguishable, hence have the same f-value.

Equations

• QuantumQueryComplexity.recDecode read f w = if h : ∃ (x : X), ∀ (i : ι), w i = some (read x i) then f h.choose else Classical.arbitrary O

theorem QuantumQueryComplexity.recDecode_apply {ι σ O : Type} [Fintype ι] [DecidableEq σ] {X : Type} [Fintype X] [Nonempty O] {read : X → ι → σ} {f : X → O} (hdet : ∀ (x y : X), read x = read y → f x = f y) (x : X) : (recDecode read f fun (i : ι) => some (read x i)) = f x

theorem QuantumQueryComplexity.exists_computesWithErrorOn {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} [DecidableEq O] [Nonempty O] {read : X → ι → σ} {f : X → O} (hdet : ∀ (x y : X), read x = read y → f x = f y) {ε : ℝ} (hε : 0 ≤ ε) [Finite X] : ∃ (A : QAlg ι σ O (QRec ι σ)), ComputesWithErrorOn A (Fintype.card ι) read f ε

Every observationally determined problem has an exact |ι|-query algorithm. In particular the set of achievable query counts is nonempty, so qQueryOn is a genuine minimum.

theorem QuantumQueryComplexity.queryCounts_nonempty {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} [DecidableEq O] [Nonempty O] {read : X → ι → σ} {f : X → O} (hdet : ∀ (x y : X), read x = read y → f x = f y) {ε : ℝ} (hε : 0 ≤ ε) [Finite X] : (QueryCounts read f ε).Nonempty

The achievable set is nonempty, which is the hypothesis every lower bound in SourceQuantumComplexity carries.

theorem QuantumQueryComplexity.qQueryOn_le_card {ι σ O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} [DecidableEq O] [Nonempty O] {read : X → ι → σ} {f : X → O} (hdet : ∀ (x y : X), read x = read y → f x = f y) {ε : ℝ} (hε : 0 ≤ ε) [Finite X] : qQueryOn read f ε ≤ Fintype.card ι

Reading everything is enough: qQueryOn ≤ |ι|.

Running a routine against an arbitrary oracle matrix

The QRoutine.runWith semantics and composition laws are proved alongside QRoutine in SourceQuantumRoutine. The standard runUpto semantics is their transposition-oracle specialization. Both the standard and XOR simulation compilers use the shared arbitrary-oracle implementation.

The uniform alphabet factorization

This alphabet factorization removes the √|σ| loss in uniform extraction.

A dual solution has to realise the inequality indicator [a ≠ b] as an inner product of vectors attached to the two letters. The construction used so far copies a value onto every letter that differs, so its norms grow like √|σ|. The uniform replacement lives on Option σ — one extra "constant" coordinate beside the σ-indexed ones. The vectors live in an ambient space of dimension |σ| + 1, but each is supported on exactly two coordinates; they are two-sparse independently of the alphabet size:

μ a = (1,  e a)          ν b = (1, − e b)

⟨μ a, ν b⟩ = 1 − δ_{ab} = [a ≠ b]
‖μ a‖² = ‖ν b‖² = 2

The constant coordinate contributes 1 to every pairing; the letter coordinates contribute −1 exactly when the letters agree, cancelling it. Both squared norms are 2 — equivalently both norms are √2 — independently of the alphabet size, which is the whole point.

def QuantumQueryComplexity.uniformLeft {σ : Type} [DecidableEq σ] (a : σ) : Option σ → ℝ

The left vector of the factorization: 1 on the constant coordinate and 1 at its own letter.

Equations

• QuantumQueryComplexity.uniformLeft a none = 1
• QuantumQueryComplexity.uniformLeft a (some j) = if j = a then 1 else 0

def QuantumQueryComplexity.uniformRight {σ : Type} [DecidableEq σ] (b : σ) : Option σ → ℝ

The right vector: 1 on the constant coordinate and −1 at its own letter.

Equations

• QuantumQueryComplexity.uniformRight b none = 1
• QuantumQueryComplexity.uniformRight b (some j) = if j = b then -1 else 0

@[simp]

theorem QuantumQueryComplexity.uniformLeft_none {σ : Type} [DecidableEq σ] (a : σ) : uniformLeft a none = 1

@[simp]

theorem QuantumQueryComplexity.uniformLeft_some {σ : Type} [DecidableEq σ] (a x : σ) : uniformLeft a (some x) = if x = a then 1 else 0

@[simp]

theorem QuantumQueryComplexity.uniformRight_none {σ : Type} [DecidableEq σ] (b : σ) : uniformRight b none = 1

@[simp]

theorem QuantumQueryComplexity.uniformRight_some {σ : Type} [DecidableEq σ] (b x : σ) : uniformRight b (some x) = if x = b then -1 else 0

theorem QuantumQueryComplexity.uniform_dotProduct {σ : Type} [Fintype σ] [DecidableEq σ] (a b : σ) : uniformLeft a ⬝ᵥ uniformRight b = if a = b then 0 else 1

The factorization: the pairing is the inequality indicator.

theorem QuantumQueryComplexity.uniformLeft_normSq {σ : Type} [Fintype σ] [DecidableEq σ] (a : σ) : uniformLeft a ⬝ᵥ uniformLeft a = 2

Both squared norms are 2 — equivalently both norms are √2 — independently of the alphabet size.

theorem QuantumQueryComplexity.uniformRight_normSq {σ : Type} [Fintype σ] [DecidableEq σ] (b : σ) : uniformRight b ⬝ᵥ uniformRight b = 2

theorem QuantumQueryComplexity.uniform_dotProduct_eq_zero_iff {σ : Type} [Fintype σ] [DecidableEq σ] (a b : σ) : uniformLeft a ⬝ᵥ uniformRight b = 0 ↔ a = b

The factorization in the form the dual constraint consumes: the pairing vanishes exactly when the letters agree, i.e. when the query does not distinguish the two inputs.

The Hadamard test, compiled

The generic measurement layer of the algorithm extraction: given a routine R and a unit vector u, the Hadamard test prepares (|0⟩ + |1⟩)/√2 ⊗ u, runs R controlled on the first qubit, applies a Hadamard to it, and measures it. The whole point:

P(announce true)  = (1 + Re⟪u, R.run a · u⟫)/2
P(announce false) = (1 − Re⟪u, R.run a · u⟫)/2

(hadTest_prob_true / hadTest_prob_false) — the test turns the real part of the expectation ⟪u, R_a u⟫, which the fidelity bounds of SourceQuantumFidelity control, into an outcome probability, at exactly R.len queries (QRoutine.control costs R.len, the Hadamards are free).

The compilation reuses the existing plumbing wholesale: QRoutine.control for the controlled run, regOp for the Hadamard on the control register, comp/ofUnitary for the final gate, and toAlg for the bridge to QAlg. The announcement convention is true on control 0: the detector this test will be applied to is ≈ +1 on the accepting side, so acceptance is constructive interference back onto |0⟩.

hadMat is real symmetric, and everything about it is decided entrywise over Bool — no 2 × 2 matrix theory is imported.

The Hadamard gate, on the control register

noncomputable def QuantumQueryComplexity.hadS : ℂ

1/√2, as a complex scalar.

Equations

• QuantumQueryComplexity.hadS = ↑(√2)⁻¹

theorem QuantumQueryComplexity.star_hadS : star hadS = hadS

theorem QuantumQueryComplexity.hadS_mul_hadS : hadS * hadS = 2⁻¹

theorem QuantumQueryComplexity.normSq_hadS : Complex.normSq hadS = 2⁻¹

noncomputable def QuantumQueryComplexity.hadMat : Matrix Bool Bool ℂ

The Hadamard gate on one qubit: (1/√2)·(−1)^{b·b'}.

Equations

• QuantumQueryComplexity.hadMat = Matrix.of fun (b b' : Bool) => if (b && b') = true then -QuantumQueryComplexity.hadS else QuantumQueryComplexity.hadS

@[simp]

theorem QuantumQueryComplexity.hadMat_apply (b b' : Bool) : hadMat b b' = if (b && b') = true then -hadS else hadS

theorem QuantumQueryComplexity.hadMat_mem_unitaryGroup : hadMat ∈ Matrix.unitaryGroup Bool ℂ

noncomputable def QuantumQueryComplexity.ctrlHad {ι σ W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] : Matrix (QBasis ι σ (CtrlWork ι W)) (QBasis ι σ (CtrlWork ι W)) ℂ

The Hadamard on the control register of CtrlWork.

Equations

• QuantumQueryComplexity.ctrlHad = QuantumQueryComplexity.regOp QuantumQueryComplexity.hadMat

theorem QuantumQueryComplexity.regOp_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {V : Type} [Fintype V] [DecidableEq V] {A : Matrix V V ℂ} (hA : A ∈ Matrix.unitaryGroup V ℂ) : regOp A ∈ Matrix.unitaryGroup (QBasis ι σ (V × W)) ℂ

theorem QuantumQueryComplexity.ctrlHad_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] : ctrlHad ∈ Matrix.unitaryGroup (QBasis ι σ (CtrlWork ι W)) ℂ

theorem QuantumQueryComplexity.ctrlHad_mulVec_embedCtrl {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (b : Bool) (ψ : QBasis ι σ W → ℂ) : ctrlHad.mulVec (embedCtrl b ψ) = hadMat true b • embedCtrl true ψ + hadMat false b • embedCtrl false ψ

The Hadamard acts on the control sectors as its column says.

Sector algebra

theorem QuantumQueryComplexity.embedCtrl_add {ι σ W : Type} [DecidableEq ι] (b : Bool) (ψ φ : QBasis ι σ W → ℂ) : embedCtrl b (ψ + φ) = embedCtrl b ψ + embedCtrl b φ

theorem QuantumQueryComplexity.embedCtrl_sub {ι σ W : Type} [DecidableEq ι] (b : Bool) (ψ φ : QBasis ι σ W → ℂ) : embedCtrl b (ψ - φ) = embedCtrl b ψ - embedCtrl b φ

theorem QuantumQueryComplexity.qNormSq_embedCtrl {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] (b : Bool) (ψ : QBasis ι σ W → ℂ) : qNormSq (embedCtrl b ψ) = qNormSq ψ

theorem QuantumQueryComplexity.qInner_embedCtrl {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] (b b' : Bool) (ψ φ : QBasis ι σ W → ℂ) : qInner (embedCtrl b ψ) (embedCtrl b' φ) = if b = b' then qInner ψ φ else 0

The test

noncomputable def QuantumQueryComplexity.hadInit {ι σ W : Type} [DecidableEq ι] (u : QBasis ι σ W → ℂ) : QBasis ι σ (CtrlWork ι W) → ℂ

The Hadamard-test initial state: (|0⟩ + |1⟩)/√2 ⊗ u.

Equations

• QuantumQueryComplexity.hadInit u = QuantumQueryComplexity.hadS • (QuantumQueryComplexity.embedCtrl false u + QuantumQueryComplexity.embedCtrl true u)

theorem QuantumQueryComplexity.isQState_hadInit {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] {u : QBasis ι σ W → ℂ} (hu : IsQState u) : IsQState (hadInit u)

noncomputable def QuantumQueryComplexity.hadTest {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (u : QBasis ι σ W → ℂ) (hu : IsQState u) : QAlg ι σ Bool (CtrlWork ι W)

The Hadamard test of R on u: controlled-R between two Hadamards on a control qubit, measuring the control. Announces true on control 0. Costs exactly R.len queries.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumQueryComplexity.hadTest_readout {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (u : QBasis ι σ W → ℂ) (hu : IsQState u) : (hadTest R u hu).readout = fun (p : QBasis ι σ (CtrlWork ι W)) => !p.2.2.1

theorem QuantumQueryComplexity.hadTest_state {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (u : QBasis ι σ W → ℂ) (hu : IsQState u) (a : ι → σ) : (hadTest R u hu).state a R.len = (hadS * hadS) • (embedCtrl false (u + (R.run a).mulVec u) + embedCtrl true (u - (R.run a).mulVec u))

The final state of the test, exactly: interference between u and R_a u, sorted by the control bit.

theorem QuantumQueryComplexity.qProb_hadReadout_true {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] (a : ℂ) (χ₁ χ₂ : QBasis ι σ W → ℂ) : qProb (fun (p : QBasis ι σ (CtrlWork ι W)) => !p.2.2.1) (a • (embedCtrl false χ₁ + embedCtrl true χ₂)) true = Complex.normSq a * qNormSq χ₁

The measurement rule of the sorted state.

theorem QuantumQueryComplexity.qProb_hadReadout_false {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] (a : ℂ) (χ₁ χ₂ : QBasis ι σ W → ℂ) : qProb (fun (p : QBasis ι σ (CtrlWork ι W)) => !p.2.2.1) (a • (embedCtrl false χ₁ + embedCtrl true χ₂)) false = Complex.normSq a * qNormSq χ₂

theorem QuantumQueryComplexity.hadTest_prob_true {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) {u : QBasis ι σ W → ℂ} (hu : IsQState u) (a : ι → σ) : (hadTest R u hu).prob a R.len true = (1 + (qInner u ((R.run a).mulVec u)).re) / 2

The acceptance probability of the Hadamard test.

theorem QuantumQueryComplexity.hadTest_prob_false {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) {u : QBasis ι σ W → ℂ} (hu : IsQState u) (a : ι → σ) : (hadTest R u hu).prob a R.len false = (1 - (qInner u ((R.run a).mulVec u)).re) / 2

The rejection probability of the Hadamard test.

The independent-run compiler: exact product statistics

Two algorithms, compiled into one whose outcome distribution is the exact product of theirs — the engine of amplification and of the finite-output construction.

Banks, not uncompute. The compiled workspace holds a full QBasis ι σ Wⱼ-valued bank for each algorithm; the global initial state is the tensor product of the two initial states parked in their banks, with blank global query registers. Phase j swaps bank j into the active position (a basis permutation exchanging the global query/answer registers with the bank's stored pair), runs algorithm j's schedule lifted along the oracle-compatible equivalence pairEquivⱼ (SourceQuantumKronLift), and swaps back. Each phase therefore acts on a pristine tensor factor: no uncompute, no factor two in the cost, and the final state is literally

prodState blank (A₁.state a q₁) (A₂.state a q₂),

so the joint measurement factorizes exactly (qProb_pairReadout).

Realizes read q P packages "some algorithm has outcome distribution P after q queries"; Realizes.pair is the compiler, Realizes.map reshapes outcomes through the readout for free, and Realizes.fold iterates the pair into a k-tuple with product statistics at cost ∑ qⱼ.

The two factorizing equivalences and the two swaps

def QuantumQueryComplexity.pairEquiv₁ {ι σ W₁ W₂ : Type} : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂) ≃ QBasis ι σ W₁ × (Option ι × Option σ) × QBasis ι σ W₂

Phase 1's view: system = (global registers, bank 1's workspace), environment = (bank 1's parked registers, bank 2).

Equations

• One or more equations did not get rendered due to their size.

def QuantumQueryComplexity.pairEquiv₂ {ι σ W₁ W₂ : Type} : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂) ≃ QBasis ι σ W₂ × (Option ι × Option σ) × QBasis ι σ W₁

Phase 2's view.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumQueryComplexity.oracleCompat_pairEquiv₁ {ι σ : Type} [DecidableEq σ] {W₁ W₂ : Type} : OracleCompat pairEquiv₁

theorem QuantumQueryComplexity.oracleCompat_pairEquiv₂ {ι σ : Type} [DecidableEq σ] {W₁ W₂ : Type} : OracleCompat pairEquiv₂

def QuantumQueryComplexity.pairSwap₁Map {ι σ W₁ W₂ : Type} : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂) → QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)

Swap the global query/answer registers with bank 1's parked pair.

Equations

• QuantumQueryComplexity.pairSwap₁Map (idx, ans, (i₁, a₁, w₁), β₂) = (i₁, a₁, (idx, ans, w₁), β₂)

theorem QuantumQueryComplexity.pairSwap₁Map_involutive {ι σ W₁ W₂ : Type} : Function.Involutive pairSwap₁Map

def QuantumQueryComplexity.pairSwap₂Map {ι σ W₁ W₂ : Type} : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂) → QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)

Swap the global query/answer registers with bank 2's parked pair.

Equations

• QuantumQueryComplexity.pairSwap₂Map (idx, ans, β₁, i₂, a₂, w₂) = (i₂, a₂, β₁, idx, ans, w₂)

theorem QuantumQueryComplexity.pairSwap₂Map_involutive {ι σ W₁ W₂ : Type} : Function.Involutive pairSwap₂Map

def QuantumQueryComplexity.pairSwap₁Mat {ι σ : Type} [DecidableEq ι] [DecidableEq σ] {W₁ W₂ : Type} [DecidableEq W₁] [DecidableEq W₂] : Matrix (QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)) (QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)) ℂ

The swap-in unitary for bank 1.

Equations

• QuantumQueryComplexity.pairSwap₁Mat = QuantumQueryComplexity.qPerm (Function.Involutive.toPerm QuantumQueryComplexity.pairSwap₁Map ⋯)

theorem QuantumQueryComplexity.pairSwap₁Mat_mem_unitaryGroup {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] : pairSwap₁Mat ∈ Matrix.unitaryGroup (QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)) ℂ

theorem QuantumQueryComplexity.pairSwap₁Mat_mulVec_apply {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (ψ : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂) → ℂ) (p : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)) : pairSwap₁Mat.mulVec ψ p = ψ (pairSwap₁Map p)

def QuantumQueryComplexity.pairSwap₂Mat {ι σ : Type} [DecidableEq ι] [DecidableEq σ] {W₁ W₂ : Type} [DecidableEq W₁] [DecidableEq W₂] : Matrix (QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)) (QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)) ℂ

The swap-in unitary for bank 2.

Equations

• QuantumQueryComplexity.pairSwap₂Mat = QuantumQueryComplexity.qPerm (Function.Involutive.toPerm QuantumQueryComplexity.pairSwap₂Map ⋯)

theorem QuantumQueryComplexity.pairSwap₂Mat_mem_unitaryGroup {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] : pairSwap₂Mat ∈ Matrix.unitaryGroup (QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)) ℂ

theorem QuantumQueryComplexity.pairSwap₂Mat_mulVec_apply {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (ψ : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂) → ℂ) (p : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)) : pairSwap₂Mat.mulVec ψ p = ψ (pairSwap₂Map p)

Product states

def QuantumQueryComplexity.prodState {ι σ W₁ W₂ : Type} (χ : Option ι × Option σ → ℂ) (ψ₁ : QBasis ι σ W₁ → ℂ) (ψ₂ : QBasis ι σ W₂ → ℂ) : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂) → ℂ

The banked product state: χ on the global registers, ψⱼ in bank j.

Equations

• QuantumQueryComplexity.prodState χ ψ₁ ψ₂ p = χ (p.1, p.2.1) * ψ₁ p.2.2.1 * ψ₂ p.2.2.2

def QuantumQueryComplexity.blankReg {ι σ : Type} [DecidableEq ι] [DecidableEq σ] : Option ι × Option σ → ℂ

Blank global registers.

Equations

• QuantumQueryComplexity.blankReg q = if q = (none, none) then 1 else 0

theorem QuantumQueryComplexity.sum_normSq_blankReg {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] : ∑ q : Option ι × Option σ, Complex.normSq (blankReg q) = 1

theorem QuantumQueryComplexity.qNormSq_prodState {ι σ : Type} [Fintype ι] [Fintype σ] {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] (χ : Option ι × Option σ → ℂ) (ψ₁ : QBasis ι σ W₁ → ℂ) (ψ₂ : QBasis ι σ W₂ → ℂ) : qNormSq (prodState χ ψ₁ ψ₂) = (∑ q : Option ι × Option σ, Complex.normSq (χ q)) * qNormSq ψ₁ * qNormSq ψ₂

theorem QuantumQueryComplexity.isQState_prodState {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] {ψ₁ : QBasis ι σ W₁ → ℂ} {ψ₂ : QBasis ι σ W₂ → ℂ} (h₁ : IsQState ψ₁) (h₂ : IsQState ψ₂) : IsQState (prodState blankReg ψ₁ ψ₂)

The phase actions

theorem QuantumQueryComplexity.pairSwap₁_mulVec_prodState {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (χ : Option ι × Option σ → ℂ) (ψ₁ : QBasis ι σ W₁ → ℂ) (ψ₂ : QBasis ι σ W₂ → ℂ) : pairSwap₁Mat.mulVec (prodState χ ψ₁ ψ₂) = splitVec pairEquiv₁ ψ₁ fun (q : (Option ι × Option σ) × QBasis ι σ W₂) => χ q.1 * ψ₂ q.2

theorem QuantumQueryComplexity.pairSwap₁_mulVec_splitVec {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (χ : Option ι × Option σ → ℂ) (ψ₁ : QBasis ι σ W₁ → ℂ) (ψ₂ : QBasis ι σ W₂ → ℂ) : pairSwap₁Mat.mulVec (splitVec pairEquiv₁ ψ₁ fun (q : (Option ι × Option σ) × QBasis ι σ W₂) => χ q.1 * ψ₂ q.2) = prodState χ ψ₁ ψ₂

theorem QuantumQueryComplexity.pairSwap₂_mulVec_prodState {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (χ : Option ι × Option σ → ℂ) (ψ₁ : QBasis ι σ W₁ → ℂ) (ψ₂ : QBasis ι σ W₂ → ℂ) : pairSwap₂Mat.mulVec (prodState χ ψ₁ ψ₂) = splitVec pairEquiv₂ ψ₂ fun (q : (Option ι × Option σ) × QBasis ι σ W₁) => χ q.1 * ψ₁ q.2

theorem QuantumQueryComplexity.pairSwap₂_mulVec_splitVec {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (χ : Option ι × Option σ → ℂ) (ψ₁ : QBasis ι σ W₁ → ℂ) (ψ₂ : QBasis ι σ W₂ → ℂ) : pairSwap₂Mat.mulVec (splitVec pairEquiv₂ ψ₂ fun (q : (Option ι × Option σ) × QBasis ι σ W₁) => χ q.1 * ψ₁ q.2) = prodState χ ψ₁ ψ₂

The compiled routine

def QuantumQueryComplexity.pairRoutine {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (R₁ : QRoutine ι σ W₁) (R₂ : QRoutine ι σ W₂) : QRoutine ι σ (QBasis ι σ W₁ × QBasis ι σ W₂)

The pair compiler: swap in bank 1, run schedule 1 lifted, swap out; swap in bank 2, run schedule 2 lifted, swap out. R₁.len + R₂.len queries.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumQueryComplexity.pairRoutine_len {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (R₁ : QRoutine ι σ W₁) (R₂ : QRoutine ι σ W₂) : (pairRoutine R₁ R₂).len = R₁.len + R₂.len

theorem QuantumQueryComplexity.pairRoutine_run_prodState {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {W₁ W₂ : Type} [Fintype W₁] [DecidableEq W₁] [Fintype W₂] [DecidableEq W₂] (R₁ : QRoutine ι σ W₁) (R₂ : QRoutine ι σ W₂) (a : ι → σ) (χ : Option ι × Option σ → ℂ) (ψ₁ : QBasis ι σ W₁ → ℂ) (ψ₂ : QBasis ι σ W₂ → ℂ) : ((pairRoutine R₁ R₂).run a).mulVec (prodState χ ψ₁ ψ₂) = prodState χ ((R₁.run a).mulVec ψ₁) ((R₂.run a).mulVec ψ₂)

The compiled run is the product of the runs.

The joint measurement factorizes

def QuantumQueryComplexity.pairReadout {ι σ W₁ W₂ O₁ O₂ : Type} (r₁ : QBasis ι σ W₁ → O₁) (r₂ : QBasis ι σ W₂ → O₂) : QBasis ι σ (QBasis ι σ W₁ × QBasis ι σ W₂) → O₁ × O₂

Read both banks.

Equations

• QuantumQueryComplexity.pairReadout r₁ r₂ p = (r₁ p.2.2.1, r₂ p.2.2.2)

theorem QuantumQueryComplexity.qProb_pairReadout {ι σ : Type} [Fintype ι] [Fintype σ] {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] {O₁ O₂ : Type} [DecidableEq O₁] [DecidableEq O₂] (r₁ : QBasis ι σ W₁ → O₁) (r₂ : QBasis ι σ W₂ → O₂) (χ : Option ι × Option σ → ℂ) (ψ₁ : QBasis ι σ W₁ → ℂ) (ψ₂ : QBasis ι σ W₂ → ℂ) (o₁ : O₁) (o₂ : O₂) : qProb (pairReadout r₁ r₂) (prodState χ ψ₁ ψ₂) (o₁, o₂) = (∑ q : Option ι × Option σ, Complex.normSq (χ q)) * qProb r₁ ψ₁ o₁ * qProb r₂ ψ₂ o₂

Realizes, and the product-run calculus

def QuantumQueryComplexity.Realizes {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O : Type} [DecidableEq O] (read : X → ι → σ) (q : ℕ) (P : X → O → ℝ) : Prop

Some algorithm has outcome distribution P after q queries.

Equations

• QuantumQueryComplexity.Realizes read q P = ∃ (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (A : QuantumQueryComplexity.QAlg ι σ O W), ∀ (x_2 : X) (o : O), A.prob (read x_2) q o = P x_2 o

theorem QuantumQueryComplexity.Realizes.congr {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O : Type} [DecidableEq O] {read : X → ι → σ} {q : ℕ} {P Q : X → O → ℝ} (h : Realizes read q P) (hPQ : ∀ (x : X) (o : O), P x o = Q x o) : Realizes read q Q

theorem QuantumQueryComplexity.Realizes.nonneg {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O : Type} [DecidableEq O] {read : X → ι → σ} {q : ℕ} {P : X → O → ℝ} (h : Realizes read q P) (x : X) (o : O) : 0 ≤ P x o

Every distribution an algorithm realizes is one the model measures: values are probabilities of the final state.

theorem QuantumQueryComplexity.Realizes.pair {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O O' : Type} [DecidableEq O] [DecidableEq O'] {read : X → ι → σ} {q₁ q₂ : ℕ} {P₁ : X → O → ℝ} {P₂ : X → O' → ℝ} (h₁ : Realizes read q₁ P₁) (h₂ : Realizes read q₂ P₂) : Realizes read (q₁ + q₂) fun (x : X) (o : O × O') => P₁ x o.1 * P₂ x o.2

The pair compiler, packaged: two realizable distributions have a jointly realizable product, at the sum of the costs.

theorem QuantumQueryComplexity.Realizes.map {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O O' : Type} [DecidableEq O] [DecidableEq O'] [Fintype O] {read : X → ι → σ} {q : ℕ} {P : X → O → ℝ} (h : Realizes read q P) (g : O → O') : Realizes read q fun (x : X) (o' : O') => ∑ o : O with g o = o', P x o

Reshaping the outcome through the readout is free.

theorem QuantumQueryComplexity.Realizes.map_equiv {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O O' : Type} [DecidableEq O] [DecidableEq O'] {read : X → ι → σ} {q : ℕ} {P : X → O → ℝ} (h : Realizes read q P) (g : O ≃ O') : Realizes read q fun (x : X) (o' : O') => P x (g.symm o')

The bijective special case: relabel the outcomes.

The standard Boolean XOR oracle, and its query model

The conventional oracle for Boolean inputs: on the answer register,

|i⟩|b⟩|w⟩ ↦ |i⟩|b ⊕ a i⟩|w⟩,

with an idle index (none, no query) and a fixed blank answer — on this model's basis QBasis ι Bool W the answer register is Option Bool, the XOR acts on the some-part, and both none sectors are fixed. Boolean specifically: for an arbitrary alphabet there is no canonical XOR directly on σ without choosing a group structure, so the simulation theorems start here. The upstream construction (upstream OneHot.lean) instead XORs an encoding of the letter — its one-hot code in Hot σ := σ → Bool — which needs no structure on σ.

Like the transposition oracle it is a basis permutation and an involution, so unitarity and query = unquery are free.

The model: QAlg is oracle-agnostic data (initial state, steps, readout); only the state semantics names the oracle. xorState is QAlg.state with xorOracleMat in place of oracleMat, and XorComputesWithErrorOn, XorQueryCounts, xorQQueryOn mirror the standard model's definitions verbatim. SourceQuantumSimulation proves the two models equivalent within a factor of two in the query count.

The XOR on an optional Boolean

def QuantumQueryComplexity.optXor : Option Bool → Option Bool → Option Bool

XOR the some-part of s into the some-part of t; blank on either side leaves t alone.

Equations

• QuantumQueryComplexity.optXor (some b) (some c) = some (b ^^ c)
• QuantumQueryComplexity.optXor x✝¹ x✝ = x✝¹

@[simp]

theorem QuantumQueryComplexity.optXor_some_some (b c : Bool) : optXor (some b) (some c) = some (b ^^ c)

@[simp]

theorem QuantumQueryComplexity.optXor_none (s : Option Bool) : optXor none s = none

@[simp]

theorem QuantumQueryComplexity.optXor_blank (t : Option Bool) : optXor t none = t

theorem QuantumQueryComplexity.optXor_optXor (t s : Option Bool) : optXor (optXor t s) s = t

The oracle

def QuantumQueryComplexity.xorOracleMap {ι W : Type} (a : ι → Bool) : QBasis ι Bool W → QBasis ι Bool W

The XOR oracle's action on the computational basis.

Equations

• QuantumQueryComplexity.xorOracleMap a (none, t, w) = (none, t, w)
• QuantumQueryComplexity.xorOracleMap a (some i, t, w) = (some i, QuantumQueryComplexity.optXor t (some (a i)), w)

@[simp]

theorem QuantumQueryComplexity.xorOracleMap_none {ι W : Type} (a : ι → Bool) (t : Option Bool) (w : W) : xorOracleMap a (none, t, w) = (none, t, w)

@[simp]

theorem QuantumQueryComplexity.xorOracleMap_some {ι W : Type} (a : ι → Bool) (i : ι) (t : Option Bool) (w : W) : xorOracleMap a (some i, t, w) = (some i, optXor t (some (a i)), w)

The XOR oracle reads the input only at the queried index.

theorem QuantumQueryComplexity.xorOracleMap_blank {ι W : Type} (a : ι → Bool) (i : ι) (w : W) : xorOracleMap a (some i, none, w) = (some i, none, w)

The blank answer is fixed: the XOR oracle, too, has an idle answer.

theorem QuantumQueryComplexity.xorOracleMap_involutive {ι W : Type} (a : ι → Bool) : Function.Involutive (xorOracleMap a)

def QuantumQueryComplexity.xorOraclePerm {ι W : Type} (a : ι → Bool) : Equiv.Perm (QBasis ι Bool W)

The XOR oracle as a permutation of the basis.

Equations

• QuantumQueryComplexity.xorOraclePerm a = Function.Involutive.toPerm (QuantumQueryComplexity.xorOracleMap a) ⋯

@[simp]

theorem QuantumQueryComplexity.xorOraclePerm_apply {ι W : Type} (a : ι → Bool) (p : QBasis ι Bool W) : (xorOraclePerm a) p = xorOracleMap a p

def QuantumQueryComplexity.xorOracleMat {ι W : Type} [DecidableEq ι] [DecidableEq W] (a : ι → Bool) : Matrix (QBasis ι Bool W) (QBasis ι Bool W) ℂ

The XOR oracle unitary.

Equations

• QuantumQueryComplexity.xorOracleMat a = QuantumQueryComplexity.qPerm (QuantumQueryComplexity.xorOraclePerm a)

theorem QuantumQueryComplexity.xorOracleMat_mem_unitaryGroup {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (a : ι → Bool) : xorOracleMat a ∈ Matrix.unitaryGroup (QBasis ι Bool W) ℂ

theorem QuantumQueryComplexity.xorOracleMat_mul_self {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (a : ι → Bool) : xorOracleMat a * xorOracleMat a = 1

Query = unquery, here too.

theorem QuantumQueryComplexity.xorOracleMat_mulVec_apply {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (a : ι → Bool) (ψ : QBasis ι Bool W → ℂ) (p : QBasis ι Bool W) : (xorOracleMat a).mulVec ψ p = ψ (xorOracleMap a p)

The XOR query model

QAlg carries no oracle; the state semantics does. These definitions mirror QAlg.state, ComputesWithErrorOn, QueryCounts, and qQueryOn with the XOR oracle substituted.

def QuantumQueryComplexity.xorState {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] {O : Type} (A : QAlg ι Bool O W) (a : ι → Bool) : ℕ → QBasis ι Bool W → ℂ

The state of A on input a after t XOR queries.

Equations

• QuantumQueryComplexity.xorState A a 0 = (A.step 0).mulVec A.init
• QuantumQueryComplexity.xorState A a t.succ = (A.step (t + 1)).mulVec ((QuantumQueryComplexity.xorOracleMat a).mulVec (QuantumQueryComplexity.xorState A a t))

@[simp]

theorem QuantumQueryComplexity.xorState_zero {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] {O : Type} (A : QAlg ι Bool O W) (a : ι → Bool) : xorState A a 0 = (A.step 0).mulVec A.init

@[simp]

theorem QuantumQueryComplexity.xorState_succ {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] {O : Type} (A : QAlg ι Bool O W) (a : ι → Bool) (t : ℕ) : xorState A a (t + 1) = (A.step (t + 1)).mulVec ((xorOracleMat a).mulVec (xorState A a t))

theorem QuantumQueryComplexity.xorState_isQState {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] {O : Type} (A : QAlg ι Bool O W) (a : ι → Bool) (t : ℕ) : IsQState (xorState A a t)

theorem QuantumQueryComplexity.xorState_eq_runWith {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] {O : Type} (A : QAlg ι Bool O W) (n : ℕ) (a : ι → Bool) (t : ℕ) : xorState A a t = (QRoutine.runWith (xorOracleMat a) { len := n, step := A.step, step_unitary := ⋯ } t).mulVec A.init

The bridge to the parametric run: the XOR state is runWith of the algorithm's step schedule, packaged with any length.

def QuantumQueryComplexity.XorComputesWithErrorOn {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] {O : Type} [DecidableEq O] {X : Type} (A : QAlg ι Bool O W) (q : ℕ) (read : X → ι → Bool) (f : X → O) (ε : ℝ) : Prop

A computes f on the promise read with error at most ε in q XOR queries.

Equations

• QuantumQueryComplexity.XorComputesWithErrorOn A q read f ε = ∀ (x : X), 1 - ε ≤ QuantumQueryComplexity.qProb A.readout (QuantumQueryComplexity.xorState A (read x) q) (f x)

def QuantumQueryComplexity.XorQueryCounts {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {X : Type} (read : X → ι → Bool) (f : X → O) (ε : ℝ) : Set ℕ

The achievable XOR-query counts.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumQueryComplexity.xorQQueryOn {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {X : Type} (read : X → ι → Bool) (f : X → O) (ε : ℝ) : ℕ

Quantum query complexity in the XOR-oracle model.

Equations

• QuantumQueryComplexity.xorQQueryOn read f ε = sInf (QuantumQueryComplexity.XorQueryCounts read f ε)

theorem QuantumQueryComplexity.mem_xorQueryCounts {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {X : Type} {read : X → ι → Bool} {f : X → O} {ε : ℝ} {q : ℕ} {W : Type} [Fintype W] [DecidableEq W] {A : QAlg ι Bool O W} (h : XorComputesWithErrorOn A q read f ε) : q ∈ XorQueryCounts read f ε

Folding the pair compiler: tuples, majority, and joint correctness

The k-fold iteration of Realizes.pair, and its two consumers:

• amplify — majority over k independent runs of a Boolean algorithm. The record statistics are an exact product, so the failure probability is the pattern count sum_prod_majority_le: at per-run error ε the amplified error is 2^k·ε^{⌈k/2⌉}; at the native ε = 1/16 this is ≤ 2^{-k}.
• exists_tuple_computes — B Boolean algorithms joined into one computing the tuple, with error ∑ εᵢ (the product of the diagonal probabilities, bounded by Weierstrass).

Costs add exactly throughout — the bank-swap compiler has no uncompute overhead.

The k-fold product realization over any decidable output type

def QuantumQueryComplexity.consEquiv (O : Type) (k : ℕ) : O × (Fin k → O) ≃ (Fin (k + 1) → O)

Prepending a coordinate to a record.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumQueryComplexity.realizes_zero_rec {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O : Type} [DecidableEq O] (read : X → ι → σ) : Realizes read 0 fun (x : X) (x_1 : Fin 0 → O) => 1

The trivial realization: no runs, the constant distribution 1 on the empty record.

theorem QuantumQueryComplexity.Realizes.foldRec {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O : Type} [DecidableEq O] {read : X → ι → σ} (k : ℕ) (q : Fin k → ℕ) (P : Fin k → X → O → ℝ) : (∀ (j : Fin k), Realizes read (q j) (P j)) → Realizes read (∑ j : Fin k, q j) fun (x : X) (y : Fin k → O) => ∏ j : Fin k, P j x (y j)

The k-fold product realization over any decidable output type: costs add, distributions multiply.

The base and the cons step

def QuantumQueryComplexity.finConsEquiv (k : ℕ) : Bool × (Fin k → Bool) ≃ (Fin (k + 1) → Bool)

Prepending a coordinate to a Boolean tuple.

Equations

• QuantumQueryComplexity.finConsEquiv k = QuantumQueryComplexity.consEquiv Bool k

theorem QuantumQueryComplexity.realizes_zero_tuple {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} (read : X → ι → σ) : Realizes read 0 fun (x : X) (x_1 : Fin 0 → Bool) => 1

The trivial realization: no runs, the constant distribution 1 on the empty tuple.

theorem QuantumQueryComplexity.Realizes.fold {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} {read : X → ι → σ} (k : ℕ) (q : Fin k → ℕ) (P : Fin k → X → Bool → ℝ) : (∀ (j : Fin k), Realizes read (q j) (P j)) → Realizes read (∑ j : Fin k, q j) fun (x : X) (y : Fin k → Bool) => ∏ j : Fin k, P j x (y j)

The k-fold product realization: costs add, distributions multiply.

theorem QuantumQueryComplexity.QAlg.sum_prob {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {O W : Type} [DecidableEq O] [Fintype O] [Fintype W] [DecidableEq W] (A : QAlg ι σ O W) (a : ι → σ) (t : ℕ) : ∑ o : O, A.prob a t o = 1

Probabilities sum to one.

theorem QuantumQueryComplexity.sum_pattern_prod {k : ℕ} (p : Bool → ℝ) : ∑ y : Fin k → Bool, ∏ j : Fin k, p (y j) = (∑ b : Bool, p b) ^ k

The full pattern sum of a product distribution is the product of the totals.

Majority amplification

def QuantumQueryComplexity.majVote (k : ℕ) (y : Fin k → Bool) : Bool

The majority vote.

Equations

• QuantumQueryComplexity.majVote k y = decide (k < 2 * {j : Fin k | y j = true}.card)

theorem QuantumQueryComplexity.le_card_wrong_of_majVote_ne {k : ℕ} {y : Fin k → Bool} {b : Bool} (h : majVote k y ≠ b) : (k + 1) / 2 ≤ {j : Fin k | y j ≠ b}.card

A wrong majority has at least ⌈k/2⌉ wrong votes.

theorem QuantumQueryComplexity.amplify {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} {read : X → ι → σ} {f : X → Bool} {q : ℕ} {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hex : ∃ (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (A : QAlg ι σ Bool W), ComputesWithErrorOn A q read f ε) (k : ℕ) : ∃ (W' : Type) (x : Fintype W') (x_1 : DecidableEq W') (A' : QAlg ι σ Bool W'), ComputesWithErrorOn A' (k * q) read f (2 ^ k * ε ^ ((k + 1) / 2))

Majority amplification. k independent runs of a Boolean algorithm with error ε ≤ 1 compute the same function with error 2^k·ε^{⌈k/2⌉}, at k times the cost.

Joining Boolean algorithms into a tuple

theorem QuantumQueryComplexity.one_sub_sum_le_prod {k : ℕ} (p e : Fin k → ℝ) (hp0 : ∀ (j : Fin k), 0 ≤ p j) (hp1 : ∀ (j : Fin k), p j ≤ 1) (he0 : ∀ (j : Fin k), 0 ≤ e j) (h : ∀ (j : Fin k), 1 - e j ≤ p j) : 1 - ∑ j : Fin k, e j ≤ ∏ j : Fin k, p j

Weierstrass: the product of near-one probabilities is near one.

theorem QuantumQueryComplexity.exists_tuple_computes {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X : Type} {read : X → ι → σ} {B : ℕ} {g : Fin B → X → Bool} {q : Fin B → ℕ} {ε : Fin B → ℝ} (hε0 : ∀ (i : Fin B), 0 ≤ ε i) (hex : ∀ (i : Fin B), ∃ (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (A : QAlg ι σ Bool W), ComputesWithErrorOn A (q i) read (g i) (ε i)) : ∃ (W' : Type) (x : Fintype W') (x_1 : DecidableEq W') (A' : QAlg ι σ (Fin B → Bool) W'), ComputesWithErrorOn A' (∑ i : Fin B, q i) read (fun (x : X) (i : Fin B) => g i x) (∑ i : Fin B, ε i)

The tuple compiler: B Boolean algorithms joined into one computing the tuple function, at the sum of the costs and the sum of the errors.

Oracle simulation: transposition ↔ XOR, at two queries per query

The model-equivalence theorem for Boolean input alphabets. Each direction is one two-query gadget on a clean-ancilla encoded subspace (embedReg with an Option Bool ancilla register), compiled over whole routines at exactly 2·R.len queries, and exported as a QueryCounts translation:

q ∈ XorQueryCounts read f ε  →  2q ∈ QueryCounts read f ε
q ∈ QueryCounts read f ε     →  2q ∈ XorQueryCounts read f ε

with the complexity inequalities

qQueryOn read f ε ≤ 2 · xorQQueryOn read f ε
xorQQueryOn read f ε ≤ 2 · qQueryOn read f ε.

The gadgets. With ancilla v, answer t:

• transposition simulates XOR (xorGadget, clean value ⊥): swap t ↔ v, query (⊥ ↦ a i), XOR the answer into the ancilla, unquery, swap back — swap · O · xorInto · O · swap;
• XOR simulates transposition (transGadget, clean value some false): swap, query (some false ↦ some (a i)), controlled-swap ⊥ ↔ some v on the ancilla where v is the answer's value, unquery, swap back — swap · Oˣ · ctrlSwap · Oˣ · swap.

Both middle unitaries are input-independent basis permutations; the controlled swap is additionally controlled on the index register being active, which is what keeps the idle sector exactly fixed. Off the clean sector each gadget moves the ancilla away from the clean value, so the encoded-subspace statements hold with no side condition.

The compilers are compositional (QRoutine.comp + ofUnitary of lifted steps, exactly like selectPowers), with comp_run sequencing the standard side and comp_runWith/xorRun (from SourceQuantumRunWith) the XOR side.

Boolean specifically: for an arbitrary alphabet there is no canonical XOR directly on σ without choosing a group structure on σ; the transposition oracle is the alphabet-free primitive, which is why it is this development's native model. The upstream construction (upstream OneHotSimulation.lean) handles arbitrary finite alphabets by XORing the letter's one-hot encoding into a Hot σ register, with the same two-queries-per-query gadget pattern as here.

The run in the XOR model, packaged

def QuantumQueryComplexity.QRoutine.xorRun {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) (a : ι → Bool) : Matrix (QBasis ι Bool W) (QBasis ι Bool W) ℂ

The operator implemented by R against the XOR oracle.

Equations

• R.xorRun a = QuantumQueryComplexity.QRoutine.runWith (QuantumQueryComplexity.xorOracleMat a) R R.len

theorem QuantumQueryComplexity.QRoutine.comp_xorRun {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R S : QRoutine ι Bool W) (a : ι → Bool) : (R.comp S).xorRun a = S.xorRun a * R.xorRun a

@[simp]

theorem QuantumQueryComplexity.QRoutine.ofUnitary_xorRun {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (U : Matrix (QBasis ι Bool W) (QBasis ι Bool W) ℂ) (hU : U ∈ Matrix.unitaryGroup (QBasis ι Bool W) ℂ) (a : ι → Bool) : (ofUnitary U hU).xorRun a = U

The gadget permutations

All on QBasis ι Bool (Option Bool × W): index, answer, ancilla, workspace.

def QuantumQueryComplexity.swapAncMap {ι W : Type} : QBasis ι Bool (Option Bool × W) → QBasis ι Bool (Option Bool × W)

Swap the answer register with the ancilla.

Equations

• QuantumQueryComplexity.swapAncMap (idx, t, v, w) = (idx, v, t, w)

@[simp]

theorem QuantumQueryComplexity.swapAncMap_apply {ι W : Type} (idx : Option ι) (t v : Option Bool) (w : W) : swapAncMap (idx, t, v, w) = (idx, v, t, w)

theorem QuantumQueryComplexity.swapAncMap_involutive {ι W : Type} : Function.Involutive swapAncMap

def QuantumQueryComplexity.xorIntoMap {ι W : Type} : QBasis ι Bool (Option Bool × W) → QBasis ι Bool (Option Bool × W)

XOR the answer register's value into the ancilla.

Equations

• QuantumQueryComplexity.xorIntoMap (idx, t, v, w) = (idx, t, QuantumQueryComplexity.optXor v t, w)

@[simp]

theorem QuantumQueryComplexity.xorIntoMap_apply {ι W : Type} (idx : Option ι) (s t : Option Bool) (w : W) : xorIntoMap (idx, s, t, w) = (idx, s, optXor t s, w)

theorem QuantumQueryComplexity.xorIntoMap_involutive {ι W : Type} : Function.Involutive xorIntoMap

def QuantumQueryComplexity.ctrlSwapMap {ι W : Type} : QBasis ι Bool (Option Bool × W) → QBasis ι Bool (Option Bool × W)

On an active index with answer some v: swap ⊥ ↔ some v in the ancilla. Controlled on the index being active, so the idle sector is exactly fixed.

Equations

• QuantumQueryComplexity.ctrlSwapMap (some i, some v, t, w) = (some i, some v, (Equiv.swap none (some v)) t, w)
• QuantumQueryComplexity.ctrlSwapMap x✝ = x✝

@[simp]

theorem QuantumQueryComplexity.ctrlSwapMap_active {ι W : Type} (i : ι) (v : Bool) (t : Option Bool) (w : W) : ctrlSwapMap (some i, some v, t, w) = (some i, some v, (Equiv.swap none (some v)) t, w)

@[simp]

theorem QuantumQueryComplexity.ctrlSwapMap_idle {ι W : Type} (s t : Option Bool) (w : W) : ctrlSwapMap (none, s, t, w) = (none, s, t, w)

@[simp]

theorem QuantumQueryComplexity.ctrlSwapMap_blank {ι W : Type} (i : ι) (t : Option Bool) (w : W) : ctrlSwapMap (some i, none, t, w) = (some i, none, t, w)

theorem QuantumQueryComplexity.ctrlSwapMap_involutive {ι W : Type} : Function.Involutive ctrlSwapMap

The gadget unitaries

def QuantumQueryComplexity.swapAncMat {ι W : Type} [DecidableEq ι] [DecidableEq W] : Matrix (QBasis ι Bool (Option Bool × W)) (QBasis ι Bool (Option Bool × W)) ℂ

The answer–ancilla swap.

Equations

• QuantumQueryComplexity.swapAncMat = QuantumQueryComplexity.qPerm (Function.Involutive.toPerm QuantumQueryComplexity.swapAncMap ⋯)

theorem QuantumQueryComplexity.swapAncMat_mem_unitaryGroup {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] : swapAncMat ∈ Matrix.unitaryGroup (QBasis ι Bool (Option Bool × W)) ℂ

theorem QuantumQueryComplexity.swapAncMat_mulVec_apply {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (ψ : QBasis ι Bool (Option Bool × W) → ℂ) (p : QBasis ι Bool (Option Bool × W)) : swapAncMat.mulVec ψ p = ψ (swapAncMap p)

def QuantumQueryComplexity.xorIntoMat {ι W : Type} [DecidableEq ι] [DecidableEq W] : Matrix (QBasis ι Bool (Option Bool × W)) (QBasis ι Bool (Option Bool × W)) ℂ

The XOR-into-the-ancilla unitary.

Equations

• QuantumQueryComplexity.xorIntoMat = QuantumQueryComplexity.qPerm (Function.Involutive.toPerm QuantumQueryComplexity.xorIntoMap ⋯)

theorem QuantumQueryComplexity.xorIntoMat_mem_unitaryGroup {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] : xorIntoMat ∈ Matrix.unitaryGroup (QBasis ι Bool (Option Bool × W)) ℂ

theorem QuantumQueryComplexity.xorIntoMat_mulVec_apply {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (ψ : QBasis ι Bool (Option Bool × W) → ℂ) (p : QBasis ι Bool (Option Bool × W)) : xorIntoMat.mulVec ψ p = ψ (xorIntoMap p)

def QuantumQueryComplexity.ctrlSwapMat {ι W : Type} [DecidableEq ι] [DecidableEq W] : Matrix (QBasis ι Bool (Option Bool × W)) (QBasis ι Bool (Option Bool × W)) ℂ

The controlled-swap unitary.

Equations

• QuantumQueryComplexity.ctrlSwapMat = QuantumQueryComplexity.qPerm (Function.Involutive.toPerm QuantumQueryComplexity.ctrlSwapMap ⋯)

theorem QuantumQueryComplexity.ctrlSwapMat_mem_unitaryGroup {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] : ctrlSwapMat ∈ Matrix.unitaryGroup (QBasis ι Bool (Option Bool × W)) ℂ

theorem QuantumQueryComplexity.ctrlSwapMat_mulVec_apply {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (ψ : QBasis ι Bool (Option Bool × W) → ℂ) (p : QBasis ι Bool (Option Bool × W)) : ctrlSwapMat.mulVec ψ p = ψ (ctrlSwapMap p)

The two gadgets

def QuantumQueryComplexity.xorGadget {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] : QRoutine ι Bool (Option Bool × W)

Transposition simulates XOR: two physical queries.

Equations

• QuantumQueryComplexity.xorGadget = { len := 2, step := fun (t : ℕ) => if t = 1 then QuantumQueryComplexity.xorIntoMat else QuantumQueryComplexity.swapAncMat, step_unitary := ⋯ }

@[simp]

theorem QuantumQueryComplexity.xorGadget_len {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] : xorGadget.len = 2

def QuantumQueryComplexity.transGadget {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] : QRoutine ι Bool (Option Bool × W)

XOR simulates transposition: two physical queries.

Equations

• QuantumQueryComplexity.transGadget = { len := 2, step := fun (t : ℕ) => if t = 1 then QuantumQueryComplexity.ctrlSwapMat else QuantumQueryComplexity.swapAncMat, step_unitary := ⋯ }

@[simp]

theorem QuantumQueryComplexity.transGadget_len {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] : transGadget.len = 2

theorem QuantumQueryComplexity.xorGadget_run {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (a : ι → Bool) (ψ : QBasis ι Bool W → ℂ) : (xorGadget.run a).mulVec (embedReg none ψ) = embedReg none ((xorOracleMat a).mulVec ψ)

The XOR gadget's action on the clean-ancilla sector is exactly one XOR query.

theorem QuantumQueryComplexity.transGadget_xorRun {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (a : ι → Bool) (ψ : QBasis ι Bool W → ℂ) : (transGadget.xorRun a).mulVec (embedReg (some false) ψ) = embedReg (some false) ((oracleMat a).mulVec ψ)

The transposition gadget's action on the clean-ancilla sector is exactly one transposition query, under XOR semantics.

The compilers

def QuantumQueryComplexity.simXorUpto {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) : ℕ → QRoutine ι Bool (Option Bool × W)

Compile the first t XOR queries of a schedule into the transposition model: lifted steps, one xorGadget per query.

Equations

• One or more equations did not get rendered due to their size.
• QuantumQueryComplexity.simXorUpto R 0 = QuantumQueryComplexity.QRoutine.ofUnitary (QuantumQueryComplexity.liftReg (Option Bool) (R.step 0)) ⋯

@[simp]

theorem QuantumQueryComplexity.simXorUpto_len {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) (t : ℕ) : (simXorUpto R t).len = 2 * t

theorem QuantumQueryComplexity.simXorUpto_run {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) (a : ι → Bool) (t : ℕ) (ψ : QBasis ι Bool W → ℂ) : ((simXorUpto R t).run a).mulVec (embedReg none ψ) = embedReg none ((QRoutine.runWith (xorOracleMat a) R t).mulVec ψ)

def QuantumQueryComplexity.simXor {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) : QRoutine ι Bool (Option Bool × W)

The compiled XOR schedule: 2·R.len transposition queries.

Equations

• QuantumQueryComplexity.simXor R = QuantumQueryComplexity.simXorUpto R R.len

@[simp]

theorem QuantumQueryComplexity.simXor_len {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) : (simXor R).len = 2 * R.len

theorem QuantumQueryComplexity.simXor_run {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) (a : ι → Bool) (ψ : QBasis ι Bool W → ℂ) : ((simXor R).run a).mulVec (embedReg none ψ) = embedReg none ((QRoutine.runWith (xorOracleMat a) R R.len).mulVec ψ)

def QuantumQueryComplexity.simTransUpto {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) : ℕ → QRoutine ι Bool (Option Bool × W)

Compile the first t transposition queries of a schedule into the XOR model: lifted steps, one transGadget per query.

Equations

• One or more equations did not get rendered due to their size.
• QuantumQueryComplexity.simTransUpto R 0 = QuantumQueryComplexity.QRoutine.ofUnitary (QuantumQueryComplexity.liftReg (Option Bool) (R.step 0)) ⋯

@[simp]

theorem QuantumQueryComplexity.simTransUpto_len {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) (t : ℕ) : (simTransUpto R t).len = 2 * t

theorem QuantumQueryComplexity.simTransUpto_xorRun {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) (a : ι → Bool) (t : ℕ) (ψ : QBasis ι Bool W → ℂ) : ((simTransUpto R t).xorRun a).mulVec (embedReg (some false) ψ) = embedReg (some false) ((R.runUpto a t).mulVec ψ)

def QuantumQueryComplexity.simTrans {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) : QRoutine ι Bool (Option Bool × W)

The compiled transposition schedule: 2·R.len XOR queries.

Equations

• QuantumQueryComplexity.simTrans R = QuantumQueryComplexity.simTransUpto R R.len

@[simp]

theorem QuantumQueryComplexity.simTrans_len {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) : (simTrans R).len = 2 * R.len

theorem QuantumQueryComplexity.simTrans_xorRun {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] (R : QRoutine ι Bool W) (a : ι → Bool) (ψ : QBasis ι Bool W → ℂ) : ((simTrans R).xorRun a).mulVec (embedReg (some false) ψ) = embedReg (some false) ((R.run a).mulVec ψ)

Transporting states, readouts, and probabilities

theorem QuantumQueryComplexity.isQState_embedReg {ι W : Type} [Fintype ι] [Fintype W] {σ V : Type} [Fintype σ] [Fintype V] [DecidableEq V] (v : V) {ψ : QBasis ι σ W → ℂ} (hψ : IsQState ψ) : IsQState (embedReg v ψ)

def QuantumQueryComplexity.stripReadout {ι W σ V O : Type} (r : QBasis ι σ W → O) : QBasis ι σ (V × W) → O

Read the underlying registers, ignoring the ancilla.

Equations

• QuantumQueryComplexity.stripReadout r p = r (p.1, p.2.1, p.2.2.2)

theorem QuantumQueryComplexity.qRestrict_stripReadout_embedReg {ι W σ V O : Type} [DecidableEq V] [DecidableEq O] (r : QBasis ι σ W → O) (v : V) (o : O) (χ : QBasis ι σ W → ℂ) : qRestrict (stripReadout r) o (embedReg v χ) = embedReg v (qRestrict r o χ)

theorem QuantumQueryComplexity.qProb_stripReadout_embedReg {ι W : Type} [Fintype ι] [Fintype W] {σ V O : Type} [Fintype σ] [Fintype V] [DecidableEq V] [DecidableEq O] (r : QBasis ι σ W → O) (v : V) (o : O) (χ : QBasis ι σ W → ℂ) : qProb (stripReadout r) (embedReg v χ) o = qProb r χ o

Measuring through the ancilla changes nothing.

The state bridges

theorem QuantumQueryComplexity.state_eq_runUpto {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] {O : Type} (A : QAlg ι Bool O W) (n : ℕ) (a : ι → Bool) (t : ℕ) : A.state a t = ({ len := n, step := A.step, step_unitary := ⋯ }.runUpto a t).mulVec A.init

The standard state is the run of the algorithm's own schedule.

theorem QuantumQueryComplexity.xorState_toAlg {ι W : Type} [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W] {O : Type} (R : QRoutine ι Bool W) (init : QBasis ι Bool W → ℂ) (hinit : IsQState init) (r : QBasis ι Bool W → O) (a : ι → Bool) (t : ℕ) : xorState (R.toAlg init hinit r) a t = (QRoutine.runWith (xorOracleMat a) R t).mulVec init

The XOR state of a packaged routine is its parametric run.

The QueryCounts translations

theorem QuantumQueryComplexity.two_mul_mem_queryCounts_of_xor {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {X : Type} {read : X → ι → Bool} {f : X → O} {ε : ℝ} {q : ℕ} (hq : q ∈ XorQueryCounts read f ε) : 2 * q ∈ QueryCounts read f ε

The transposition model simulates the XOR model at a factor of two: every achievable XOR query count doubles into the native model.

theorem QuantumQueryComplexity.two_mul_mem_xorQueryCounts_of_std {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {X : Type} {read : X → ι → Bool} {f : X → O} {ε : ℝ} {q : ℕ} (hq : q ∈ QueryCounts read f ε) : 2 * q ∈ XorQueryCounts read f ε

The XOR model simulates the transposition model at a factor of two.

The complexity comparison

theorem QuantumQueryComplexity.xorQueryCounts_nonempty {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {X : Type} [Nonempty O] {read : X → ι → Bool} {f : X → O} {ε : ℝ} (hdet : ∀ (x y : X), read x = read y → f x = f y) (hε0 : 0 ≤ ε) [Finite X] : (XorQueryCounts read f ε).Nonempty

theorem QuantumQueryComplexity.qQueryOn_le_two_mul_xorQQueryOn {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {X : Type} [Nonempty O] {read : X → ι → Bool} {f : X → O} {ε : ℝ} (hdet : ∀ (x y : X), read x = read y → f x = f y) (hε0 : 0 ≤ ε) [Finite X] : qQueryOn read f ε ≤ 2 * xorQQueryOn read f ε

Model equivalence, one direction: standard complexity is at most twice the XOR complexity.

theorem QuantumQueryComplexity.xorQQueryOn_le_two_mul_qQueryOn {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {X : Type} [Nonempty O] {read : X → ι → Bool} {f : X → O} {ε : ℝ} (hdet : ∀ (x y : X), read x = read y → f x = f y) (hε0 : 0 ≤ ε) [Finite X] : xorQQueryOn read f ε ≤ 2 * qQueryOn read f ε

Model equivalence, the other direction: XOR complexity is at most twice the standard complexity.

Finite outputs by bit encoding

A finite output type O with m values is encoded in B = ⌈log₂ m⌉ = Nat.clog 2 m Boolean bits through Fintype.equivFin; each bit of f is a post-composition of f, so on the adversary side it costs nothing (advPMOn_comp_le). Given a 1/16-algorithm for each bit, the assembly is:

• amplify each bit to error (1/4)ᵗ with 2t majority rounds (amplify; the exponent arithmetic is 2^{2t}·(1/16)^t = (1/4)^t);
• join the B amplified bits into the tuple (exists_tuple_computes), error B·(1/4)ᵗ, cost ∑ᵢ 2t·qᵢ;
• decode by post-composing the readout with the inverse encoding (ComputesWithErrorOn.postcomp from SourceQuantumPostcomp — the fibre sum only grows the correct outcome's probability).

exists_decode_computes is the generic assembly; the final theorem against advPMOn lives in SourceQuantumCharacterization, which supplies the per-bit algorithms from the promise-Boolean characterization.

The bit encoding

def QuantumQueryComplexity.encBits (O : Type) [Fintype O] : ℕ

The number of encoding bits: ⌈log₂ |O|⌉.

Equations

• QuantumQueryComplexity.encBits O = Nat.clog 2 (Fintype.card O)

noncomputable def QuantumQueryComplexity.encBit {O : Type} [Fintype O] (o : O) (i : Fin (encBits O)) : Bool

Bit i of the encoded value.

Equations

• QuantumQueryComplexity.encBit o i = (↑((Fintype.equivFin O) o)).testBit ↑i

theorem QuantumQueryComplexity.encBit_injective {O : Type} [Fintype O] {o o' : O} (h : ∀ (i : Fin (encBits O)), encBit o i = encBit o' i) : o = o'

The encoding is injective: values are below 2^B, so the first B bits determine them.

noncomputable def QuantumQueryComplexity.encDecode {O : Type} [Fintype O] [Nonempty O] (y : Fin (encBits O) → Bool) : O

The decoder: the (unique) value with the given bits, if any.

Equations

• QuantumQueryComplexity.encDecode y = if h : ∃ (o : O), (fun (i : Fin (QuantumQueryComplexity.encBits O)) => QuantumQueryComplexity.encBit o i) = y then h.choose else Classical.arbitrary O

theorem QuantumQueryComplexity.encDecode_encBit {O : Type} [Fintype O] [Nonempty O] (o : O) : (encDecode fun (i : Fin (encBits O)) => encBit o i) = o

The assembly

theorem QuantumQueryComplexity.exists_decode_computes {ι σ : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] {X O : Type} [Fintype O] [DecidableEq O] [Nonempty O] {read : X → ι → σ} {f : X → O} {qb : Fin (encBits O) → ℕ} (t : ℕ) (halg : ∀ (i : Fin (encBits O)), ∃ (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (A : QAlg ι σ Bool W), ComputesWithErrorOn A (qb i) read (fun (x : X) => encBit (f x) i) (1 / 16)) : ∃ (W' : Type) (x : Fintype W') (x_1 : DecidableEq W') (A' : QAlg ι σ O W'), ComputesWithErrorOn A' (∑ i : Fin (encBits O), 2 * t * qb i) read f (↑(encBits O) * (1 / 4) ^ t)

The finite-output assembly: given a 1/16-algorithm for each encoding bit of f, there is an algorithm for f itself with error B·(1/4)ᵗ at cost ∑ᵢ 2t·qᵢ.