Spectral detection and coherent state conversion

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

The chord form of a unitary

A spike for the spectral layer. Spectral windows for a unitary U are usually stated with Complex.arg of its eigenvalues, which drags in branch cuts and trigonometry. The chord distance ‖1 - z‖ avoids that, and it has a matrix avatar that avoids diagonalizing U at all:

chordSq U = (1 - U)ᴴ (1 - U).

This matrix is Hermitian (chordSq_conjTranspose) and positive semidefinite, so Mathlib's spectral theory for Hermitian matrices applies directly — no eigenbasis for a general unitary is needed. Its quadratic form is exactly the squared chord distance (qNormSq_sub_mulVec), so "the eigenvalues of chordSq U are at most Δ²" is precisely "the chord-distance window of threshold Δ²" (equivalently of radius |Δ| — nothing here assumes Δ nonnegative).

Two facts make one Hermitian decomposition serve both halves of the phase detector:

• chordSq_commute — chordSq U commutes with U, so U preserves each of its spectral subspaces. This is what removes the need for simultaneous diagonalization: the windows are defined by a Hermitian matrix, and U acts within them.
• one_sub_mul_geom_sum — (1 - U) ∑_{t<T} U^t = 1 - U^T, the telescoping identity behind the uniform-clock estimate on the far window.

On a unitary the chord form collapses to 2 - U - Uᴴ, which is where both facts come from.

def QuantumQueryComplexity.chordSq {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) : Matrix H H ℂ

The chord form of U: (1 - U)ᴴ (1 - U).

Equations

• QuantumQueryComplexity.chordSq U = (1 - U).conjTranspose * (1 - U)

theorem QuantumQueryComplexity.chordSq_conjTranspose {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) : (chordSq U).conjTranspose = chordSq U

The chord form is Hermitian — stated as the raw identity, so this section needs no extra Mathlib import.

theorem QuantumQueryComplexity.qNormSq_sub_mulVec {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (ψ : H → ℂ) : qNormSq ((1 - U).mulVec ψ) = (qInner ψ ((chordSq U).mulVec ψ)).re

The quadratic form of chordSq is the squared chord distance. This is what makes a spectral window of chordSq U a chord-distance window.

theorem QuantumQueryComplexity.chordSq_eq_of_unitary {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) : chordSq U = 1 + 1 - U - U.conjTranspose

On a unitary the chord form collapses.

theorem QuantumQueryComplexity.chordSq_commute {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) : chordSq U * U = U * chordSq U

The chord form commutes with the unitary, so U preserves each spectral subspace of chordSq U. No simultaneous diagonalization is needed.

theorem QuantumQueryComplexity.chordSq_mulVec_eq_zero_iff {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (ψ : H → ℂ) : (chordSq U).mulVec ψ = 0 ↔ (1 - U).mulVec ψ = 0

The chord form kills exactly what 1 - U kills.

theorem QuantumQueryComplexity.one_sub_qRefl_mul_qRefl_mulVec {H : Type} [Fintype H] [DecidableEq H] {P L : Matrix H H ℂ} {w : H → ℂ} (hw : L.mulVec w = 0) : (1 - qRefl P * qRefl L).mulVec w = 2 • P.mulVec w

The core identity of the effective gap. If L (the plan's Λ) kills w, the product of the two reflections moves w by exactly 2 P w (the plan's 2 Π w). Π is reserved notation in Lean, hence the renaming.

theorem QuantumQueryComplexity.one_sub_mul_geom_sum {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (T : ℕ) : (1 - U) * ∑ t ∈ Finset.range T, U ^ t = 1 - U ^ T

The telescoping identity behind the uniform clock.

Orthogonal projectors and reflections, as raw matrices

A spike, to fix the representation before the witness construction.

The upper bound reflects about the span of a finite family of vectors coming from a DualPair. Rather than build projectors by hand, construct the subspace in EuclideanSpace ℂ H, take Mathlib's Submodule.starProjection, and carry it back to a raw Matrix H H ℂ.

The transport is Matrix.toEuclideanCLM, which is a star-algebra equivalence — not merely a linear one. That single fact is what makes this representation the right one: idempotence and self-adjointness of the projector come from map_mul and map_star, with no matrix computation at all, and IsQProjector (hence qRefl, already proved unitary and involutive) follows immediately.

What the spike establishes

• subProj_mulVec — the raw action: subProj K *ᵥ ψ is K.starProjection applied to ψ, read back through WithLp.
• subProj_mulVec_of_mem / subProj_mulVec_of_mem_orthogonal — the fixed space and the killed space, the two characterizations a reflection argument actually uses.
• isQProjector_subProj, and hence subRefl with subRefl_mul_self, subRefl_mem_unitaryGroup, subRefl_mulVec_of_mem (+ψ) and subRefl_mulVec_of_mem_orthogonal (-ψ).
• spanProj / spanRefl — the finite-span case, which is the one the witness construction needs.

The membership side conditions are stated in EuclideanSpace (WithLp.toLp 2 ψ ∈ K) rather than raw, deliberately: that is where the span of a family of vectors is easy to reason about, and WithLp.toLp is an equivalence, so nothing is lost.

The projector

noncomputable def QuantumQueryComplexity.subProj {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] : Matrix H H ℂ

The orthogonal projector onto K, as a raw matrix.

Equations

• QuantumQueryComplexity.subProj K = Matrix.toEuclideanCLM.symm K.starProjection

theorem QuantumQueryComplexity.toEuclideanCLM_subProj {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] : Matrix.toEuclideanCLM (subProj K) = K.starProjection

theorem QuantumQueryComplexity.subProj_mulVec {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] (ψ : H → ℂ) : WithLp.toLp 2 ((subProj K).mulVec ψ) = K.starProjection (WithLp.toLp 2 ψ)

The raw action of the projector.

theorem QuantumQueryComplexity.isQProjector_subProj {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] : IsQProjector (subProj K)

It is an orthogonal projector. Both halves come from Matrix.toEuclideanCLM being a star-algebra equivalence.

theorem QuantumQueryComplexity.subProj_mulVec_of_mem {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] {ψ : H → ℂ} (h : WithLp.toLp 2 ψ ∈ K) : (subProj K).mulVec ψ = ψ

The fixed space.

theorem QuantumQueryComplexity.subProj_mulVec_eq_self_iff {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] (ψ : H → ℂ) : (subProj K).mulVec ψ = ψ ↔ WithLp.toLp 2 ψ ∈ K

The fixed space, as an iff. What a witness construction has to hit: being fixed by the projector is membership.

theorem QuantumQueryComplexity.subProj_mulVec_of_mem_orthogonal {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] {ψ : H → ℂ} (h : WithLp.toLp 2 ψ ∈ Kᗮ) : (subProj K).mulVec ψ = 0

The killed space.

The reflection

noncomputable def QuantumQueryComplexity.subRefl {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] : Matrix H H ℂ

The reflection about K.

Equations

• QuantumQueryComplexity.subRefl K = QuantumQueryComplexity.qRefl (QuantumQueryComplexity.subProj K)

theorem QuantumQueryComplexity.subRefl_mem_unitaryGroup {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] : subRefl K ∈ Matrix.unitaryGroup H ℂ

theorem QuantumQueryComplexity.subRefl_mul_self {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] : subRefl K * subRefl K = 1

theorem QuantumQueryComplexity.subRefl_mulVec {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] (ψ : H → ℂ) : (subRefl K).mulVec ψ = 2 • (subProj K).mulVec ψ - ψ

theorem QuantumQueryComplexity.subRefl_mulVec_of_mem {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] {ψ : H → ℂ} (h : WithLp.toLp 2 ψ ∈ K) : (subRefl K).mulVec ψ = ψ

The reflection fixes K.

theorem QuantumQueryComplexity.subRefl_mulVec_of_mem_orthogonal {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] {ψ : H → ℂ} (h : WithLp.toLp 2 ψ ∈ Kᗮ) : (subRefl K).mulVec ψ = -ψ

The reflection negates Kᗮ.

The orthogonal complement

The sign matters. The plan's Λ is the projector onto span{ψₓ}ᗮ, and its reflection is minus the reflection about the span. A global sign shifts every eigenphase by π, so it cannot be dropped when the operator is fed to controlled phase detection.

theorem QuantumQueryComplexity.subProj_orthogonal {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] : subProj Kᗮ = 1 - subProj K

The projector onto the orthogonal complement.

theorem QuantumQueryComplexity.subRefl_orthogonal {H : Type} [Fintype H] [DecidableEq H] (K : Submodule ℂ (EuclideanSpace ℂ H)) [K.HasOrthogonalProjection] : subRefl Kᗮ = -subRefl K

The reflection about the complement is minus the reflection about the subspace. This is the sign that must not be dropped.

Finite spans

The case the witness construction needs: reflect about the span of a finite family of raw vectors.

noncomputable def QuantumQueryComplexity.rawSpan {H ι' : Type} (v : ι' → H → ℂ) : Submodule ℂ (EuclideanSpace ℂ H)

The subspace spanned by a finite family of raw vectors.

Equations

• QuantumQueryComplexity.rawSpan v = Submodule.span ℂ (Set.range fun (i : ι') => WithLp.toLp 2 (v i))

theorem QuantumQueryComplexity.mem_rawSpan_orthogonal_iff {H : Type} [Fintype H] {ι' : Type} (v : ι' → H → ℂ) (ψ : H → ℂ) : WithLp.toLp 2 ψ ∈ (rawSpan v)ᗮ ↔ ∀ (i : ι'), qInner (v i) ψ = 0

Orthogonality to a span is orthogonality to its generators. This is the form a witness construction can actually verify: one inner product per generator, no spans.

noncomputable def QuantumQueryComplexity.spanProj {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) : Matrix H H ℂ

The projector onto the span of a finite family.

Equations

• QuantumQueryComplexity.spanProj v = QuantumQueryComplexity.subProj (QuantumQueryComplexity.rawSpan v)

noncomputable def QuantumQueryComplexity.spanRefl {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) : Matrix H H ℂ

The reflection about the span of a finite family.

Equations

• QuantumQueryComplexity.spanRefl v = QuantumQueryComplexity.subRefl (QuantumQueryComplexity.rawSpan v)

theorem QuantumQueryComplexity.isQProjector_spanProj {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) : IsQProjector (spanProj v)

theorem QuantumQueryComplexity.spanRefl_mem_unitaryGroup {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) : spanRefl v ∈ Matrix.unitaryGroup H ℂ

theorem QuantumQueryComplexity.spanRefl_mul_self {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) : spanRefl v * spanRefl v = 1

theorem QuantumQueryComplexity.spanProj_orthogonal {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) : subProj (rawSpan v)ᗮ = 1 - spanProj v

The projector onto the complement of a span.

theorem QuantumQueryComplexity.spanRefl_orthogonal {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) : subRefl (rawSpan v)ᗮ = -spanRefl v

The reflection about the complement of a span, with its sign.

theorem QuantumQueryComplexity.spanProj_mulVec_self {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) (i : ι') : (spanProj v).mulVec (v i) = v i

Each spanning vector is fixed by the projector.

theorem QuantumQueryComplexity.spanRefl_mulVec_self {H : Type} [Fintype H] [DecidableEq H] {ι' : Type} (v : ι' → H → ℂ) (i : ι') : (spanRefl v).mulVec (v i) = v i

Each spanning vector is fixed by the reflection.

The chord-distance spectral windows

The near and far windows of a unitary U at threshold Δ² — equivalently chord radius |Δ|, since Δ is not assumed nonnegative anywhere — as the spectral projectors of the Hermitian matrix chordSq U = (1-U)ᴴ(1-U):

chordNearProj U Δ = cfc (fun l => if l ≤ Δ² then 1 else 0) (chordSq U), chordFarProj U Δ = 1 - chordNearProj U Δ.

Two things make this work where diagonalizing a general unitary would not:

• The discontinuous mask is legitimate. Mathlib's cfc needs the function continuous only on the spectrum, and a matrix has finite real spectrum (Matrix.finite_real_spectrum), which is discrete — so Set.Finite.continuousOn discharges every side condition. Nothing here is an approximation of an indicator; it is the indicator.
• U preserves the windows. chordSq_commute says U commutes with chordSq U, and Commute.cfc_real upgrades that to commuting with any cfc of it. No simultaneous diagonalization, and no eigenbasis for U.

theorem QuantumQueryComplexity.IsQProjector.one_sub {H : Type} [Fintype H] [DecidableEq H] {P : Matrix H H ℂ} (hP : IsQProjector P) : IsQProjector (1 - P)

The complement of a projector is a projector.

theorem QuantumQueryComplexity.isSelfAdjoint_chordSq {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) : IsSelfAdjoint (chordSq U)

noncomputable def QuantumQueryComplexity.chordMask (Δ : ℝ) : ℝ → ℝ

The near-window mask. Discontinuous on ℝ, but that is irrelevant: it is only ever restricted to a finite spectrum.

Equations

• QuantumQueryComplexity.chordMask Δ l = if l ≤ Δ ^ 2 then 1 else 0

theorem QuantumQueryComplexity.continuousOn_chordMask {H : Type} [Fintype H] [DecidableEq H] (A : Matrix H H ℂ) (Δ : ℝ) : ContinuousOn (chordMask Δ) (spectrum ℝ A)

theorem QuantumQueryComplexity.chordMask_mul_self (Δ l : ℝ) : chordMask Δ l * chordMask Δ l = chordMask Δ l

noncomputable def QuantumQueryComplexity.chordNearProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : Matrix H H ℂ

The near window: the spectral projector of chordSq U for eigenvalues at most Δ², i.e. chord distance at most |Δ|.

Equations

• QuantumQueryComplexity.chordNearProj U Δ = cfc (QuantumQueryComplexity.chordMask Δ) (QuantumQueryComplexity.chordSq U)

noncomputable def QuantumQueryComplexity.chordFarProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : Matrix H H ℂ

The far window.

Equations

• QuantumQueryComplexity.chordFarProj U Δ = 1 - QuantumQueryComplexity.chordNearProj U Δ

theorem QuantumQueryComplexity.isQProjector_chordNearProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : IsQProjector (chordNearProj U Δ)

theorem QuantumQueryComplexity.isQProjector_chordFarProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : IsQProjector (chordFarProj U Δ)

theorem QuantumQueryComplexity.chordNearProj_commute {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) (Δ : ℝ) : chordNearProj U Δ * U = U * chordNearProj U Δ

U preserves the near window.

theorem QuantumQueryComplexity.chordFarProj_commute {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) (Δ : ℝ) : chordFarProj U Δ * U = U * chordFarProj U Δ

U preserves the far window.

Quadratic forms

The bound below is an inequality between quadratic forms, so these are the manipulations it needs. Nothing here is specific to the chord form.

theorem QuantumQueryComplexity.qInner_add_mulVec {H : Type} [Fintype H] (M M' : Matrix H H ℂ) (x : H → ℂ) : qInner x ((M + M').mulVec x) = qInner x (M.mulVec x) + qInner x (M'.mulVec x)

theorem QuantumQueryComplexity.qInner_smul_mulVec {H : Type} [Fintype H] (r : ℝ) (M : Matrix H H ℂ) (x : H → ℂ) : qInner x ((r • M).mulVec x) = ↑r * qInner x (M.mulVec x)

theorem QuantumQueryComplexity.qInner_proj_self {H : Type} [Fintype H] {P : Matrix H H ℂ} (hP : IsQProjector P) (x : H → ℂ) : qInner x (P.mulVec x) = ↑(qNormSq (P.mulVec x))

On a projector the quadratic form is the squared norm of the image.

theorem QuantumQueryComplexity.qInner_mul_proj {H : Type} [Fintype H] {A P : Matrix H H ℂ} (hP : IsQProjector P) (hc : A * P = P * A) (x : H → ℂ) : qInner x ((A * P).mulVec x) = qInner (P.mulVec x) (A.mulVec (P.mulVec x))

For an operator commuting with a projector, the quadratic form restricts to the projector's range.

theorem QuantumQueryComplexity.qInner_cfc_nonneg {H : Type} [Fintype H] [DecidableEq H] (a : Matrix H H ℂ) (g : ℝ → ℝ) (hg : ∀ (l : ℝ), 0 ≤ g l) (x : H → ℂ) : 0 ≤ (qInner x ((cfc g a).mulVec x)).re

A cfc of a nonnegative function has nonnegative quadratic form. Proved by writing g = √g · √g, so the matrix is MᴴM; no order theory is needed.

The near-window bound

noncomputable def QuantumQueryComplexity.chordGapFun (Δ : ℝ) : ℝ → ℝ

The gap function (Δ² - l)·mask l, nonnegative everywhere.

Equations

• QuantumQueryComplexity.chordGapFun Δ l = (Δ ^ 2 - l) * QuantumQueryComplexity.chordMask Δ l

theorem QuantumQueryComplexity.chordGapFun_nonneg (Δ l : ℝ) : 0 ≤ chordGapFun Δ l

theorem QuantumQueryComplexity.chordSq_mul_chordNearProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : chordSq U * chordNearProj U Δ + cfc (chordGapFun Δ) (chordSq U) = Δ ^ 2 • chordNearProj U Δ

theorem QuantumQueryComplexity.chordNear_bound_sq {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) (x : H → ℂ) : qNormSq ((1 - U).mulVec ((chordNearProj U Δ).mulVec x)) ≤ Δ ^ 2 * qNormSq ((chordNearProj U Δ).mulVec x)

The near-window bound: on the near window the chord distance is at most |Δ| (stated squared, so no absolute value appears).

Decomposition, and the fixed space

The two windows are complementary orthogonal projectors, so every state splits into a near part and a far part with no cross term. And the fixed space of U sits entirely in the near window, for every Δ: a vector with U x = x has chord distance 0, and 0 ≤ Δ² always. That is the statement a phase detector needs in order to conclude that it never mistakes a fixed vector for a rotating one.

@[simp]

theorem QuantumQueryComplexity.chordNearProj_add_chordFarProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : chordNearProj U Δ + chordFarProj U Δ = 1

theorem QuantumQueryComplexity.chordNearProj_mul_chordFarProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : chordNearProj U Δ * chordFarProj U Δ = 0

theorem QuantumQueryComplexity.chordFarProj_mul_chordNearProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : chordFarProj U Δ * chordNearProj U Δ = 0

theorem QuantumQueryComplexity.qNormSq_chord_decomp {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) (x : H → ℂ) : qNormSq x = qNormSq ((chordNearProj U Δ).mulVec x) + qNormSq ((chordFarProj U Δ).mulVec x)

The Pythagorean decomposition across the two windows.

theorem QuantumQueryComplexity.cfc_mulVec_eq_zero_of_mulVec_eq_zero {H : Type} [Fintype H] [DecidableEq H] {a : Matrix H H ℂ} (ha : IsSelfAdjoint a) (g : ℝ → ℝ) (hg0 : g 0 = 0) {x : H → ℂ} (hx : a.mulVec x = 0) : (cfc g a).mulVec x = 0

If g vanishes at 0 then cfc g a kills the kernel of a. Proved by factoring g l = l · h l — legitimate for any g here, since h need only be continuous on a finite spectrum.

theorem QuantumQueryComplexity.chordNearProj_mulVec_of_fixed {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) {x : H → ℂ} (hx : U.mulVec x = x) : (chordNearProj U Δ).mulVec x = x

The fixed space of U lies in the near window, for every Δ.

theorem QuantumQueryComplexity.chordFarProj_mulVec_of_fixed {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) {x : H → ℂ} (hx : U.mulVec x = x) : (chordFarProj U Δ).mulVec x = 0

The far window misses the fixed space.

The far-window bound

The companion to chordNear_bound_sq, and the coercivity estimate the uniform-clock argument consumes: off the near window the chord distance is at least |Δ|. Same proof shape, with the gap function's sign reversed.

theorem QuantumQueryComplexity.chordFarProj_eq_cfc {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : chordFarProj U Δ = cfc (fun (l : ℝ) => 1 - chordMask Δ l) (chordSq U)

noncomputable def QuantumQueryComplexity.chordFarGapFun (Δ : ℝ) : ℝ → ℝ

The far gap function (l - Δ²)·(1 - mask l), nonnegative everywhere.

Equations

• QuantumQueryComplexity.chordFarGapFun Δ l = (l - Δ ^ 2) * (1 - QuantumQueryComplexity.chordMask Δ l)

theorem QuantumQueryComplexity.chordFarGapFun_nonneg (Δ l : ℝ) : 0 ≤ chordFarGapFun Δ l

theorem QuantumQueryComplexity.chordSq_mul_chordFarProj {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) : Δ ^ 2 • chordFarProj U Δ + cfc (chordFarGapFun Δ) (chordSq U) = chordSq U * chordFarProj U Δ

theorem QuantumQueryComplexity.chordFar_bound_sq {H : Type} [Fintype H] [DecidableEq H] (U : Matrix H H ℂ) (Δ : ℝ) (x : H → ℂ) : Δ ^ 2 * qNormSq ((chordFarProj U Δ).mulVec x) ≤ qNormSq ((1 - U).mulVec ((chordFarProj U Δ).mulVec x))

The far-window bound (coercivity): off the near window the chord distance is at least |Δ|.

The effective spectral gap

The statement is naturally squared: everything in sight is a squared norm, and squaring avoids square roots entirely. The core is the elementary identity (1 - R_P R_L) w = 2 P w of SourceQuantumChordGap; the spectral content is only that the near window contracts 1 - U by Δ and that a projector does not expand.

theorem QuantumQueryComplexity.effective_chord_gap_sq {H : Type} [Fintype H] [DecidableEq H] {P L : Matrix H H ℂ} (hP : IsQProjector P) (hL : IsQProjector L) {w : H → ℂ} (hw : L.mulVec w = 0) (Δ : ℝ) : qNormSq ((chordNearProj (qRefl P * qRefl L) Δ).mulVec (P.mulVec w)) ≤ Δ ^ 2 / 4 * qNormSq w

The effective spectral gap. If L annihilates w, then the part of P w lying in the chord-distance window of threshold Δ² (radius |Δ|) of R_P R_L has squared norm at most (Δ²/4)‖w‖².

No sign hypothesis on Δ is needed: the squared formulation makes 0 ≤ Δ vacuous, since only Δ² ever appears.

Uniform-clock suppression on the far window

The spectral half of the uniform-clock detector, and nothing operational: this section knows about a unitary and its chord windows, not about clocks, routines, or queries.

The statement is that on the far window — chord distance at least |Δ| — the uniform average of the first T powers is small:

‖T⁻¹ ∑_{c<T} Uᶜ x‖² ≤ 4/(T²Δ²) · ‖x‖².

The proof is three lines of mathematics. Telescoping gives (1 - U)·∑_{t<T} Uᵗ = 1 - Uᵀ, so the average, hit with 1 - U, becomes T⁻¹(1 - Uᵀ)x, which has norm at most 2/T·‖x‖ because Uᵀ is unitary. On the far window ‖(1 - U)y‖ ≥ |Δ|·‖y‖ (chordFar_bound_sq), and dividing by Δ gives the bound. The far projector commutes with U, so it commutes with the geometric sum and can be moved wherever it is needed.

The workhorse is stated multiplied out, T²Δ²·‖avg‖² ≤ 4‖x‖², which holds for every Δ and every T with no positivity hypothesis; the divided form follows for 0 < Δ and 0 < T.

theorem QuantumQueryComplexity.qNormSq_one_sub_pow_mulVec_le {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) (T : ℕ) (x : H → ℂ) : qNormSq ((1 - U ^ T).mulVec x) ≤ 4 * qNormSq x

A unitary moves a vector by at most twice its norm: ‖(1 - Uᵀ)x‖ ≤ 2‖x‖, squared.

theorem QuantumQueryComplexity.chordFarProj_commute_geom {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) (Δ : ℝ) (T : ℕ) : Commute (chordFarProj U Δ) (∑ t ∈ Finset.range T, U ^ t)

The far projector commutes with the geometric sum, since it commutes with U.

theorem QuantumQueryComplexity.qNormSq_avg_pow_chordFar {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) (Δ : ℝ) (T : ℕ) (x : H → ℂ) : ↑T ^ 2 * Δ ^ 2 * qNormSq ((↑T)⁻¹ • ∑ c : Fin T, (U ^ ↑c).mulVec ((chordFarProj U Δ).mulVec x)) ≤ 4 * qNormSq x

Uniform-clock suppression, multiplied out. Holds for every Δ and every T, with no positivity hypothesis: it is vacuous at Δ = 0 or T = 0, which is exactly why the divided form below is the one that asks for both to be positive.

theorem QuantumQueryComplexity.qNormSq_avg_pow_chordFar_div {H : Type} [Fintype H] [DecidableEq H] {U : Matrix H H ℂ} (hU : U ∈ Matrix.unitaryGroup H ℂ) {Δ : ℝ} (hΔ : 0 < Δ) {T : ℕ} (hT : 0 < T) (x : H → ℂ) : qNormSq ((↑T)⁻¹ • ∑ c : Fin T, (U ^ ↑c).mulVec ((chordFarProj U Δ).mulVec x)) ≤ 4 / (↑T ^ 2 * Δ ^ 2) * qNormSq x

Uniform-clock suppression, in the form the detector uses: ‖T⁻¹ ∑_{c<T} Uᶜ x‖² ≤ 4/(T²Δ²)·‖x‖² on the far window.

The input-dependent reflection, in exactly two queries

The reflection the upper bound needs is about the orthogonal complement of a span of input-dependent vectors; it is built as

O_a · (fixed reflection) · O_a,

one query on each side of a fixed unitary, and that is exactly two queries — QRoutine.conjFixed costs 2 · R.len, and inversion is free because the transposition oracle is self-adjoint.

The sign is part of the statement. spanRefl v fixes the span, but the construction reflects about the complement, and subRefl (rawSpan v)ᗮ = -spanRefl v. Dropping that minus would shift every eigenphase by π, which controlled phase detection would then read off wrongly. inputRefl_run therefore carries the negation explicitly.

noncomputable def QuantumQueryComplexity.inputRefl {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) : QRoutine ι σ W

The input-dependent reflection: reflect about the orthogonal complement of a span, conjugated by one query on each side.

Equations

• QuantumQueryComplexity.inputRefl v = QuantumQueryComplexity.QRoutine.query.conjFixed (QuantumQueryComplexity.subRefl (QuantumQueryComplexity.rawSpan v)ᗮ) ⋯

@[simp]

theorem QuantumQueryComplexity.inputRefl_len {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) : (inputRefl v).len = 2

Exactly two queries.

theorem QuantumQueryComplexity.inputRefl_run {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) : (inputRefl v).run a = oracleMat a * (-spanRefl v * oracleMat a)

The operator it implements, with the complement's sign explicit.

theorem QuantumQueryComplexity.inputRefl_run' {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) : (inputRefl v).run a = oracleMat a * (subRefl (rawSpan v)ᗮ * oracleMat a)

The same, before the sign is resolved: it is the conjugate of the complement reflection.

The bridge to the mathematical layer

The effective-gap theorem is cleanest stated for an arbitrary projector. This is the projector the operational two-query reflection actually reflects about, so the final algorithm can instantiate the abstract theorem with it.

noncomputable def QuantumQueryComplexity.inputProj {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ

The input-dependent projector: the fixed complement projector, conjugated by one query on each side.

Equations

• QuantumQueryComplexity.inputProj v a = QuantumQueryComplexity.oracleMat a * QuantumQueryComplexity.subProj (QuantumQueryComplexity.rawSpan v)ᗮ * QuantumQueryComplexity.oracleMat a

theorem QuantumQueryComplexity.isQProjector_inputProj {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) : IsQProjector (inputProj v a)

theorem QuantumQueryComplexity.inputRefl_run_eq_qRefl {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) : (inputRefl v).run a = qRefl (inputProj v a)

The operational reflection is the reflection about that projector.

The composition-order trap

QRoutine.comp composes in execution order, while the matrix product composes in the opposite one: comp_run : (R.comp S).run a = S.run a * R.run a. So the operator R_P · R_L — the one the effective-gap theorem takes — is implemented by running L first, i.e. by RL.comp RP. Getting this backwards would silently build R_L · R_P, whose spectrum is the same but whose eigenvectors are not, so it is pinned here as a theorem rather than a comment.

theorem QuantumQueryComplexity.comp_run_eq_qRefl_mul {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {RP RL : QRoutine ι σ W} {P L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} (a : ι → σ) (hP : RP.run a = qRefl P) (hL : RL.run a = qRefl L) : (RL.comp RP).run a = qRefl P * qRefl L

The reflection product, in execution order.

@[simp]

theorem QuantumQueryComplexity.comp_len_reflProd {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (RP RL : QRoutine ι σ W) : (RL.comp RP).len = RL.len + RP.len

The reflection product

effective_chord_gap_sq consumes qRefl P * qRefl L. This definition builds exactly that operator as a routine, and in doing so pins the two facts a query count depends on:

• the order — L is run first, so the operator is R_P · R_L and not its reverse (see the trap above);
• the cost — the L-side reflection is a fixed, input-independent unitary, supplied as a zero-query ofUnitary. So the product costs exactly the two queries of the input-dependent side. inputRefl_len = 2 on its own says nothing about this: if both sides were input-dependent the product would cost four, and every downstream clock estimate would double.

inputReflProduct_len is therefore the theorem that licenses the 2 in the detector's query accounting. The specialization of the effective-gap theorem to this routine is proved in SourceQuantumOperationalGap.

noncomputable def QuantumQueryComplexity.inputReflProduct {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hL : IsQProjector L) : QRoutine ι σ W

The reflection product R_P · R_L, with R_L a fixed zero-query reflection and R_P the input-dependent two-query reflection.

Equations

• QuantumQueryComplexity.inputReflProduct v L hL = (QuantumQueryComplexity.QRoutine.ofUnitary (QuantumQueryComplexity.qRefl L) ⋯).comp (QuantumQueryComplexity.inputRefl v)

@[simp]

theorem QuantumQueryComplexity.inputReflProduct_len {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hL : IsQProjector L) : (inputReflProduct v L hL).len = 2

Exactly two queries — because the L-side is fixed.

theorem QuantumQueryComplexity.inputReflProduct_run {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hL : IsQProjector L) (a : ι → σ) : (inputReflProduct v L hL).run a = qRefl (inputProj v a) * qRefl L

The operator it implements, in the order effective_chord_gap_sq expects.

theorem QuantumQueryComplexity.inputRefl_run_mem_unitaryGroup {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) : (inputRefl v).run a ∈ Matrix.unitaryGroup (QBasis ι σ W) ℂ

Lifting a routine along a workspace extension

A routine built on workspace W runs unchanged on V × W: lift every fixed step with liftReg, and the queries pass through because the oracle ignores the workspace (blockFam_oracle). The query count is unchanged, and on the encoded subspace the lifted routine does exactly what the original does.

This is what lets a subroutine written for a small workspace be used inside a circuit that carries extra registers — a phase register, say.

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

Lift a routine along a workspace extension.

Equations

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

@[simp]

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

@[simp]

theorem QuantumQueryComplexity.QRoutine.liftReg_step {ι σ V W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (t : ℕ) : (liftReg V R).step t = QuantumQueryComplexity.liftReg V (R.step t)

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

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

theorem QuantumQueryComplexity.QRoutine.liftReg_run_embed {ι σ V W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype V] [DecidableEq V] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (a : ι → σ) (v : V) (ψ : QBasis ι σ W → ℂ) : ((liftReg V R).run a).mulVec (embedReg v ψ) = embedReg v ((R.run a).mulVec ψ)

The lifted routine acts as the original on the encoded subspace.

The clock compiler: coherent powers of a routine

A uniform clock needs selectPowers, the coherent map

|c⟩|ψ⟩ ↦ |c⟩ Uᶜ|ψ⟩,

which is not QRoutine.iterate — that applies a global Uⁿ to every branch. The compilation is the standard one: T-1 rounds, the j-th applying U exactly on the branches whose clock has reached j. Each round is

XOR the predicate j ≤ c into the control bit (a basis permutation, free) → QRoutine.control of the lifted routine (R.len queries) → XOR it back (free),

so a round costs exactly R.len and selectPowers R T costs (T-1)·R.len.

On top of SELECT this section builds the rest of the operational side of a uniform-clock detector:

• clockPack — a packed history, one workspace vector per clock branch. The branches are orthogonal, so Pythagoras holds and SELECT acts entrywise.
• uniformClock — the constant packed history, normalized.
• clockAvgProj — projection of the clock register onto its uniform superposition. On a packed history it returns the exact vector average T⁻¹ ∑_{c<T} f c; on SELECT applied to a uniform clock, T⁻¹ ∑_{c<T} Uᶜψ.
• clockPhaseRefl — the conjugation SELECTᴴ · clockRefl · SELECT, of exact length 2(T-1)·R.len: the reflection is a fixed unitary, so conjugation is the only cost.

The workspace is CtrlWork ι (Fin T × W): the control bit and parking slot of SourceQuantumControl, then the clock register, then the routine's own workspace. This file depends only on Control and RoutineLift; whether that average is small — the spectral half of the detector — is proved elsewhere, and the connection to spectral suppression belongs in a later file, not here.

@[reducible, inline]

abbrev QuantumQueryComplexity.ClockWork (ι : Type) (T : ℕ) (W : Type) : Type

The workspace of a clocked routine.

Equations

• QuantumQueryComplexity.ClockWork ι T W = QuantumQueryComplexity.CtrlWork ι (Fin T × W)

noncomputable def QuantumQueryComplexity.embedClock {ι σ W : Type} [DecidableEq ι] {T : ℕ} (c : Fin T) (b : Bool) (ψ : QBasis ι σ W → ℂ) : QBasis ι σ (ClockWork ι T W) → ℂ

The state with clock c, control bit b, blank parking slot, and ψ elsewhere.

Equations

• QuantumQueryComplexity.embedClock c b ψ = QuantumQueryComplexity.embedCtrl b (QuantumQueryComplexity.embedReg c ψ)

Flipping the control bit on the clock

def QuantumQueryComplexity.clockXorMap {ι σ W : Type} {T : ℕ} (j : ℕ) : QBasis ι σ (ClockWork ι T W) → QBasis ι σ (ClockWork ι T W)

Flip the control bit exactly on the branches whose clock has reached j.

Equations

• QuantumQueryComplexity.clockXorMap j (k, t, b, s, c, w) = (k, t, b ^^ decide (j ≤ ↑c), s, c, w)

theorem QuantumQueryComplexity.clockXorMap_involutive {ι σ W : Type} {T : ℕ} (j : ℕ) : Function.Involutive (clockXorMap j)

def QuantumQueryComplexity.clockXorPerm {ι σ W : Type} {T : ℕ} (j : ℕ) : Equiv.Perm (QBasis ι σ (ClockWork ι T W))

The bit flip, as a permutation of the basis.

Equations

• QuantumQueryComplexity.clockXorPerm j = Function.Involutive.toPerm (QuantumQueryComplexity.clockXorMap j) ⋯

def QuantumQueryComplexity.clockXorMat {ι σ W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] {T : ℕ} (j : ℕ) : Matrix (QBasis ι σ (ClockWork ι T W)) (QBasis ι σ (ClockWork ι T W)) ℂ

The bit flip, as a zero-query unitary.

Equations

• QuantumQueryComplexity.clockXorMat j = QuantumQueryComplexity.qPerm (QuantumQueryComplexity.clockXorPerm j)

theorem QuantumQueryComplexity.clockXorMat_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {T : ℕ} (j : ℕ) : clockXorMat j ∈ Matrix.unitaryGroup (QBasis ι σ (ClockWork ι T W)) ℂ

theorem QuantumQueryComplexity.clockXorMat_mulVec_apply {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {T : ℕ} (j : ℕ) (Φ : QBasis ι σ (ClockWork ι T W) → ℂ) (p : QBasis ι σ (ClockWork ι T W)) : (clockXorMat j).mulVec Φ p = Φ (clockXorMap j p)

theorem QuantumQueryComplexity.clockXorMat_mulVec_embedClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {T : ℕ} (j : ℕ) (c : Fin T) (b : Bool) (ψ : QBasis ι σ W → ℂ) : (clockXorMat j).mulVec (embedClock c b ψ) = embedClock c (b ^^ decide (j ≤ ↑c)) ψ

The bit flip reads the clock and touches nothing else.

One round

noncomputable def QuantumQueryComplexity.clockRound {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T j : ℕ) : QRoutine ι σ (ClockWork ι T W)

One clocked round: apply R exactly on the branches whose clock has reached j. The two bit flips are free, so this costs exactly R.len queries.

Equations

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

@[simp]

theorem QuantumQueryComplexity.clockRound_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T j : ℕ) : (clockRound R T j).len = R.len

theorem QuantumQueryComplexity.clockRound_run_matrix {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T j : ℕ) (a : ι → σ) : (clockRound R T j).run a = clockXorMat j * ((QRoutine.liftReg (Fin T) R).control.run a * clockXorMat j)

theorem QuantumQueryComplexity.clockRound_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T j : ℕ) (a : ι → σ) (c : Fin T) (ψ : QBasis ι σ W → ℂ) : ((clockRound R T j).run a).mulVec (embedClock c false ψ) = embedClock c false (if j ≤ ↑c then (R.run a).mulVec ψ else ψ)

One round applies R exactly on the branches that have reached j.

Coherent powers

noncomputable def QuantumQueryComplexity.selectUpto {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T a✝ : ℕ) : QRoutine ι σ (ClockWork ι T W)

The first n clocked rounds.

Equations

• QuantumQueryComplexity.selectUpto R T 0 = QuantumQueryComplexity.QRoutine.identity
• QuantumQueryComplexity.selectUpto R T n.succ = (QuantumQueryComplexity.selectUpto R T n).comp (QuantumQueryComplexity.clockRound R T (n + 1))

noncomputable def QuantumQueryComplexity.selectPowers {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) : QRoutine ι σ (ClockWork ι T W)

Coherent powers: |c⟩|ψ⟩ ↦ |c⟩ Uᶜ|ψ⟩, compiled as T-1 rounds.

Equations

• QuantumQueryComplexity.selectPowers R T = QuantumQueryComplexity.selectUpto R T (T - 1)

@[simp]

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

@[simp]

theorem QuantumQueryComplexity.selectPowers_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) : (selectPowers R T).len = (T - 1) * R.len

The exact query count: (T-1) · R.len.

theorem QuantumQueryComplexity.selectUpto_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T n : ℕ) (a : ι → σ) (c : Fin T) (ψ : QBasis ι σ W → ℂ) : ((selectUpto R T n).run a).mulVec (embedClock c false ψ) = embedClock c false ((R.run a ^ min n ↑c).mulVec ψ)

theorem QuantumQueryComplexity.selectPowers_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) (c : Fin T) (ψ : QBasis ι σ W → ℂ) : ((selectPowers R T).run a).mulVec (embedClock c false ψ) = embedClock c false ((R.run a ^ ↑c).mulVec ψ)

Coherent powers, verified: on a branch with clock c the routine has been applied exactly c times.

Packed histories

A packed history places a clock-indexed family in the clock branches, all with a blank control bit. It is the shape every statement about the clock takes: selectPowers acts on one entrywise, the branches are mutually orthogonal, and the uniform clock is the constant packed history, normalized.

noncomputable def QuantumQueryComplexity.clockPack {ι σ W : Type} [DecidableEq ι] {T : ℕ} (f : Fin T → QBasis ι σ W → ℂ) : QBasis ι σ (ClockWork ι T W) → ℂ

The packed history: f c in the branch whose clock reads c.

Equations

• QuantumQueryComplexity.clockPack f = ∑ c : Fin T, QuantumQueryComplexity.embedClock c false (f c)

theorem QuantumQueryComplexity.embedClock_smul {ι σ W : Type} [DecidableEq ι] {T : ℕ} (c : Fin T) (b : Bool) (a : ℂ) (ψ : QBasis ι σ W → ℂ) : embedClock c b (a • ψ) = a • embedClock c b ψ

theorem QuantumQueryComplexity.embedClock_sum {ι σ W : Type} [DecidableEq ι] {T : ℕ} {α : Type u_1} (c : Fin T) (b : Bool) (s : Finset α) (f : α → QBasis ι σ W → ℂ) : embedClock c b (∑ i ∈ s, f i) = ∑ i ∈ s, embedClock c b (f i)

theorem QuantumQueryComplexity.selectPowers_run_clockPack {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) (f : Fin T → QBasis ι σ W → ℂ) : ((selectPowers R T).run a).mulVec (clockPack f) = clockPack fun (c : Fin T) => (R.run a ^ ↑c).mulVec (f c)

SELECT acts on a packed history entrywise: branch c gets Uᶜ.

theorem QuantumQueryComplexity.qInner_embedClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] {T : ℕ} (c c' : Fin T) (b b' : Bool) (ψ φ : QBasis ι σ W → ℂ) : qInner (embedClock c b ψ) (embedClock c' b' φ) = if c = c' ∧ b = b' then qInner ψ φ else 0

Distinct clock branches are orthogonal, and a branch is an isometry.

theorem QuantumQueryComplexity.qNormSq_clockPack {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] {T : ℕ} (f : Fin T → QBasis ι σ W → ℂ) : qNormSq (clockPack f) = ∑ c : Fin T, qNormSq (f c)

Pythagoras for a packed history.

The uniform clock

noncomputable def QuantumQueryComplexity.uniformClock {ι σ W : Type} [DecidableEq ι] (T : ℕ) (ψ : QBasis ι σ W → ℂ) : QBasis ι σ (ClockWork ι T W) → ℂ

The uniform clock: ψ in every branch, normalized.

Equations

• QuantumQueryComplexity.uniformClock T ψ = (↑√↑T)⁻¹ • QuantumQueryComplexity.clockPack fun (x : Fin T) => ψ

theorem QuantumQueryComplexity.qNormSq_uniformClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] {T : ℕ} (hT : 0 < T) (ψ : QBasis ι σ W → ℂ) : qNormSq (uniformClock T ψ) = qNormSq ψ

The uniform clock is normalized (for 0 < T).

theorem QuantumQueryComplexity.uniformClock_apply_eq_zero {ι σ W : Type} [DecidableEq ι] (T : ℕ) (ψ : QBasis ι σ W → ℂ) {b : QBasis ι σ (ClockWork ι T W)} (h : ψ (b.1, b.2.1, b.2.2.2.2.2) = 0) : uniformClock T ψ b = 0

The clock spread preserves basis support: where the underlying vector vanishes at the stripped coordinate, the clocked vector vanishes at the full one. This is what lets a readout of the underlying workspace act through the clock.

theorem QuantumQueryComplexity.selectPowers_run_uniformClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) (ψ : QBasis ι σ W → ℂ) : ((selectPowers R T).run a).mulVec (uniformClock T ψ) = (↑√↑T)⁻¹ • clockPack fun (c : Fin T) => (R.run a ^ ↑c).mulVec ψ

SELECT on the uniform clock builds the history Uᶜψ.

The averaging projector

Projecting the clock register back onto the uniform superposition is what turns a packed history into the vector average T⁻¹ ∑_{c<T} Uᶜψ. That average is the whole point of a uniform clock: it is 1 on a fixed vector and small on a vector whose chord distance is large, which is the suppression the detector needs.

noncomputable def QuantumQueryComplexity.avgMat (T : ℕ) : Matrix (Fin T) (Fin T) ℂ

The uniform-average matrix on the clock register.

Equations

• QuantumQueryComplexity.avgMat T = Matrix.of fun (x x_1 : Fin T) => (↑T)⁻¹

theorem QuantumQueryComplexity.isQProjector_avgMat (T : ℕ) : IsQProjector (avgMat T)

noncomputable def QuantumQueryComplexity.clockAvgProj {ι σ W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] (T : ℕ) : Matrix (QBasis ι σ (ClockWork ι T W)) (QBasis ι σ (ClockWork ι T W)) ℂ

The averaging projector on the clock register.

Equations

• QuantumQueryComplexity.clockAvgProj T = QuantumQueryComplexity.liftReg Bool (QuantumQueryComplexity.liftReg (Option ι) (QuantumQueryComplexity.regOp (QuantumQueryComplexity.avgMat T)))

theorem QuantumQueryComplexity.isQProjector_clockAvgProj {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (T : ℕ) : IsQProjector (clockAvgProj T)

theorem QuantumQueryComplexity.clockAvgProj_mulVec_embedClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (T : ℕ) (c : Fin T) (ψ : QBasis ι σ W → ℂ) : (clockAvgProj T).mulVec (embedClock c false ψ) = ∑ c' : Fin T, (↑T)⁻¹ • embedClock c' false ψ

theorem QuantumQueryComplexity.clockAvgProj_mulVec_clockPack {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (T : ℕ) (f : Fin T → QBasis ι σ W → ℂ) : (clockAvgProj T).mulVec (clockPack f) = clockPack fun (x : Fin T) => (↑T)⁻¹ • ∑ c : Fin T, f c

The averaging projector produces the exact vector average. On the packed history f it returns the constant history T⁻¹ ∑_{c<T} f c — in particular, on SELECT applied to a uniform clock, T⁻¹ ∑_{c<T} Uᶜψ.

The phase reflection

clockRefl reflects about the uniform-clock subspace; it is a fixed unitary, touching no oracle. Conjugating it by SELECT is the phase reflection of a uniform-clock detector, and the conjugation is where the query count doubles — and only doubles.

noncomputable def QuantumQueryComplexity.clockRefl {ι σ W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] (T : ℕ) : Matrix (QBasis ι σ (ClockWork ι T W)) (QBasis ι σ (ClockWork ι T W)) ℂ

The reflection about the uniform-clock subspace.

Equations

• QuantumQueryComplexity.clockRefl T = QuantumQueryComplexity.qRefl (QuantumQueryComplexity.clockAvgProj T)

theorem QuantumQueryComplexity.clockRefl_mem_unitaryGroup {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (T : ℕ) : clockRefl T ∈ Matrix.unitaryGroup (QBasis ι σ (ClockWork ι T W)) ℂ

theorem QuantumQueryComplexity.selectPowers_conjTranspose_mulVec_embedClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) (c : Fin T) (ψ : QBasis ι σ W → ℂ) : ((selectPowers R T).run a).conjTranspose.mulVec (embedClock c false ψ) = embedClock c false ((R.run a ^ ↑c).conjTranspose.mulVec ψ)

SELECTᴴ undoes the powers branchwise.

theorem QuantumQueryComplexity.selectPowers_conjTranspose_mulVec_clockPack {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) (f : Fin T → QBasis ι σ W → ℂ) : ((selectPowers R T).run a).conjTranspose.mulVec (clockPack f) = clockPack fun (c : Fin T) => (R.run a ^ ↑c).conjTranspose.mulVec (f c)

SELECTᴴ on a packed history.

theorem QuantumQueryComplexity.clockRefl_conjTranspose {ι σ W : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq W] (T : ℕ) [Finite W] [Finite σ] [Finite ι] : (clockRefl T).conjTranspose = clockRefl T

The clock reflection is self-adjoint — it is the reflection about a projector. No positivity hypothesis.

noncomputable def QuantumQueryComplexity.clockPhaseRefl {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) : QRoutine ι σ (ClockWork ι T W)

The phase reflection: SELECTᴴ · clockRefl · SELECT.

Equations

• QuantumQueryComplexity.clockPhaseRefl R T = (QuantumQueryComplexity.selectPowers R T).conjFixed (QuantumQueryComplexity.clockRefl T) ⋯

@[simp]

theorem QuantumQueryComplexity.clockPhaseRefl_len {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) : (clockPhaseRefl R T).len = 2 * ((T - 1) * R.len)

The exact query count of the phase reflection: 2(T-1)·R.len. The reflection itself is free, so conjugation is the only cost.

theorem QuantumQueryComplexity.clockPhaseRefl_run {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) : (clockPhaseRefl R T).run a = ((selectPowers R T).run a).conjTranspose * (clockRefl T * (selectPowers R T).run a)

theorem QuantumQueryComplexity.clockPhaseRefl_run_conjTranspose {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) : ((clockPhaseRefl R T).run a).conjTranspose = (clockPhaseRefl R T).run a

The detector is self-adjoint. Conjugating a self-adjoint reflection by a unitary keeps it self-adjoint. With unitarity this is what makes the two signed conversion errors orthogonal, so they combine by an exact half-sum rather than a triangle inequality — which is where the constant would otherwise be lost.

The averaging identity, and exact completeness

Two facts fix the detector's behaviour at the two extremes. On a fixed vector it is exactly the identity — not approximately, which is what lets the effective-gap argument conclude anything at all. On a general vector it returns the vector average T⁻¹ ∑_{c<T} Uᶜψ, whose size is the detector's entire content; bounding that is the spectral half, proved elsewhere.

theorem QuantumQueryComplexity.clockAvgProj_mulVec_selectPowers_uniformClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) (ψ : QBasis ι σ W → ℂ) : (clockAvgProj T).mulVec (((selectPowers R T).run a).mulVec (uniformClock T ψ)) = uniformClock T ((↑T)⁻¹ • ∑ c : Fin T, (R.run a ^ ↑c).mulVec ψ)

The normalized averaging identity. Projecting SELECT applied to a uniform clock returns a uniform clock carrying the exact vector average.

theorem QuantumQueryComplexity.clockAvgProj_mulVec_uniformClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {T : ℕ} (hT : 0 < T) (ψ : QBasis ι σ W → ℂ) : (clockAvgProj T).mulVec (uniformClock T ψ) = uniformClock T ψ

The uniform clock is fixed by the averaging projector: averaging a constant history changes nothing.

theorem QuantumQueryComplexity.clockRefl_mulVec_uniformClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {T : ℕ} (hT : 0 < T) (ψ : QBasis ι σ W → ℂ) : (clockRefl T).mulVec (uniformClock T ψ) = uniformClock T ψ

The reflection fixes the uniform clock (+1).

theorem QuantumQueryComplexity.clockRefl_mulVec_of_avg_eq_zero {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {T : ℕ} {v : QBasis ι σ (ClockWork ι T W) → ℂ} (h : (clockAvgProj T).mulVec v = 0) : (clockRefl T).mulVec v = -v

The reflection negates the complement (-1). This is the sign: with qRefl P = 2P - 1 the uniform subspace is the +1 eigenspace, so a detector built from it reports agreement as +1 and disagreement as -1.

theorem QuantumQueryComplexity.pow_mulVec_eq_self {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {U : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} {ψ : QBasis ι σ W → ℂ} (h : U.mulVec ψ = ψ) (n : ℕ) : (U ^ n).mulVec ψ = ψ

theorem QuantumQueryComplexity.selectPowers_run_mulVec_uniformClock_of_fixed {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) {ψ : QBasis ι σ W → ℂ} (h : (R.run a).mulVec ψ = ψ) : ((selectPowers R T).run a).mulVec (uniformClock T ψ) = uniformClock T ψ

SELECT fixes a uniform clock over a fixed vector: every branch applies a power of U, and every power fixes ψ.

theorem QuantumQueryComplexity.clockPhaseRefl_run_mulVec_uniformClock_of_fixed {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) {T : ℕ} (hT : 0 < T) (a : ι → σ) {ψ : QBasis ι σ W → ℂ} (h : (R.run a).mulVec ψ = ψ) : ((clockPhaseRefl R T).run a).mulVec (uniformClock T ψ) = uniformClock T ψ

Exact completeness: on a fixed vector the detector is the identity, with no error term at all.

The uniform clock, as an isometry

Moved down from SourceQuantumDetection: this geometry is generic, and the uniform witness needs the clock isometry without importing the Boolean detection layer.

theorem QuantumQueryComplexity.embedReg_add {ι σ W V : Type} [DecidableEq V] (v : V) (ψ φ : QBasis ι σ W → ℂ) : embedReg v (ψ + φ) = embedReg v ψ + embedReg v φ

theorem QuantumQueryComplexity.embedClock_add {ι σ W : Type} [DecidableEq ι] {T : ℕ} (c : Fin T) (b : Bool) (ψ φ : QBasis ι σ W → ℂ) : embedClock c b (ψ + φ) = embedClock c b ψ + embedClock c b φ

theorem QuantumQueryComplexity.uniformClock_add {ι σ W : Type} [DecidableEq ι] (T : ℕ) (ψ φ : QBasis ι σ W → ℂ) : uniformClock T (ψ + φ) = uniformClock T ψ + uniformClock T φ

The uniform clock is additive.

theorem QuantumQueryComplexity.qInner_clockPack {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] {T : ℕ} (f g : Fin T → QBasis ι σ W → ℂ) : qInner (clockPack f) (clockPack g) = ∑ c : Fin T, qInner (f c) (g c)

The inner product of two packed histories is branchwise.

theorem QuantumQueryComplexity.qInner_uniformClock {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype W] {T : ℕ} (hT : 0 < T) (ψ φ : QBasis ι σ W → ℂ) : qInner (uniformClock T ψ) (uniformClock T φ) = qInner ψ φ

The uniform clock is an isometry (for 0 < T).

theorem QuantumQueryComplexity.uniformClock_smul {ι σ W : Type} [DecidableEq ι] (T : ℕ) (r : ℂ) (ψ : QBasis ι σ W → ℂ) : uniformClock T (r • ψ) = r • uniformClock T ψ

The uniform clock is ℂ-homogeneous.

theorem QuantumQueryComplexity.uniformClock_sub {ι σ W : Type} [DecidableEq ι] (T : ℕ) (ψ φ : QBasis ι σ W → ℂ) : uniformClock T (ψ - φ) = uniformClock T ψ - uniformClock T φ

The uniform clock is subtractive.

theorem QuantumQueryComplexity.uniformClock_zero {ι σ W : Type} [DecidableEq ι] (ψ : QBasis ι σ W → ℂ) : uniformClock 0 ψ = 0

The empty clock carries nothing: at T = 0 the clock pack is an empty sum, so uniformClock 0 ψ = 0. This is what lets T = 0 splits downstream avoid positivity hypotheses.

The effective gap, for the operational reflection product

The effective-gap specialization bridge, where the operational layer (routines, queries, oracles) and the spectral layer (functional calculus, chord windows) meet for the reflection product. It is not the only such crossing — SourceQuantumClockDetector is the suppression bridge, joining the same two layers for the uniform clock — so the two are kept apart, and SourceQuantumInputDetector combines both estimates.

SourceQuantumChordWindow states the effective gap for an arbitrary pair of projectors, which is how it should be stated — it is a fact about reflections, not about queries. SourceQuantumReflection builds the operational product R_P · R_L as a two-query routine. This section instantiates the spectral theorem with that routine.

theorem QuantumQueryComplexity.effective_chord_gap_sq_inputReflProduct {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hL : IsQProjector L) (a : ι → σ) {w : QBasis ι σ W → ℂ} (hw : L.mulVec w = 0) (Δ : ℝ) : qNormSq ((chordNearProj ((inputReflProduct v L hL).run a) Δ).mulVec ((inputProj v a).mulVec w)) ≤ Δ ^ 2 / 4 * qNormSq w

The effective gap, for the operational product. The abstract theorem of SourceQuantumChordWindow, instantiated by the two-query routine of SourceQuantumReflection.

The uniform-clock detector

The suppression bridge: the operational clock of SourceQuantumClock meets the spectral estimate of SourceQuantumClockGap. It needs those two and nothing else — in particular not SourceQuantumOperationalGap, which is for specializing this to the input reflection product, not for stating it.

The detector is clockPhaseRefl R T = SELECTᴴ · clockRefl · SELECT, and the two facts about it are exactly the two extremes:

• Completeness (SourceQuantumClock): on a fixed vector it is the identity, exactly.

• Soundness (here): on the far window it is -1 up to an error that shrinks like 1/T:

  `‖D·u + u‖² ≤ 16/(T²Δ²)·‖x‖²`,   `u = uniformClock T (F x)`.
  

Both come from one algebraic identity, D·u + u = 2·SELECTᴴ P SELECT u: the detector's deviation from -1 is twice the averaging projector's output, so soundness is precisely the statement that the vector average is small. The 16 is 4 · 4: one factor from that 2, squared, and one from ‖1 - Uᵀ‖ ≤ 2 inside the suppression bound.

theorem QuantumQueryComplexity.clockPhaseRefl_run_mulVec_add {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) (u : QBasis ι σ (ClockWork ι T W) → ℂ) : ((clockPhaseRefl R T).run a).mulVec u + u = 2 • ((selectPowers R T).run a).conjTranspose.mulVec ((clockAvgProj T).mulVec (((selectPowers R T).run a).mulVec u))

The detector's deviation from -1 is twice the averaged state. This is the identity behind everything below: D·u + u = 2·SELECTᴴ P SELECT u.

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

theorem QuantumQueryComplexity.qNormSq_clockPhaseRefl_add_le {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) (T : ℕ) (a : ι → σ) (Δ : ℝ) (x : QBasis ι σ W → ℂ) : ↑T ^ 2 * Δ ^ 2 * qNormSq (((clockPhaseRefl R T).run a).mulVec (uniformClock T ((chordFarProj (R.run a) Δ).mulVec x)) + uniformClock T ((chordFarProj (R.run a) Δ).mulVec x)) ≤ 16 * qNormSq x

Soundness of the detector, multiplied out. On the far window the detector is -1 up to an error controlled by 1/(TΔ). As with the suppression bound it rests on, this form needs no positivity hypothesis: at T = 0 the factor T² kills the left side.

theorem QuantumQueryComplexity.qNormSq_clockPhaseRefl_add_le_div {ι σ W : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (R : QRoutine ι σ W) {T : ℕ} (hT : 0 < T) (a : ι → σ) {Δ : ℝ} (hΔ : 0 < Δ) (x : QBasis ι σ W → ℂ) : qNormSq (((clockPhaseRefl R T).run a).mulVec (uniformClock T ((chordFarProj (R.run a) Δ).mulVec x)) + uniformClock T ((chordFarProj (R.run a) Δ).mulVec x)) ≤ 16 / (↑T ^ 2 * Δ ^ 2) * qNormSq x

Soundness of the detector, in divided form: ‖D·u + u‖² ≤ 16/(T²Δ²)·‖x‖².

The detector for the input reflection product

The specialization, and the only file that needs both the suppression bridge (SourceQuantumClockDetector) and the effective gap for the operational product (SourceQuantumOperationalGap). Everything upstream stays generic: ClockDetector knows nothing about input reflections, OperationalGap nothing about clocks.

Three facts, which together are the detector's guarantee on P w:

• Cost. 4(T-1) queries, exactly. inputReflProduct costs 2 because the L-side reflection is a fixed, zero-query ofUnitary, and conjugating SELECT doubles (T-1)·2. If both sides were input-dependent this would be 8(T-1).
• The far part is large. The effective gap bounds the near part of P w by (Δ²/4)‖w‖², so by the Pythagorean decomposition the far part carries at least ‖P w‖² - (Δ²/4)‖w‖².
• The detector reads -1 there, up to 16/(T²Δ²)·‖P w‖².

Completeness is clockPhaseRefl_run_mulVec_uniformClock_of_fixed: on a vector fixed by the reflection product the detector is exactly the identity, so the two verdicts are separated with no error on one side.

theorem QuantumQueryComplexity.clockPhaseRefl_len_inputReflProduct {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hL : IsQProjector L) (T : ℕ) : (clockPhaseRefl (inputReflProduct v L hL) T).len = 4 * (T - 1)

The exact cost of the input detector: 4(T-1) queries.

theorem QuantumQueryComplexity.le_qNormSq_chordFar_inputProj {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hL : IsQProjector L) (a : ι → σ) {w : QBasis ι σ W → ℂ} (hw : L.mulVec w = 0) (Δ : ℝ) : qNormSq ((inputProj v a).mulVec w) - Δ ^ 2 / 4 * qNormSq w ≤ qNormSq ((chordFarProj ((inputReflProduct v L hL).run a) Δ).mulVec ((inputProj v a).mulVec w))

The far window carries what the effective gap leaves. The near part of P w is at most (Δ²/4)‖w‖², so the far part — the part the detector sees — is at least ‖P w‖² minus that.

theorem QuantumQueryComplexity.qNormSq_clockPhaseRefl_add_le_inputReflProduct {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hL : IsQProjector L) (T : ℕ) (a : ι → σ) (Δ : ℝ) (w : QBasis ι σ W → ℂ) : ↑T ^ 2 * Δ ^ 2 * qNormSq (((clockPhaseRefl (inputReflProduct v L hL) T).run a).mulVec (uniformClock T ((chordFarProj ((inputReflProduct v L hL).run a) Δ).mulVec ((inputProj v a).mulVec w))) + uniformClock T ((chordFarProj ((inputReflProduct v L hL).run a) Δ).mulVec ((inputProj v a).mulVec w))) ≤ 16 * qNormSq ((inputProj v a).mulVec w)

The input detector reads -1 on the far window, multiplied out — and, like the bound it specializes, with no positivity hypothesis.

theorem QuantumQueryComplexity.qNormSq_clockPhaseRefl_add_le_div_inputReflProduct {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (hL : IsQProjector L) {T : ℕ} (hT : 0 < T) (a : ι → σ) {Δ : ℝ} (hΔ : 0 < Δ) (w : QBasis ι σ W → ℂ) : qNormSq (((clockPhaseRefl (inputReflProduct v L hL) T).run a).mulVec (uniformClock T ((chordFarProj ((inputReflProduct v L hL).run a) Δ).mulVec ((inputProj v a).mulVec w))) + uniformClock T ((chordFarProj ((inputReflProduct v L hL).run a) Δ).mulVec ((inputProj v a).mulVec w))) ≤ 16 / (↑T ^ 2 * Δ ^ 2) * qNormSq ((inputProj v a).mulVec w)

The input detector reads -1 on the far window, in divided form.

Witness states for state conversion

The detector of SourceQuantumInputDetector distinguishes two kinds of vector: those fixed by the reflection product R_P R_L, which it reports as +1 exactly, and those in the far window, which it reports as -1 up to 16/(T²Δ²). State conversion has to supply both, from a dual adversary solution.

This section fixes the contracts — what a construction must prove — and derives everything that follows from them formally, so that the construction itself has a single, sharp target.

The positive side

A positive witness for the input a is a state φ with

inputProj v a *ᵥ φ = φ        and        L *ᵥ φ = φ.

Both reflections then fix φ, hence so does inputReflProduct, hence the detector is exactly the identity on uniformClock T φ. No estimate is involved on this side, which is the point.

The witness is not the bare target. In the corrected LMRSS construction the fixed point is φₓ = t₊ + (witness-workspace term), not t₊ itself: t₊ alone is in general not fixed by inputProj v a, since being fixed means the oracle-rotated state is orthogonal to every generator v i, which the workspace term is exactly what arranges. Building the algorithm around bare t₊ would be a real error, not a normalization detail, so the overlap ⟪t₊, φₓ⟫ is a separate obligation of the construction rather than something this interface can assume.

inputProj_mulVec_eq_self_iff reduces the first contract to one inner product per generator, which is the form a construction can discharge.

The negative side

A negative witness is a w with L *ᵥ w = 0. That is precisely the hypothesis of effective_chord_gap_sq_inputReflProduct, so the near component of P w is at most (Δ²/4)‖w‖² and — by le_qNormSq_chordFar_inputProj — the far window carries the rest.

That is the spectral half of the negative side, and it is all this interface supplies. It is not all the construction owes. Two further obligations stay with the concrete witness, and neither is formal:

• a bound on ‖w‖², since the effective gap charges (Δ²/4)‖w‖² against ‖P w‖² — a negative witness of uncontrolled norm buys nothing;
• the identification of inputProj v a *ᵥ w with the intended t₋ direction. As on the positive side, w carries a correction term beyond t₋, and what has to be shown is that inputProj kills that term, leaving the direction the algorithm measures.

So the asymmetry between the two sides is real but small: the positive side ends in an exact fixed-point identity, the negative side in two estimates. Both are quantitative facts about a particular construction, which is why neither lives in IsPosWitness.

Being fixed by the input projector

theorem QuantumQueryComplexity.inputProj_mulVec_eq_self_iff {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) (φ : QBasis ι σ W → ℂ) : (inputProj v a).mulVec φ = φ ↔ ∀ (i : ι'), qInner (v i) ((oracleMat a).mulVec φ) = 0

Fixed by the input projector = orthogonal to every generator, after the query. inputProj v a conjugates the complement projector by one oracle call on each side, so its fixed space is the pullback along the oracle of the orthogonal complement of the generators.

The positive witness

structure QuantumQueryComplexity.IsPosWitness {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ) (a : ι → σ) (φ : QBasis ι σ W → ℂ) : Prop

A positive witness for the input a: fixed by the input projector and by L. These are the two contracts a state-conversion construction must discharge; everything below is formal consequence.

• inputFixed : (inputProj v a).mulVec φ = φ

  The oracle-rotated witness is orthogonal to every generator.

• fixedL : L.mulVec φ = φ

  The witness lies in the fixed space of L.

theorem QuantumQueryComplexity.IsPosWitness.of_inner {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {v : ι' → QBasis ι σ W → ℂ} {L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} {a : ι → σ} {φ : QBasis ι σ W → ℂ} (h : ∀ (i : ι'), qInner (v i) ((oracleMat a).mulVec φ) = 0) (hL : L.mulVec φ = φ) : IsPosWitness v L a φ

Build a witness from the generator-orthogonality form.

theorem QuantumQueryComplexity.IsPosWitness.inputRefl_run_mulVec {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {v : ι' → QBasis ι σ W → ℂ} {L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} {a : ι → σ} {φ : QBasis ι σ W → ℂ} (h : IsPosWitness v L a φ) : ((inputRefl v).run a).mulVec φ = φ

The input reflection fixes the witness.

theorem QuantumQueryComplexity.IsPosWitness.qRefl_mulVec {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {v : ι' → QBasis ι σ W → ℂ} {L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} {a : ι → σ} {φ : QBasis ι σ W → ℂ} (h : IsPosWitness v L a φ) : (qRefl L).mulVec φ = φ

The L-reflection fixes the witness.

theorem QuantumQueryComplexity.IsPosWitness.inputReflProduct_run_mulVec {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {v : ι' → QBasis ι σ W → ℂ} {L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} {a : ι → σ} {φ : QBasis ι σ W → ℂ} (h : IsPosWitness v L a φ) (hL : IsQProjector L) : ((inputReflProduct v L hL).run a).mulVec φ = φ

The reflection product fixes the witness. Both factors do, so the product does — and this is the hypothesis the detector's completeness theorem asks for.

theorem QuantumQueryComplexity.IsPosWitness.clockPhaseRefl_run_mulVec_uniformClock {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {v : ι' → QBasis ι σ W → ℂ} {L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} {a : ι → σ} {φ : QBasis ι σ W → ℂ} (h : IsPosWitness v L a φ) (hL : IsQProjector L) {T : ℕ} (hT : 0 < T) : ((clockPhaseRefl (inputReflProduct v L hL) T).run a).mulVec (uniformClock T φ) = uniformClock T φ

Detector completeness, immediately. On a uniform clock over a positive witness the detector is exactly the identity — no error term, at cost 4(T-1).

theorem QuantumQueryComplexity.IsPosWitness.chordNearProj_mulVec {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {v : ι' → QBasis ι σ W → ℂ} {L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} {a : ι → σ} {φ : QBasis ι σ W → ℂ} (h : IsPosWitness v L a φ) (hL : IsQProjector L) (Δ : ℝ) : (chordNearProj ((inputReflProduct v L hL).run a) Δ).mulVec φ = φ

The witness lies in the near window for every Δ: it is fixed, so its chord distance is zero.

theorem QuantumQueryComplexity.IsPosWitness.chordFarProj_mulVec {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] {v : ι' → QBasis ι σ W → ℂ} {L : Matrix (QBasis ι σ W) (QBasis ι σ W) ℂ} {a : ι → σ} {φ : QBasis ι σ W → ℂ} (h : IsPosWitness v L a φ) (hL : IsQProjector L) (Δ : ℝ) : (chordFarProj ((inputReflProduct v L hL).run a) Δ).mulVec φ = 0

…and therefore contributes nothing to the far window, which is what keeps the two verdicts apart.

Generators are killed by the input projector

inputProj v a is oracleMat a conjugating the projector onto (rawSpan v)ᗮ. A generator, carried through the oracle, therefore lands on the span itself and is annihilated. This is the one fact the uniform witness's projector contracts need, and it is generic: nothing about the particular family v enters.

theorem QuantumQueryComplexity.inputProj_mulVec_of_forall_qInner_eq_zero {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) {ψ : QBasis ι σ W → ℂ} (h : ∀ (p : ι'), qInner (v p) ((oracleMat a).mulVec ψ) = 0) : (inputProj v a).mulVec ψ = ψ

The fixed space of inputProj, in the form a witness can check: one inner product per generator, no spans.

theorem QuantumQueryComplexity.inputProj_mulVec_oracle_generator {ι σ W ι' : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype W] [DecidableEq W] (v : ι' → QBasis ι σ W → ℂ) (a : ι → σ) (p : ι') : (inputProj v a).mulVec ((oracleMat a).mulVec (v p)) = 0

The coherent target states

These coherent targets fix the normalization used by the uniform extraction. The Boolean witness construction is retained in SourceQuantumWitness.

The output register must not be indexed by O — O is an arbitrary decidable type with no Fintype — but it need not be: only the image of f is ever occupied, and Set.range f is finite whenever X is, whatever O is. So the workspace is Option ↥(Set.range f): one "common" coordinate beside one coordinate per attained output. (X = ∅ is handled separately by the caller; [Nonempty O] is what keeps the readout total.)

The target states are

t_{x±} = (|common⟩ ± |f x⟩) / √2

and the identity that drives the whole construction is

⟪t_{y−}, t_{x+}⟫ = ½·[f y ≠ f x].

The ½ is load-bearing. It is what forces the witness scaling to be

φ_x = t_{x+} + α·V_x,        w_y = t_{y−} − (2α)⁻¹·U_y,

since then (2α)⁻¹·α = ½ cancels the ½ above against ⟪U_y, V_x⟫ = [f y ≠ f x], giving exact orthogonality ⟪w_y, φ_x⟫ = 0. Dropping the ½ — scaling by α⁻¹ instead — would destroy that cancellation, and the resulting norm bound 1 + 2α⁻²c is in any case four times looser than the correct 1 + c/(2α²).

These states are literally the alphabet gadget of SourceQuantumUniformAlphabet applied to the alphabet Set.range f and rescaled by (√2)⁻¹: the ½ in the overlap is exactly that rescaling squared. So the (1, ±e) factorization does double duty — packets on σ, targets on range f — and the two ½s that cancel have a common origin.

def QuantumQueryComplexity.rangeElem {X O : Type} (f : X → O) (x : X) : ↑(Set.range f)

The attained output of x, as an element of the finite workspace.

Equations

• QuantumQueryComplexity.rangeElem f x = ⟨f x, ⋯⟩

@[simp]

theorem QuantumQueryComplexity.rangeElem_val {X O : Type} (f : X → O) (x : X) : ↑(rangeElem f x) = f x

theorem QuantumQueryComplexity.rangeElem_eq_iff {X O : Type} (f : X → O) (x y : X) : rangeElem f x = rangeElem f y ↔ f x = f y

noncomputable def QuantumQueryComplexity.tPlus {X O : Type} [DecidableEq O] (f : X → O) (x : X) : Option ↑(Set.range f) → ℝ

The + target state (|common⟩ + |f x⟩)/√2.

Equations

• QuantumQueryComplexity.tPlus f x = (√2)⁻¹ • QuantumQueryComplexity.uniformLeft (QuantumQueryComplexity.rangeElem f x)

noncomputable def QuantumQueryComplexity.tMinus {X O : Type} [DecidableEq O] (f : X → O) (x : X) : Option ↑(Set.range f) → ℝ

The − target state (|common⟩ − |f x⟩)/√2.

Equations

• QuantumQueryComplexity.tMinus f x = (√2)⁻¹ • QuantumQueryComplexity.uniformRight (QuantumQueryComplexity.rangeElem f x)

theorem QuantumQueryComplexity.inv_sqrt_two_sq : (√2)⁻¹ * (√2)⁻¹ = 1 / 2

theorem QuantumQueryComplexity.normSq_inv_sqrt_two : Complex.normSq ↑(√2)⁻¹ = 1 / 2

The normalization fact in the form the conversion bounds consume.

theorem QuantumQueryComplexity.tPlus_dotProduct_tMinus {X O : Type} [Fintype X] [DecidableEq O] (f : X → O) (x y : X) : tPlus f x ⬝ᵥ tMinus f y = if f x = f y then 0 else 1 / 2

The + and − targets are orthogonal on matching outputs.

theorem QuantumQueryComplexity.tPlus_normSq {X O : Type} [Fintype X] [DecidableEq O] (f : X → O) (x : X) : tPlus f x ⬝ᵥ tPlus f x = 1

The target states are unit vectors.

theorem QuantumQueryComplexity.tMinus_normSq {X O : Type} [Fintype X] [DecidableEq O] (f : X → O) (x : X) : tMinus f x ⬝ᵥ tMinus f x = 1

theorem QuantumQueryComplexity.tMinus_dotProduct_tPlus {X O : Type} [Fintype X] [DecidableEq O] (f : X → O) (x y : X) : tMinus f y ⬝ᵥ tPlus f x = if f x = f y then 0 else 1 / 2

The driving identity: ⟪t_{y−}, t_{x+}⟫ = ½·[f y ≠ f x]. The ½ is what forces the (2α)⁻¹ in the witness scaling.

theorem QuantumQueryComplexity.tMinus_dotProduct_tPlus_of_ne {X O : Type} [Fintype X] [DecidableEq O] (f : X → O) {x y : X} (h : f x ≠ f y) : tMinus f y ⬝ᵥ tPlus f x = 1 / 2

The same identity in the form the orthogonality computation uses: the overlap is ½ exactly on the pairs the dual constraint has to separate.

theorem QuantumQueryComplexity.tMinus_dotProduct_tPlus_of_eq {X O : Type} [Fintype X] [DecidableEq O] (f : X → O) {x y : X} (h : f x = f y) : tMinus f y ⬝ᵥ tPlus f x = 0

The common and output vectors

The conversion combines the two signed targets through

common = (t_{x+} + t_{x−})/√2        out(f x) = (t_{x+} − t_{x−})/√2,

which are exactly the constant coordinate and the attained-output coordinate: the algorithm starts on the input-independent common state, and the detector carries it onto the output-labelled unit vector. Distinct outputs give orthogonal out vectors, which is what the final readout measures — one coherent conversion, never one detector per output.

def QuantumQueryComplexity.commonVec {R : Type} : Option R → ℝ

The common initial vector: the constant coordinate alone.

Equations

• QuantumQueryComplexity.commonVec none = 1
• QuantumQueryComplexity.commonVec (some val) = 0

def QuantumQueryComplexity.outVec {R : Type} [DecidableEq R] (r : R) : Option R → ℝ

The output-labelled vector: the coordinate of one attained output.

Equations

• QuantumQueryComplexity.outVec r none = 0
• QuantumQueryComplexity.outVec r (some val) = if val = r then 1 else 0

@[simp]

theorem QuantumQueryComplexity.commonVec_none {R : Type} : commonVec none = 1

@[simp]

theorem QuantumQueryComplexity.commonVec_some {R : Type} (r : R) : commonVec (some r) = 0

@[simp]

theorem QuantumQueryComplexity.outVec_none {R : Type} [DecidableEq R] (r : R) : outVec r none = 0

@[simp]

theorem QuantumQueryComplexity.outVec_some {R : Type} [DecidableEq R] (r s : R) : outVec r (some s) = if s = r then 1 else 0

theorem QuantumQueryComplexity.commonVec_dotProduct_commonVec {R : Type} [Fintype R] : commonVec ⬝ᵥ commonVec = 1

The common vector is a unit vector.

theorem QuantumQueryComplexity.outVec_dotProduct_outVec {R : Type} [Fintype R] [DecidableEq R] (r r' : R) : outVec r ⬝ᵥ outVec r' = if r = r' then 1 else 0

The output vectors are orthonormal: the pairing is the equality indicator.

theorem QuantumQueryComplexity.commonVec_dotProduct_outVec {R : Type} [Fintype R] [DecidableEq R] (r : R) : commonVec ⬝ᵥ outVec r = 0

The common and output vectors are orthogonal.

theorem QuantumQueryComplexity.outVec_dotProduct_commonVec {R : Type} [Fintype R] [DecidableEq R] (r : R) : outVec r ⬝ᵥ commonVec = 0

theorem QuantumQueryComplexity.smul_tPlus_add_tMinus {X O : Type} [DecidableEq O] (f : X → O) (x : X) : (√2)⁻¹ • (tPlus f x + tMinus f x) = commonVec

(t₊ + t₋)/√2 is exactly the common vector — the x-dependence cancels.

theorem QuantumQueryComplexity.smul_tPlus_sub_tMinus {X O : Type} [DecidableEq O] (f : X → O) (x : X) : (√2)⁻¹ • (tPlus f x - tMinus f x) = outVec (rangeElem f x)

(t₊ − t₋)/√2 is exactly the output-labelled vector.

The tagged query packets

The packet register is one Option σ block per pair (i, k) — every pair carries its own flag coordinate. A shared flag would make different blocks overlap, and the whole point of the construction is that they do not.

g_{i,k}         = idleFlag_{i,k} + activeBlank_{i,k}
leftAtom_{i,k,a}  = idleFlag_{i,k} + answer_{i,k,a}      (the oracle image)
rightAtom_{i,k,a} = idleFlag_{i,k} − answer_{i,k,a}

Inside a block these are exactly uniformLeft and uniformRight, so the [a ≠ b] factorization is inherited blockwise, and distinct blocks are orthogonal. The ambient space is the target register direct-summed with the packet blocks, which makes every target/packet cross term vanish by construction.

@[reducible, inline]

abbrev QuantumQueryComplexity.UBasis (R ι σ K : Type) : Type

The ambient index: the target register, direct-summed with one Option σ packet block per (i, k).

Equations

• QuantumQueryComplexity.UBasis R ι σ K = (Option R ⊕ (ι × K) × Option σ)

def QuantumQueryComplexity.uTarget {R ι σ K : Type} (t : Option R → ℝ) : UBasis R ι σ K → ℂ

A target-register vector, embedded.

Equations

• QuantumQueryComplexity.uTarget t = Sum.elim (fun (s : Option R) => ↑(t s)) fun (x : (ι × K) × Option σ) => 0

theorem QuantumQueryComplexity.uTarget_add {R ι σ K : Type} (t t' : Option R → ℝ) : uTarget (t + t') = uTarget t + uTarget t'

theorem QuantumQueryComplexity.uTarget_sub {R ι σ K : Type} (t t' : Option R → ℝ) : uTarget (t - t') = uTarget t - uTarget t'

theorem QuantumQueryComplexity.uTarget_realSmul {R ι σ K : Type} (r : ℝ) (t : Option R → ℝ) : uTarget (r • t) = ↑r • uTarget t

Real scaling of the target vector is complex scaling of its embedding.

def QuantumQueryComplexity.blockVec {R ι σ K : Type} [DecidableEq ι] [DecidableEq K] (p : ι × K) (w : Option σ → ℝ) : UBasis R ι σ K → ℂ

A real vector placed in the packet block p, zero elsewhere. Every block carries its own flag coordinate, which is what keeps distinct blocks orthogonal.

Equations

• QuantumQueryComplexity.blockVec p w = Sum.elim (fun (x : Option R) => 0) fun (q : (ι × K) × Option σ) => if q.1 = p then ↑(w q.2) else 0

theorem QuantumQueryComplexity.qInner_blockVec {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [DecidableEq K] (p p' : ι × K) (w w' : Option σ → ℝ) : qInner (blockVec p w) (blockVec p' w') = if p = p' then ↑(w ⬝ᵥ w') else 0

The one computation the packet layer needs: blocks are orthogonal, and inside a block the pairing is the real one.

def QuantumQueryComplexity.leftAtom {R ι σ K : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq K] (i : ι) (k : K) (a : σ) : UBasis R ι σ K → ℂ

idleFlag_{i,k} + answer_{i,k,a}: the oracle image of the tagged generator g_{i,k} = idleFlag_{i,k} + activeBlank_{i,k}.

Equations

• QuantumQueryComplexity.leftAtom i k a = QuantumQueryComplexity.blockVec (i, k) (QuantumQueryComplexity.uniformLeft a)

def QuantumQueryComplexity.rightAtom {R ι σ K : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq K] (i : ι) (k : K) (a : σ) : UBasis R ι σ K → ℂ

idleFlag_{i,k} − answer_{i,k,a}.

Equations

• QuantumQueryComplexity.rightAtom i k a = QuantumQueryComplexity.blockVec (i, k) (QuantumQueryComplexity.uniformRight a)

theorem QuantumQueryComplexity.qInner_leftAtom_rightAtom {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (i : ι) (k : K) (a : σ) (j : ι) (l : K) (b : σ) : qInner (leftAtom i k a) (rightAtom j l b) = if (i, k) = (j, l) then if a = b then 0 else 1 else 0

The blockwise factorization: distinct blocks are orthogonal, and inside a block the pairing is the inequality indicator.

theorem QuantumQueryComplexity.qInner_leftAtom_self {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (i : ι) (k : K) (a : σ) : qInner (leftAtom i k a) (leftAtom i k a) = 2

Each atom has squared norm 2 — independently of the alphabet.

theorem QuantumQueryComplexity.qInner_rightAtom_self {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (i : ι) (k : K) (a : σ) : qInner (rightAtom i k a) (rightAtom i k a) = 2

@[simp]

theorem QuantumQueryComplexity.qInner_uTarget_blockVec {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [DecidableEq K] (t : Option R → ℝ) (p : ι × K) (w : Option σ → ℝ) : qInner (uTarget t) (blockVec p w) = 0

Targets and packets never interfere: they sit in complementary summands.

@[simp]

theorem QuantumQueryComplexity.qInner_blockVec_uTarget {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [DecidableEq K] (p : ι × K) (w : Option σ → ℝ) (t : Option R → ℝ) : qInner (blockVec p w) (uTarget t) = 0

The packets of a dual solution

U_x and V_x are the two dual families spent against the tagged atoms — u on the left (oracle images), v on the right — without swapping the families. One bilinear computation (qInner_sum_blockVec) serves both the cross pairing and the norms, exactly as qInner_blockVec served the atoms.

theorem QuantumQueryComplexity.qInner_sum_blockVec {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [DecidableEq K] (c d : ι × K → ℝ) (w w' : ι × K → Option σ → ℝ) : qInner (∑ p : ι × K, ↑(c p) • blockVec p (w p)) (∑ p : ι × K, ↑(d p) • blockVec p (w' p)) = ↑(∑ p : ι × K, c p * d p * w p ⬝ᵥ w' p)

The one bilinear computation of the packet layer. Block-diagonal by construction, so only the diagonal survives.

noncomputable def QuantumQueryComplexity.packetU {R ι σ K X : Type} [Fintype ι] [DecidableEq ι] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : UBasis R ι σ K → ℂ

The left packet: the u-family against the oracle images.

Equations

• QuantumQueryComplexity.packetU u read x = ∑ p : ι × K, ↑(u x p.1 p.2) • QuantumQueryComplexity.blockVec p (QuantumQueryComplexity.uniformLeft (read x p.1))

noncomputable def QuantumQueryComplexity.packetV {R ι σ K X : Type} [Fintype ι] [DecidableEq ι] [DecidableEq σ] [Fintype K] [DecidableEq K] (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : UBasis R ι σ K → ℂ

The right packet: the v-family against the flipped atoms.

Equations

• QuantumQueryComplexity.packetV v read x = ∑ p : ι × K, ↑(v x p.1 p.2) • QuantumQueryComplexity.blockVec p (QuantumQueryComplexity.uniformRight (read x p.1))

theorem QuantumQueryComplexity.qInner_packetU_packetV {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (u v : X → ι → K → ℝ) (read : X → ι → σ) (y x : X) : qInner (packetU u read y) (packetV v read x) = ↑(∑ i : ι, if read y i = read x i then 0 else ∑ k : K, u y i k * v x i k)

The cross pairing is the dual constraint's left-hand side, verbatim and with the families unswapped.

theorem QuantumQueryComplexity.qInner_packetU_packetV_of_dualPairOn {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] {O : Type} [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (y x : X) : qInner (packetU P.u read y) (packetV P.v read x) = if f y = f x then 0 else 1

The same, evaluated on a feasible dual solution: the packets realise the inequality indicator of the outputs.

theorem QuantumQueryComplexity.qInner_packetU_self {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qInner (packetU u read x) (packetU u read x) = ↑(2 * ∑ p : ι × K, u x p.1 p.2 * u x p.1 p.2)

The exact norms: ‖U_x‖² = 2·∑ u², no alphabet anywhere.

theorem QuantumQueryComplexity.qInner_packetV_self {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qInner (packetV v read x) (packetV v read x) = ↑(2 * ∑ p : ι × K, v x p.1 p.2 * v x p.1 p.2)

@[simp]

theorem QuantumQueryComplexity.qInner_uTarget_packetU {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (t : Option R → ℝ) (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qInner (uTarget t) (packetU u read x) = 0

Targets never meet packets.

@[simp]

theorem QuantumQueryComplexity.qInner_uTarget_packetV {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (t : Option R → ℝ) (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qInner (uTarget t) (packetV v read x) = 0

@[simp]

theorem QuantumQueryComplexity.qInner_packetU_uTarget {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) (t : Option R → ℝ) : qInner (packetU u read x) (uTarget t) = 0

Two convenience pairings

qInner_uTarget_uTarget transfers every target norm and overlap from the real computation of the first section without repeating the real-to-complex step; qInner_packetV_uTarget makes the ‖φ‖² expansion symmetric.

@[simp]

theorem QuantumQueryComplexity.qInner_uTarget_uTarget {R ι σ K : Type} [Fintype R] [Fintype ι] [Fintype σ] [Fintype K] (t t' : Option R → ℝ) : qInner (uTarget t) (uTarget t') = ↑(t ⬝ᵥ t')

@[simp]

theorem QuantumQueryComplexity.qInner_packetV_uTarget {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) (t : Option R → ℝ) : qInner (packetV v read x) (uTarget t) = 0

Operational realization

UBasis is an abstract Hilbert basis: it cannot be handed to oracleMat or inputProj, which live on QBasis. The realization places it inside a genuine query basis whose workspace is

UWork R ι K = Option R ⊕ (ι × K)

— the target register, or the name of a packet block — by

target s            ↦ (none,   none,   Sum.inl s)
block (i,k), ⊥      ↦ (none,   none,   Sum.inr (i,k))
block (i,k), some a ↦ (some i, some a, Sum.inr (i,k))

so a block's flag coordinate is idle (no index queried) and its answer coordinates are active at the block's own index. That is exactly what makes the oracle carry the physical generator

gen (i,k) = |⊥, ⊥, (i,k)⟩ + |i, ⊥, (i,k)⟩

onto the leftAtom packet: the second summand is the active-blank register, which the transposition oracle fills with some (a i).

The embedding is injective but not surjective; uRealize extends by zero, which is why it preserves qInner and qNormSq on the nose.

@[reducible, inline]

abbrev QuantumQueryComplexity.UWork (R ι K : Type) : Type

The workspace of the realized space: the target register, or the name of a packet block.

Equations

• QuantumQueryComplexity.UWork R ι K = (Option R ⊕ ι × K)

@[instance_reducible]

instance QuantumQueryComplexity.instUWorkDecidableEq {R ι K : Type} [DecidableEq R] [DecidableEq ι] [DecidableEq K] : DecidableEq (UWork R ι K)

Equations

• QuantumQueryComplexity.instUWorkDecidableEq a b = instDecidableEqSum a b

@[instance_reducible]

instance QuantumQueryComplexity.instUWorkFintype {R ι K : Type} [Fintype R] [Fintype ι] [Fintype K] : Fintype (UWork R ι K)

Equations

• QuantumQueryComplexity.instUWorkFintype = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }

@[reducible, inline]

abbrev QuantumQueryComplexity.UQBasis (R ι σ K : Type) : Type

The realized query basis.

Equations

• QuantumQueryComplexity.UQBasis R ι σ K = QuantumQueryComplexity.QBasis ι σ (QuantumQueryComplexity.UWork R ι K)

def QuantumQueryComplexity.uRealize {R ι σ K : Type} [DecidableEq ι] (ψ : UBasis R ι σ K → ℂ) : UQBasis R ι σ K → ℂ

The realization: place an abstract vector in the query basis, extending by zero off the embedded coordinates.

Equations

• QuantumQueryComplexity.uRealize ψ (none, none, Sum.inl s) = ψ (Sum.inl s)
• QuantumQueryComplexity.uRealize ψ (none, none, Sum.inr p) = ψ (Sum.inr (p, none))
• QuantumQueryComplexity.uRealize ψ (some i, some a, Sum.inr p) = if p.1 = i then ψ (Sum.inr (p, some a)) else 0
• QuantumQueryComplexity.uRealize ψ q = 0

@[simp]

theorem QuantumQueryComplexity.uRealize_target {R ι σ K : Type} [DecidableEq ι] (ψ : UBasis R ι σ K → ℂ) (s : Option R) : uRealize ψ (none, none, Sum.inl s) = ψ (Sum.inl s)

@[simp]

theorem QuantumQueryComplexity.uRealize_flag {R ι σ K : Type} [DecidableEq ι] (ψ : UBasis R ι σ K → ℂ) (p : ι × K) : uRealize ψ (none, none, Sum.inr p) = ψ (Sum.inr (p, none))

@[simp]

theorem QuantumQueryComplexity.uRealize_answer {R ι σ K : Type} [DecidableEq ι] (ψ : UBasis R ι σ K → ℂ) (i : ι) (a : σ) (p : ι × K) : uRealize ψ (some i, some a, Sum.inr p) = if p.1 = i then ψ (Sum.inr (p, some a)) else 0

def QuantumQueryComplexity.uEmb {R ι σ K : Type} : UBasis R ι σ K → UQBasis R ι σ K

The embedding itself, as a function. Its image is not oracle-invariant: the oracle swaps a realized answer coordinate with the active-blank coordinate (some i, none, Sum.inr (i,k)), which is deliberately outside the image. So there is no general theorem oracleMat a *ᵥ uRealize ψ = uRealize (…) — that statement is false, and only the generator-specific identities below hold.

Equations

• QuantumQueryComplexity.uEmb (Sum.inl s) = (none, none, Sum.inl s)
• QuantumQueryComplexity.uEmb (Sum.inr (p, none)) = (none, none, Sum.inr p)
• QuantumQueryComplexity.uEmb (Sum.inr (p, some a)) = (some p.1, some a, Sum.inr p)

@[simp]

theorem QuantumQueryComplexity.uRealize_uEmb {R ι σ K : Type} [DecidableEq ι] (ψ : UBasis R ι σ K → ℂ) (b : UBasis R ι σ K) : uRealize ψ (uEmb b) = ψ b

theorem QuantumQueryComplexity.uEmb_injective {R ι σ K : Type} : Function.Injective uEmb

theorem QuantumQueryComplexity.uRealize_eq_zero_of_forall_ne {R ι σ K : Type} [DecidableEq ι] (ψ : UBasis R ι σ K → ℂ) {q : UQBasis R ι σ K} (h : ∀ (b : UBasis R ι σ K), uEmb b ≠ q) : uRealize ψ q = 0

Off the image the realization vanishes — which is what makes it an isometry.

theorem QuantumQueryComplexity.qInner_uRealize {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] (ψ φ : UBasis R ι σ K → ℂ) : qInner (uRealize ψ) (uRealize φ) = qInner ψ φ

The master isometry.

theorem QuantumQueryComplexity.qNormSq_uRealize {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] (ψ : UBasis R ι σ K → ℂ) : qNormSq (uRealize ψ) = qNormSq ψ

@[simp]

theorem QuantumQueryComplexity.uRealize_zero {R ι σ K : Type} [DecidableEq ι] : uRealize 0 = 0

theorem QuantumQueryComplexity.uRealize_add {R ι σ K : Type} [DecidableEq ι] (ψ φ : UBasis R ι σ K → ℂ) : uRealize (ψ + φ) = uRealize ψ + uRealize φ

theorem QuantumQueryComplexity.uRealize_sub {R ι σ K : Type} [DecidableEq ι] (ψ φ : UBasis R ι σ K → ℂ) : uRealize (ψ - φ) = uRealize ψ - uRealize φ

theorem QuantumQueryComplexity.uRealize_sum {R ι σ K : Type} [DecidableEq ι] {α : Type u_1} (s : Finset α) (F : α → UBasis R ι σ K → ℂ) : uRealize (∑ a ∈ s, F a) = ∑ a ∈ s, uRealize (F a)

theorem QuantumQueryComplexity.uRealize_smul {R ι σ K : Type} [DecidableEq ι] (c : ℂ) (ψ : UBasis R ι σ K → ℂ) : uRealize (c • ψ) = c • uRealize ψ

The physical generator

idleFlag p     = |⊥, ⊥, p⟩
activeBlank p  = |p.1, ⊥, p⟩
uniformGen p   = idleFlag p + activeBlank p

The oracle fixes the idle summand (no index is queried there) and fills the active blank with some (a p.1), so it carries the generator exactly onto the realized leftAtom packet. This is the generator-specific transport identity the construction uses — arbitrary uRealize transport is false (the image is not oracle-invariant, and the active-blank coordinate is precisely the off-image coordinate the oracle uses), though linear combinations of generator identities of course still hold.

def QuantumQueryComplexity.idleFlag {R ι σ K : Type} [DecidableEq R] [DecidableEq ι] [DecidableEq σ] [DecidableEq K] (p : ι × K) : UQBasis R ι σ K → ℂ

|⊥, ⊥, p⟩ — the block's flag, idle.

Equations

• QuantumQueryComplexity.idleFlag p = QuantumQueryComplexity.qBasis (none, none, Sum.inr p)

def QuantumQueryComplexity.activeBlank {R ι σ K : Type} [DecidableEq R] [DecidableEq ι] [DecidableEq σ] [DecidableEq K] (p : ι × K) : UQBasis R ι σ K → ℂ

|p.1, ⊥, p⟩ — the block's blank answer register, active at its own index. Outside the image of uRealize, by design.

Equations

• QuantumQueryComplexity.activeBlank p = QuantumQueryComplexity.qBasis (some p.1, none, Sum.inr p)

def QuantumQueryComplexity.uniformGen {R ι σ K : Type} [DecidableEq R] [DecidableEq ι] [DecidableEq σ] [DecidableEq K] (p : ι × K) : UQBasis R ι σ K → ℂ

The tagged generator g_{i,k}.

Equations

• QuantumQueryComplexity.uniformGen p = QuantumQueryComplexity.idleFlag p + QuantumQueryComplexity.activeBlank p

theorem QuantumQueryComplexity.uRealize_leftAtom {R ι σ K : Type} [DecidableEq R] [DecidableEq ι] [DecidableEq σ] [DecidableEq K] (i : ι) (k : K) (c : σ) : uRealize (leftAtom i k c) = qBasis (none, none, Sum.inr (i, k)) + qBasis (some i, some c, Sum.inr (i, k))

The realized leftAtom is a two-term basis sum.

theorem QuantumQueryComplexity.oracleMat_mulVec_uniformGen {R ι σ K : Type} [Fintype R] [DecidableEq R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (a : ι → σ) (p : ι × K) : (oracleMat a).mulVec (uniformGen p) = uRealize (leftAtom p.1 p.2 (a p.1))

The generator-specific transport identity.

theorem QuantumQueryComplexity.qInner_uniformGen_oracle_uRealize {R ι σ K : Type} [Fintype R] [DecidableEq R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (a : ι → σ) (p : ι × K) (ψ : UBasis R ι σ K → ℂ) : qInner (uniformGen p) ((oracleMat a).mulVec (uRealize ψ)) = qInner (leftAtom p.1 p.2 (a p.1)) ψ

The scalar pullback the projector proof consumes: testing a realized vector against a generator, through the oracle, is testing it against the leftAtom packet.

theorem QuantumQueryComplexity.qInner_leftAtom_packetV_same {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] {X : Type} (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) (i : ι) (k : K) : qInner (leftAtom i k (read x i)) (packetV v read x) = 0

The per-generator cancellation. inputProj asks orthogonality against each generator separately, so the aggregate ⟪U, V⟫ identity is not enough: this is the statement that on the same input the letters agree in every block, so every term of V_x is killed.

The realized states, and their contracts

Named realized states, with their pairings and norms transported through the isometry immediately — after this section nothing downstream needs to know how the realization is built.

noncomputable def QuantumQueryComplexity.realizedTarget {R ι σ K : Type} [DecidableEq ι] (t : Option R → ℝ) : UQBasis R ι σ K → ℂ

A realized target state.

Equations

• QuantumQueryComplexity.realizedTarget t = QuantumQueryComplexity.uRealize (QuantumQueryComplexity.uTarget t)

noncomputable def QuantumQueryComplexity.realizedPacketU {R ι σ K X : Type} [Fintype ι] [DecidableEq ι] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : UQBasis R ι σ K → ℂ

The realized u-packet.

Equations

• QuantumQueryComplexity.realizedPacketU u read x = QuantumQueryComplexity.uRealize (QuantumQueryComplexity.packetU u read x)

noncomputable def QuantumQueryComplexity.realizedPacketV {R ι σ K X : Type} [Fintype ι] [DecidableEq ι] [DecidableEq σ] [Fintype K] [DecidableEq K] (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : UQBasis R ι σ K → ℂ

The realized v-packet.

Equations

• QuantumQueryComplexity.realizedPacketV v read x = QuantumQueryComplexity.uRealize (QuantumQueryComplexity.packetV v read x)

Transported pairings and norms

@[simp]

theorem QuantumQueryComplexity.qInner_realizedTarget {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] (t t' : Option R → ℝ) : qInner (realizedTarget t) (realizedTarget t') = ↑(t ⬝ᵥ t')

@[simp]

theorem QuantumQueryComplexity.qInner_realizedTarget_realizedPacketU {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (t : Option R → ℝ) (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qInner (realizedTarget t) (realizedPacketU u read x) = 0

@[simp]

theorem QuantumQueryComplexity.qInner_realizedTarget_realizedPacketV {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (t : Option R → ℝ) (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qInner (realizedTarget t) (realizedPacketV v read x) = 0

@[simp]

theorem QuantumQueryComplexity.qInner_realizedPacketU_realizedTarget {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) (t : Option R → ℝ) : qInner (realizedPacketU u read x) (realizedTarget t) = 0

@[simp]

theorem QuantumQueryComplexity.qInner_realizedPacketV_realizedTarget {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) (t : Option R → ℝ) : qInner (realizedPacketV v read x) (realizedTarget t) = 0

theorem QuantumQueryComplexity.qInner_realizedPacketU_realizedPacketV {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] {O : Type} [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (y x : X) : qInner (realizedPacketU P.u read y) (realizedPacketV P.v read x) = if f y = f x then 0 else 1

theorem QuantumQueryComplexity.qInner_realizedPacketU_self {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qInner (realizedPacketU u read x) (realizedPacketU u read x) = ↑(2 * ∑ p : ι × K, u x p.1 p.2 * u x p.1 p.2)

theorem QuantumQueryComplexity.qInner_realizedPacketV_self {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qInner (realizedPacketV v read x) (realizedPacketV v read x) = ↑(2 * ∑ p : ι × K, v x p.1 p.2 * v x p.1 p.2)

The operational form of the u-packet

theorem QuantumQueryComplexity.realizedPacketU_eq_sum_oracleGen {R ι σ K X : Type} [Fintype R] [DecidableEq R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : realizedPacketU u read x = (oracleMat (read x)).mulVec (∑ p : ι × K, ↑(u x p.1 p.2) • uniformGen p)

The u-packet is the oracle applied to a combination of generators. This is what puts it inside the killed space of inputProj.

The projector contracts

theorem QuantumQueryComplexity.inputProj_mulVec_realizedPacketU {R ι σ K X : Type} [Fintype R] [DecidableEq R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : (inputProj uniformGen (read x)).mulVec (realizedPacketU u read x) = 0

The u-packet is killed.

theorem QuantumQueryComplexity.inputProj_mulVec_realizedPacketV {R ι σ K X : Type} [Fintype R] [DecidableEq R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : (inputProj uniformGen (read x)).mulVec (realizedPacketV v read x) = realizedPacketV v read x

The v-packet is fixed.

theorem QuantumQueryComplexity.inputProj_mulVec_realizedTarget {R ι σ K : Type} [Fintype R] [DecidableEq R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (t : Option R → ℝ) (a : ι → σ) : (inputProj uniformGen a).mulVec (realizedTarget t) = realizedTarget t

Targets are fixed.

Real-valued norm corollaries

theorem QuantumQueryComplexity.qNormSq_realizedTarget {R ι σ K : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] (t : Option R → ℝ) : qNormSq (realizedTarget t) = t ⬝ᵥ t

theorem QuantumQueryComplexity.qNormSq_realizedPacketU {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (u : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qNormSq (realizedPacketU u read x) = 2 * ∑ p : ι × K, u x p.1 p.2 * u x p.1 p.2

theorem QuantumQueryComplexity.qNormSq_realizedPacketV {R ι σ K X : Type} [Fintype R] [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (v : X → ι → K → ℝ) (read : X → ι → σ) (x : X) : qNormSq (realizedPacketV v read x) = 2 * ∑ p : ι × K, v x p.1 p.2 * v x p.1 p.2

The scaled witnesses

φ_x = t_{x+} + α·V_x
w_x = t_{x−} − (2α)⁻¹·U_x
ψ_x = 2α·t_{x−} − U_x  ( = 2α·w_x when α ≠ 0)

α : ℝ, deliberately: a complex scaling would drag conjugation into the cancellation. ⟪ψ_y, φ_x⟫ = 0 holds for every α: the target term contributes 2α · ½·[f y ≠ f x] = α·[f y ≠ f x], and the packet term contributes α · ⟪U_y, V_x⟫ = α·[f y ≠ f x], with opposite signs.

One global projector L = spanProj (uniformPhi P α) indexed by all promise inputs — not one per output.

noncomputable def QuantumQueryComplexity.realizedTPlus {ι σ K X O : Type} [DecidableEq ι] [DecidableEq O] (f : X → O) (x : X) : UQBasis (↑(Set.range f)) ι σ K → ℂ

The realized + target.

Equations

• QuantumQueryComplexity.realizedTPlus f x = QuantumQueryComplexity.realizedTarget (QuantumQueryComplexity.tPlus f x)

noncomputable def QuantumQueryComplexity.realizedTMinus {ι σ K X O : Type} [DecidableEq ι] [DecidableEq O] (f : X → O) (x : X) : UQBasis (↑(Set.range f)) ι σ K → ℂ

The realized − target.

Equations

• QuantumQueryComplexity.realizedTMinus f x = QuantumQueryComplexity.realizedTarget (QuantumQueryComplexity.tMinus f x)

noncomputable def QuantumQueryComplexity.uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : UQBasis (↑(Set.range f)) ι σ K → ℂ

φ_x = t_{x+} + α·V_x.

Equations

• QuantumQueryComplexity.uniformPhi P α x = QuantumQueryComplexity.realizedTPlus f x + ↑α • QuantumQueryComplexity.realizedPacketV P.v read x

noncomputable def QuantumQueryComplexity.uniformW {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : UQBasis (↑(Set.range f)) ι σ K → ℂ

w_x = t_{x−} − (2α)⁻¹·U_x.

Equations

• QuantumQueryComplexity.uniformW P α x = QuantumQueryComplexity.realizedTMinus f x - ↑(2 * α)⁻¹ • QuantumQueryComplexity.realizedPacketU P.u read x

noncomputable def QuantumQueryComplexity.uniformPsi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : UQBasis (↑(Set.range f)) ι σ K → ℂ

ψ_x = 2α·t_{x−} − U_x.

Equations

• QuantumQueryComplexity.uniformPsi P α x = ↑(2 * α) • QuantumQueryComplexity.realizedTMinus f x - QuantumQueryComplexity.realizedPacketU P.u read x

theorem QuantumQueryComplexity.qInner_uniformPsi_uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (y x : X) : qInner (uniformPsi P α y) (uniformPhi P α x) = 0

The exact orthogonality, for every α.

theorem QuantumQueryComplexity.uniformPsi_eq_twoAlpha_smul_uniformW {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (x : X) : uniformPsi P α x = ↑(2 * α) • uniformW P α x

ψ = 2α·w once α ≠ 0.

theorem QuantumQueryComplexity.qInner_uniformW_uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (y x : X) : qInner (uniformW P α y) (uniformPhi P α x) = 0

Hence ⟪w_y, φ_x⟫ = 0 for α ≠ 0.

theorem QuantumQueryComplexity.qInner_uniformPhi_uniformW {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (y x : X) : qInner (uniformPhi P α y) (uniformW P α x) = 0

The reversed pairing, by conjugation.

noncomputable def QuantumQueryComplexity.uniformL {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) : Matrix (UQBasis (↑(Set.range f)) ι σ K) (UQBasis (↑(Set.range f)) ι σ K) ℂ

The global projector, indexed by all promise inputs.

Equations

• QuantumQueryComplexity.uniformL P α = QuantumQueryComplexity.spanProj (QuantumQueryComplexity.uniformPhi P α)

theorem QuantumQueryComplexity.isQProjector_uniformL {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) : IsQProjector (uniformL P α)

theorem QuantumQueryComplexity.uniformL_mulVec_uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : (uniformL P α).mulVec (uniformPhi P α x) = uniformPhi P α x

theorem QuantumQueryComplexity.uniformL_mulVec_uniformW {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (x : X) : (uniformL P α).mulVec (uniformW P α x) = 0

The exact norms

Orthogonality of target and packet makes both a Pythagorean sum.

theorem QuantumQueryComplexity.qNormSq_uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : qNormSq (uniformPhi P α x) = 1 + 2 * α ^ 2 * ∑ p : ι × K, P.v x p.1 p.2 * P.v x p.1 p.2

‖φ_x‖² = 1 + 2α²·(the v-mass) — no hypothesis on α.

theorem QuantumQueryComplexity.qNormSq_uniformPhi_le {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) (α : ℝ) (x : X) : qNormSq (uniformPhi P α x) ≤ 1 + 2 * α ^ 2 * c

theorem QuantumQueryComplexity.qNormSq_uniformW {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : qNormSq (uniformW P α x) = 1 + (2 * α)⁻¹ ^ 2 * (2 * ∑ p : ι × K, P.u x p.1 p.2 * P.u x p.1 p.2)

‖w_x‖² = 1 + (2α)⁻²·2·(the u-mass) — valid for every α (at α = 0 the inverse is 0, so this reads ‖w‖² = 1).

theorem QuantumQueryComplexity.qNormSq_uniformW_of_ne_zero {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (x : X) : qNormSq (uniformW P α x) = 1 + (∑ p : ι × K, P.u x p.1 p.2 * P.u x p.1 p.2) / (2 * α ^ 2)

The displayed form, for α ≠ 0.

theorem QuantumQueryComplexity.qNormSq_uniformW_le {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) {α : ℝ} (hα : α ≠ 0) (x : X) : qNormSq (uniformW P α x) ≤ 1 + c / (2 * α ^ 2)

The input-projector contracts

theorem QuantumQueryComplexity.inputProj_mulVec_uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : (inputProj uniformGen (read x)).mulVec (uniformPhi P α x) = uniformPhi P α x

theorem QuantumQueryComplexity.inputProj_mulVec_uniformW {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : (inputProj uniformGen (read x)).mulVec (uniformW P α x) = realizedTMinus f x

theorem QuantumQueryComplexity.isPosWitness_uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : IsPosWitness uniformGen (uniformL P α) (read x) (uniformPhi P α x)

φ is a positive witness.

Realized-target wrappers

@[simp]

theorem QuantumQueryComplexity.qNormSq_realizedTPlus {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x : X) : qNormSq (realizedTPlus f x) = 1

@[simp]

theorem QuantumQueryComplexity.qNormSq_realizedTMinus {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x : X) : qNormSq (realizedTMinus f x) = 1

theorem QuantumQueryComplexity.qInner_realizedTPlus_realizedTMinus {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x y : X) : qInner (realizedTPlus f x) (realizedTMinus f y) = if f x = f y then 0 else ↑(1 / 2)

t₊ ⟂ t₋ on matching outputs — in particular for the same input.

theorem QuantumQueryComplexity.qInner_realizedTMinus_realizedTPlus {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x y : X) : qInner (realizedTMinus f x) (realizedTPlus f y) = if f y = f x then 0 else ↑(1 / 2)

@[simp]

theorem QuantumQueryComplexity.qInner_realizedTPlus_realizedTMinus_self {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x : X) : qInner (realizedTPlus f x) (realizedTMinus f x) = 0

@[simp]

theorem QuantumQueryComplexity.qInner_realizedTMinus_realizedTPlus_self {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x : X) : qInner (realizedTMinus f x) (realizedTPlus f x) = 0

theorem QuantumQueryComplexity.qInner_realizedTPlus_uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (x : X) : qInner (realizedTPlus f x) (uniformPhi P α x) = 1

The target overlap the readout reads: ⟪t_{x+}, φ_x⟫ = 1.

The common and output states, realized

The conversion's initial state is input-independent; its target is labelled by the output alone. Both are unit vectors, and distinct outputs give orthogonal targets — the coherent readout geometry, with no cardinality of O anywhere.

noncomputable def QuantumQueryComplexity.realizedCommon {ι σ K X O : Type} [DecidableEq ι] (f : X → O) : UQBasis (↑(Set.range f)) ι σ K → ℂ

The realized common initial state.

Equations

• QuantumQueryComplexity.realizedCommon f = QuantumQueryComplexity.realizedTarget QuantumQueryComplexity.commonVec

noncomputable def QuantumQueryComplexity.realizedOut {ι σ K X O : Type} [DecidableEq ι] [DecidableEq O] (f : X → O) (x : X) : UQBasis (↑(Set.range f)) ι σ K → ℂ

The realized output-labelled target state.

Equations

• QuantumQueryComplexity.realizedOut f x = QuantumQueryComplexity.realizedTarget (QuantumQueryComplexity.outVec (QuantumQueryComplexity.rangeElem f x))

theorem QuantumQueryComplexity.realizedCommon_eq_smul {ι σ K X O : Type} [DecidableEq ι] [DecidableEq O] (f : X → O) (x : X) : realizedCommon f = ↑(√2)⁻¹ • (realizedTPlus f x + realizedTMinus f x)

common = (t₊ + t₋)/√2, realized — for every x.

theorem QuantumQueryComplexity.realizedOut_eq_smul {ι σ K X O : Type} [DecidableEq ι] [DecidableEq O] (f : X → O) (x : X) : realizedOut f x = ↑(√2)⁻¹ • (realizedTPlus f x - realizedTMinus f x)

out(f x) = (t₊ − t₋)/√2, realized.

@[simp]

theorem QuantumQueryComplexity.qNormSq_realizedCommon {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) : qNormSq (realizedCommon f) = 1

@[simp]

theorem QuantumQueryComplexity.qNormSq_realizedOut {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x : X) : qNormSq (realizedOut f x) = 1

theorem QuantumQueryComplexity.qInner_realizedOut_realizedOut {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x y : X) : qInner (realizedOut f x) (realizedOut f y) = if f x = f y then 1 else 0

The output states are labelled by the output: the overlap is the equality indicator, which is what the final readout measures.

@[simp]

theorem QuantumQueryComplexity.qInner_realizedCommon_realizedOut {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x : X) : qInner (realizedCommon f) (realizedOut f x) = 0

@[simp]

theorem QuantumQueryComplexity.qInner_realizedOut_realizedCommon {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] [Fintype X] [DecidableEq O] (f : X → O) (x : X) : qInner (realizedOut f x) (realizedCommon f) = 0

theorem QuantumQueryComplexity.realizedOut_apply_of_ne {ι σ K X O : Type} [DecidableEq ι] [DecidableEq O] (f : X → O) (x : X) {q : UQBasis (↑(Set.range f)) ι σ K} (hq : q.2.2 ≠ Sum.inl (some (rangeElem f x))) : realizedOut f x q = 0

The output state is supported on its own label: off the target coordinate (⊥, ⊥, inl (some (f x))) the realized output state vanishes. This is exactly what the final readout consumes.

The witness states, built from a dual adversary solution

From a DualPairOn read K f this section constructs the generators, the fixed subspace, and both witness families, and discharges the IsPosWitness contracts from the dual's feasibility identity.

The layout

The workspace is Option K: the dual's register, plus a slot none used as a flag. Three kinds of basis point matter, and the oracle is what separates them:

τ         = (none, none, none)              the target, in the idle sector
b i k     = (some i, none, some k)          blank answer — the generators
e i s k   = (some i, some s, some k)        the answer register holds `s`

The generators are the blank-answer states b i k. That single choice is what makes the whole construction work, because the transposition oracle sends

O_x (b i k) = e i (read x i) k,

so span {O_x · gen} is the span of the true-answer states of x — the input-dependent subspace, produced by conjugation rather than by fiat. By inputProj_mulVec_eq_self_iff, a state is fixed by inputProj gen (read x) exactly when it vanishes at every true-answer point of x.

The two witnesses

posWitness x = τ  -  ∑_{i,k} u x i k · (∑_{s ≠ read x i} e i s k)
negWitness y = τ  +  ∑_{i,k} v y i k · e i (read y i) k

The positive witness puts the dual's u x on every false answer letter, so it vanishes on the true-answer points of x and the first contract is immediate. The negative witness puts the dual's v y on the true answer letters of y, so it is τ plus a correction supported exactly where inputProj gen (read y) kills.

They meet only where the two inputs disagree, and there the dual's feasibility identity

∑ i, [read x i ≠ read y i] · ∑ k, u x i k · v y i k  =  [f x ≠ f y]

says precisely what is needed:

⟪posWitness x, negWitness y⟫ = 1 - [f x ≠ f y] = [f x = f y].

So distinct outputs give orthogonal witnesses. Taking L to be the projector onto the span of the positive witnesses of the inputs with f x = o then fixes every positive witness and annihilates every negative one — the two IsPosWitness contracts, and the negative side's L *ᵥ w = 0, all from one inner product.

The |σ| - 1 in qNormSq_posWitness is the price of spreading u x i k over every false letter: the construction cannot know which letter y will read. It is 1 for a Boolean alphabet.

States of the construction's shape

Every state below is α on the target and A i s k on the answer-letter points. Proving the inner product and the norm once, for this shape, is what keeps the rest of the file free of basis manipulation.

def QuantumQueryComplexity.scState {ι σ K : Type} (α : ℂ) (A : ι → σ → K → ℂ) : QBasis ι σ (Option K) → ℂ

A state of the construction's shape.

Equations

• QuantumQueryComplexity.scState α A (none, none, none) = α
• QuantumQueryComplexity.scState α A (some i, some s, some k) = A i s k
• QuantumQueryComplexity.scState α A x✝ = 0

@[simp]

theorem QuantumQueryComplexity.scState_target {ι σ K : Type} (α : ℂ) (A : ι → σ → K → ℂ) : scState α A (none, none, none) = α

@[simp]

theorem QuantumQueryComplexity.scState_letter {ι σ K : Type} (α : ℂ) (A : ι → σ → K → ℂ) (i : ι) (s : σ) (k : K) : scState α A (some i, some s, some k) = A i s k

@[simp]

theorem QuantumQueryComplexity.scState_idle_reg {ι σ K : Type} (α : ℂ) (A : ι → σ → K → ℂ) (k : K) : scState α A (none, none, some k) = 0

@[simp]

theorem QuantumQueryComplexity.scState_idle_letter {ι σ K : Type} (α : ℂ) (A : ι → σ → K → ℂ) (s : σ) (w : Option K) : scState α A (none, some s, w) = 0

@[simp]

theorem QuantumQueryComplexity.scState_blank {ι σ K : Type} (α : ℂ) (A : ι → σ → K → ℂ) (i : ι) (w : Option K) : scState α A (some i, none, w) = 0

@[simp]

theorem QuantumQueryComplexity.scState_flag {ι σ K : Type} (α : ℂ) (A : ι → σ → K → ℂ) (i : ι) (s : σ) : scState α A (some i, some s, none) = 0

theorem QuantumQueryComplexity.qInner_scState {ι σ K : Type} [Fintype ι] [Fintype σ] [Fintype K] (α β : ℂ) (A B : ι → σ → K → ℂ) : qInner (scState α A) (scState β B) = star α * β + ∑ i : ι, ∑ s : σ, ∑ k : K, star (A i s k) * B i s k

The inner product of two states of this shape.

theorem QuantumQueryComplexity.qNormSq_scState {ι σ K : Type} [Fintype ι] [Fintype σ] [Fintype K] (α : ℂ) (A : ι → σ → K → ℂ) : qNormSq (scState α A) = Complex.normSq α + ∑ i : ι, ∑ s : σ, ∑ k : K, Complex.normSq (A i s k)

The squared norm of a state of this shape.

theorem QuantumQueryComplexity.scState_add {ι σ K : Type} (α β : ℂ) (A B : ι → σ → K → ℂ) : (scState (α + β) fun (i : ι) (s : σ) (k : K) => A i s k + B i s k) = scState α A + scState β B

The generators and the target

def QuantumQueryComplexity.scGen {ι σ K : Type} [DecidableEq ι] [DecidableEq σ] [DecidableEq K] : ι × K → QBasis ι σ (Option K) → ℂ

The generators: the blank-answer states, one per index and dual register.

Equations

• QuantumQueryComplexity.scGen j = QuantumQueryComplexity.qBasis (some j.1, none, some j.2)

def QuantumQueryComplexity.scTarget {ι σ K : Type} : QBasis ι σ (Option K) → ℂ

The target: the flag state of the idle sector.

Equations

• QuantumQueryComplexity.scTarget = QuantumQueryComplexity.scState 1 fun (x : ι) (x_1 : σ) (x_2 : K) => 0

theorem QuantumQueryComplexity.qInner_qBasis_left {H : Type} [Fintype H] [DecidableEq H] (p : H) (ψ : H → ℂ) : qInner (qBasis p) ψ = ψ p

theorem QuantumQueryComplexity.qInner_scGen_oracle {ι σ K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (a : ι → σ) (φ : QBasis ι σ (Option K) → ℂ) (i : ι) (k : K) : qInner (scGen (i, k)) ((oracleMat a).mulVec φ) = φ (some i, some (a i), some k)

What the generators test. Pairing a generator against a state read through the oracle picks out the amplitude at a true-answer point.

theorem QuantumQueryComplexity.inputProj_scGen_mulVec_eq_self_iff {ι σ K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] (a : ι → σ) (φ : QBasis ι σ (Option K) → ℂ) : (inputProj scGen a).mulVec φ = φ ↔ ∀ (i : ι) (k : K), φ (some i, some (a i), some k) = 0

Being fixed by the input projector is vanishing on the true answers.

The two witness families

def QuantumQueryComplexity.posWitness {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (x : X) : QBasis ι σ (Option K) → ℂ

The positive witness for x: the target, minus the dual's u x spread over every false answer letter.

Equations

• QuantumQueryComplexity.posWitness read f P x = QuantumQueryComplexity.scState 1 fun (i : ι) (s : σ) (k : K) => if s = read x i then 0 else -↑(P.u x i k)

def QuantumQueryComplexity.negWitness {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (y : X) : QBasis ι σ (Option K) → ℂ

The negative witness for y: the target, plus the dual's v y on the true answer letters.

Equations

• QuantumQueryComplexity.negWitness read f P y = QuantumQueryComplexity.scState 1 fun (i : ι) (s : σ) (k : K) => if s = read y i then ↑(P.v y i k) else 0

def QuantumQueryComplexity.negCorr {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (y : X) : QBasis ι σ (Option K) → ℂ

The negative witness's correction term, supported exactly on the true-answer points of y.

Equations

• QuantumQueryComplexity.negCorr read f P y = QuantumQueryComplexity.scState 0 fun (i : ι) (s : σ) (k : K) => if s = read y i then ↑(P.v y i k) else 0

theorem QuantumQueryComplexity.negWitness_eq_target_add {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (y : X) : negWitness read f P y = scTarget + negCorr read f P y

The dual constraint, as an inner product

The one computation the construction rests on.

theorem QuantumQueryComplexity.qInner_posWitness_negWitness {ι σ X O K : Type} [Fintype ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (x y : X) : qInner (posWitness read f P x) (negWitness read f P y) = if f x = f y then 1 else 0

Distinct outputs give orthogonal witnesses. This is the dual's feasibility identity, read as an inner product.

The positive contracts

theorem QuantumQueryComplexity.inputProj_mulVec_posWitness {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (x : X) : (inputProj scGen (read x)).mulVec (posWitness read f P x) = posWitness read f P x

The positive witness vanishes on the true answers of its own input, which is the first contract.

noncomputable def QuantumQueryComplexity.scKer {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (o : O) : Matrix (QBasis ι σ (Option K)) (QBasis ι σ (Option K)) ℂ

The fixed subspace: the span of the positive witnesses of the inputs that f sends to o.

Equations

• QuantumQueryComplexity.scKer read f P o = QuantumQueryComplexity.subProj (QuantumQueryComplexity.rawSpan fun (x : { x : X // f x = o }) => QuantumQueryComplexity.posWitness read f P ↑x)

theorem QuantumQueryComplexity.isQProjector_scKer {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (o : O) : IsQProjector (scKer read f P o)

theorem QuantumQueryComplexity.scKer_mulVec_posWitness {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) {o : O} {x : X} (hx : f x = o) : (scKer read f P o).mulVec (posWitness read f P x) = posWitness read f P x

The fixed subspace fixes the positive witnesses, which is the second contract.

theorem QuantumQueryComplexity.isPosWitness_posWitness {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) {o : O} {x : X} (hx : f x = o) : IsPosWitness scGen (scKer read f P o) (read x) (posWitness read f P x)

Both contracts, so the detector of SourceQuantumInputDetector answers +1 on this witness exactly, at cost 4(T-1).

The negative side

theorem QuantumQueryComplexity.scKer_mulVec_negWitness {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) {o : O} {y : X} (hy : f y ≠ o) : (scKer read f P o).mulVec (negWitness read f P y) = 0

The fixed subspace annihilates the negative witnesses. This is the hypothesis effective_chord_gap_sq_inputReflProduct asks for, and it is exactly the orthogonality supplied by the dual constraint.

theorem QuantumQueryComplexity.mulVec_eq_zero_of_qInner_eq_zero {H : Type} [Fintype H] {P : Matrix H H ℂ} (hP : IsQProjector P) {ψ : H → ℂ} (h : qInner (P.mulVec ψ) ψ = 0) : P.mulVec ψ = 0

A projector kills anything orthogonal to its own image of that vector. This is the general fact; it is stated here because nothing upstream needs it yet.

theorem QuantumQueryComplexity.inputProj_mulVec_negCorr {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (y : X) : (inputProj scGen (read y)).mulVec (negCorr read f P y) = 0

The input projector kills the negative witness's correction term, which is supported exactly on the true-answer points it annihilates.

theorem QuantumQueryComplexity.inputProj_mulVec_negWitness {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (y : X) : (inputProj scGen (read y)).mulVec (negWitness read f P y) = scTarget

The negative witness is the target, up to what the input projector kills. This is the negative side's projected-direction obligation.

Overlap and norms

The exact algebra above says nothing about size; these are the estimates the query bound will consume.

theorem QuantumQueryComplexity.qInner_scTarget_posWitness {ι σ X O K : Type} [Fintype ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (x : X) : qInner scTarget (posWitness read f P x) = 1

The positive witness has overlap exactly 1 with the target. The correction term lives entirely off the target, so nothing is lost.

theorem QuantumQueryComplexity.qNormSq_negWitness {ι σ X O K : Type} [Fintype ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (y : X) : qNormSq (negWitness read f P y) = 1 + ∑ i : ι, ∑ k : K, P.v y i k * P.v y i k

The negative witness's norm is 1 plus the dual's v-mass.

theorem QuantumQueryComplexity.qNormSq_posWitness {ι σ X O K : Type} [Fintype ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (x : X) : qNormSq (posWitness read f P x) = 1 + ∑ i : ι, ∑ s : σ, if s = read x i then 0 else ∑ k : K, P.u x i k * P.u x i k

The positive witness's norm, exactly: 1 plus the dual's u-mass, once per false letter.

theorem QuantumQueryComplexity.qNormSq_negWitness_le {ι σ X O K : Type} [Fintype ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) {c : ℝ} (P : DualPairOn read K f) (hP : P.IsCostLe c) (y : X) : qNormSq (negWitness read f P y) ≤ 1 + c

The negative witness is short: ‖w‖² ≤ 1 + c for a dual of cost c.

The detector on the witness states: the two acceptance estimates

The last quantitative step of the state-conversion construction. SourceQuantumWitness built the witness states from a DualPairOn and discharged the exact contracts; this section adds the estimates and combines them with the fidelity bounds of SourceQuantumFidelity into the two numbers the eventual measurement reads: for the detector D = scDetector at clock length T and the initial state u = uniformClock T scTarget,

• f x = o (le_re_qInner_scDetector_of_eq): Re⟪u, D_x u⟫ ≥ 2/(1 + (|σ|−1)cu) − 1, from the exact fixed point posWitness x, its overlap ⟪τ, φₓ⟫ = 1, and its norm ‖φₓ‖² ≤ 1 + (|σ|−1)cu;
• f y ≠ o (re_qInner_scDetector_le_of_ne): Re⟪u, D_y u⟫ ≤ (Δ/2)√(1+cv) + 4/(TΔ) − (1 − (Δ²/4)(1+cv)), from the effective gap applied to negWitness y (whose input projection is exactly τ) and the uniform-clock suppression on the far window.

With Δ ~ 1/√(1+cv) and T ~ 1/Δ ~ √(1+cv) the second bound is ≈ −1 while the first is ≈ +1 for small (|σ|−1)cu — the separation a Hadamard test turns into a bounded-error measurement. Choosing those parameters, and the dual rescaling DualPairOn.scale that balances cu against cv, is the algorithm extraction's job; this section keeps every bound parametric.

The clock geometry those estimates ride on — the isometry qInner_uniformClock, additivity uniformClock_add, and their companions — is supplied by SourceQuantumClock and is shared with the uniform extraction.

Rescaling a dual pair

noncomputable def QuantumQueryComplexity.DualPairOn.scale {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) : DualPairOn read K f

Rescaling a dual pair: u ↦ αu, v ↦ α⁻¹v. Feasibility is scale-invariant, and the two sides' masses trade against each other — the balancing device of the algorithm extraction.

Equations

• P.scale hα = { u := fun (x : X) (i : ι) (k : K) => α * P.u x i k, v := fun (y : X) (i : ι) (k : K) => α⁻¹ * P.v y i k, constraint := ⋯ }

@[simp]

theorem QuantumQueryComplexity.DualPairOn.scale_u {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (x : X) (i : ι) (k : K) : (P.scale hα).u x i k = α * P.u x i k

@[simp]

theorem QuantumQueryComplexity.DualPairOn.scale_v {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (y : X) (i : ι) (k : K) : (P.scale hα).v y i k = α⁻¹ * P.v y i k

theorem QuantumQueryComplexity.DualPairOn.scale_u_mass {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (x : X) : ∑ i : ι, ∑ k : K, (P.scale hα).u x i k * (P.scale hα).u x i k = α ^ 2 * ∑ i : ι, ∑ k : K, P.u x i k * P.u x i k

The u-mass scales by α².

theorem QuantumQueryComplexity.DualPairOn.scale_v_mass {ι σ X O K : Type} [Fintype ι] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {α : ℝ} (hα : α ≠ 0) (y : X) : ∑ i : ι, ∑ k : K, (P.scale hα).v y i k * (P.scale hα).v y i k = α⁻¹ ^ 2 * ∑ i : ι, ∑ k : K, P.v y i k * P.v y i k

The v-mass scales by α⁻².

The witness norms, bounded

@[simp]

theorem QuantumQueryComplexity.qNormSq_scTarget {ι σ K : Type} [Fintype ι] [Fintype σ] [Fintype K] : qNormSq scTarget = 1

theorem QuantumQueryComplexity.one_le_qNormSq_posWitness {ι σ X O K : Type} [Fintype ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (x : X) : 1 ≤ qNormSq (posWitness read f P x)

The positive witness is at least a unit vector.

theorem QuantumQueryComplexity.qNormSq_posWitness_le {ι σ X O K : Type} [Fintype ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] (read : X → ι → σ) (f : X → O) [Nonempty σ] {cu : ℝ} (P : DualPairOn read K f) (x : X) (hcu : ∑ i : ι, ∑ k : K, P.u x i k * P.u x i k ≤ cu) : qNormSq (posWitness read f P x) ≤ 1 + (↑(Fintype.card σ) - 1) * cu

The positive witness is short: ‖φₓ‖² ≤ 1 + (|σ|−1)·cu when the dual's u-mass at x is at most cu. The |σ|−1 is the price of spreading u x over every false letter; it is 1 for a Boolean alphabet.

The detector

noncomputable def QuantumQueryComplexity.scDetector {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (o : O) (T : ℕ) : QRoutine ι σ (ClockWork ι T (Option K))

The detector for output o: the uniform-clock phase detector of the reflection product built from the witness construction's generators and the span of the positive witnesses of f⁻¹(o). Cost: 4(T−1) queries.

Equations

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

theorem QuantumQueryComplexity.scDetector_eq {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (o : O) (T : ℕ) : scDetector read f P o T = clockPhaseRefl (inputReflProduct scGen (scKer read f P o) ⋯) T

@[simp]

theorem QuantumQueryComplexity.scDetector_len {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (o : O) (T : ℕ) : (scDetector read f P o T).len = 4 * (T - 1)

The negative input, prepared

For f y ≠ o the fixed subspace annihilates negWitness y, whose input projection is exactly the target. So the effective gap bounds the near part of the target itself, and the detector's far-window guarantee applies to the rest — with ‖·‖² = 1 on the right of both.

theorem QuantumQueryComplexity.qNormSq_chordNear_scTarget_le {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) {o : O} {y : X} (hy : f y ≠ o) {cv : ℝ} (hcv : ∑ i : ι, ∑ k : K, P.v y i k * P.v y i k ≤ cv) (Δ : ℝ) : qNormSq ((chordNearProj ((inputReflProduct scGen (scKer read f P o) ⋯).run (read y)) Δ).mulVec scTarget) ≤ Δ ^ 2 / 4 * (1 + cv)

The near part of the target is small on a negative input: ‖N_Δ τ‖² ≤ (Δ²/4)(1 + cv).

theorem QuantumQueryComplexity.qNormSq_scDetector_far_add_le {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) (o : O) (y : X) {T : ℕ} (hT : 0 < T) {Δ : ℝ} (hΔ : 0 < Δ) : qNormSq (((scDetector read f P o T).run (read y)).mulVec (uniformClock T ((chordFarProj ((inputReflProduct scGen (scKer read f P o) ⋯).run (read y)) Δ).mulVec scTarget)) + uniformClock T ((chordFarProj ((inputReflProduct scGen (scKer read f P o) ⋯).run (read y)) Δ).mulVec scTarget)) ≤ 16 / (↑T ^ 2 * Δ ^ 2)

The detector reads −1 on the target's far part, up to 16/(T²Δ²). (The bound holds for every input; only its use is specific to f y ≠ o.)

The two acceptance estimates

theorem QuantumQueryComplexity.le_re_qInner_scDetector_of_eq {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) [Nonempty σ] (P : DualPairOn read K f) {o : O} {x : X} (hx : f x = o) {T : ℕ} (hT : 0 < T) {cu : ℝ} (hcu : ∑ i : ι, ∑ k : K, P.u x i k * P.u x i k ≤ cu) : 2 / (1 + (↑(Fintype.card σ) - 1) * cu) - 1 ≤ (qInner (uniformClock T scTarget) (((scDetector read f P o T).run (read x)).mulVec (uniformClock T scTarget))).re

The detector accepts a positive input: for f x = o, Re⟪u, D u⟫ ≥ 2/(1 + (|σ|−1)cu) − 1 on u = uniformClock T scTarget.

theorem QuantumQueryComplexity.re_qInner_scDetector_le_of_ne {ι σ X O K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → O) (P : DualPairOn read K f) {o : O} {y : X} (hy : f y ≠ o) {T : ℕ} (hT : 0 < T) {Δ : ℝ} (hΔ : 0 < Δ) {cv : ℝ} (hcv : ∑ i : ι, ∑ k : K, P.v y i k * P.v y i k ≤ cv) : (qInner (uniformClock T scTarget) (((scDetector read f P o T).run (read y)).mulVec (uniformClock T scTarget))).re ≤ Δ / 2 * √(1 + cv) + 4 / (↑T * Δ) - (1 - Δ ^ 2 / 4 * (1 + cv))

The detector rejects a negative input: for f y ≠ o, Re⟪u, D u⟫ ≤ (Δ/2)√(1+cv) + 4/(TΔ) − (1 − (Δ²/4)(1+cv)) on u = uniformClock T scTarget.

The uniform detector and its conversion errors

The detector of the cardinality-free construction: the clocked phase reflection of the reflection product built from the physical generators and the one global projector uniformL P α, at exactly 4(T-1) queries. The two signed conversion errors are

e₊ = D·clock(t_{x+}) − clock(t_{x+}),
e₋ = D·clock(t_{x−}) + clock(t_{x−}),

and this section proves the three conversion-distance facts:

• the positive bound ‖e₊‖² ≤ 8α²c — the detector fixes the clocked witness clock(φ_x) exactly, so on the bare target the error is the moved packet, e₊ = α·(1 − D)·clock(V_x), one unitary-move bound away from the v-mass that P.IsCostLe controls. A T = 0 split (uniformClock_zero) keeps the statement free of any positivity hypothesis on T;
• the negative bound ‖e₋‖ ≤ Δ√(1 + c/(2α²)) + 4/(TΔ) by one near/far split of the − target, the only statement needing hα, hT, hΔ;
• the combination: the end-to-end error D·clock(common) − clock(out) is (e₊ + e₋)/√2 by pure linearity, and e₊ ⟂ e₋ exactly — the detector is self-adjoint and unitary — so its squared norm is the exact half-sum (‖e₊‖² + ‖e₋‖²)/2, never a triangle bound.

Nested register instances

Named canonical instances for QBasis, CtrlWork, and UWork keep the nested register types within the default instance-search limit. The proofs retain the same finite types and oracle model.

noncomputable def QuantumQueryComplexity.uniformDetector {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) : QRoutine ι σ (ClockWork ι T (UWork (↑(Set.range f)) ι K))

The uniform detector: the clocked phase reflection of the reflection product R_P·R_L, for the physical generators and the global projector uniformL P α.

Equations

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

theorem QuantumQueryComplexity.uniformDetector_eq {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) : uniformDetector P α T = clockPhaseRefl (inputReflProduct uniformGen (uniformL P α) ⋯) T

The unfolding equation, so nothing downstream unfolds the definition.

@[simp]

theorem QuantumQueryComplexity.uniformDetector_len {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) : (uniformDetector P α T).len = 4 * (T - 1)

The exact cost of the uniform detector: 4(T-1) queries.

theorem QuantumQueryComplexity.uniformDetector_run_mulVec_uniformClock_uniformPhi {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) {T : ℕ} (hT : 0 < T) (x : X) : ((uniformDetector P α T).run (read x)).mulVec (uniformClock T (uniformPhi P α x)) = uniformClock T (uniformPhi P α x)

The detector fixes the clocked witness exactly — φ_x is a positive witness, so this is completeness with no error term.

The two conversion errors

noncomputable def QuantumQueryComplexity.uniformPlusError {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) (x : X) : QBasis ι σ (ClockWork ι T (UWork (↑(Set.range f)) ι K)) → ℂ

e₊ = D·clock(t_{x+}) − clock(t_{x+}): the deviation of the detector from +1 on the clocked + target.

Equations

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

noncomputable def QuantumQueryComplexity.uniformMinusError {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) (x : X) : QBasis ι σ (ClockWork ι T (UWork (↑(Set.range f)) ι K)) → ℂ

e₋ = D·clock(t_{x−}) + clock(t_{x−}): the deviation of the detector from -1 on the clocked − target. The + is the sign of the detector's -1 verdict.

Equations

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

The positive bound

theorem QuantumQueryComplexity.uniformPlusError_eq {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) {T : ℕ} (hT : 0 < T) (x : X) : uniformPlusError P α T x = ↑α • (1 - (uniformDetector P α T).run (read x)).mulVec (uniformClock T (realizedPacketV P.v read x))

The rearranged plus error: the detector fixes clock(φ_x) and φ_x = t_{x+} + α·V_x, so the error on the bare target is the moved packet, e₊ = α·(1 − D)·clock(V_x).

theorem QuantumQueryComplexity.qNormSq_uniformPlusError_le {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) (α : ℝ) (T : ℕ) (x : X) : qNormSq (uniformPlusError P α T x) ≤ 8 * α ^ 2 * c

The positive conversion bound: ‖e₊‖² ≤ 8α²c. No hypothesis on T or α: the T = 0 clock is zero, and the bound's sign comes from the cost hypothesis itself.

The negative bound

w_x is a negative witness — uniformL kills it — and inputProj sends it to the bare − target, so the effective gap and the divided detector bound apply to the near/far split of t_{x−} directly:

• the near part is small — ‖N‖² ≤ (Δ²/4)‖w_x‖² by effective_chord_gap_sq_inputReflProduct — so its detector error costs at most 2‖N‖;
• on the far part the detector reads -1 up to 4/(TΔ), by qNormSq_clockPhaseRefl_add_le_div_inputReflProduct and ‖t_{x−}‖ = 1.

One near/far triangle inequality combines the two. This is the only place hα, hT, hΔ are genuinely needed.

noncomputable def QuantumQueryComplexity.uniformNear {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α Δ : ℝ) (x : X) : UQBasis (↑(Set.range f)) ι σ K → ℂ

The near part of the realized − target, at window Δ.

Equations

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

noncomputable def QuantumQueryComplexity.uniformFar {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α Δ : ℝ) (x : X) : UQBasis (↑(Set.range f)) ι σ K → ℂ

The far part of the realized − target, at window Δ.

Equations

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

theorem QuantumQueryComplexity.uniformNear_add_uniformFar {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α Δ : ℝ) (x : X) : uniformNear P α Δ x + uniformFar P α Δ x = realizedTMinus f x

The near/far split of the − target.

theorem QuantumQueryComplexity.qNormSq_uniformNear_le {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) {α : ℝ} (hα : α ≠ 0) (Δ : ℝ) (x : X) : qNormSq (uniformNear P α Δ x) ≤ Δ ^ 2 / 4 * (1 + c / (2 * α ^ 2))

The near part is small: the effective gap charges it to ‖w_x‖², which the cost hypothesis bounds.

theorem QuantumQueryComplexity.qNormSq_uniformDetector_far_add_le {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) {T : ℕ} (hT : 0 < T) {Δ : ℝ} (hΔ : 0 < Δ) (x : X) : qNormSq (((uniformDetector P α T).run (read x)).mulVec (uniformClock T (uniformFar P α Δ x)) + uniformClock T (uniformFar P α Δ x)) ≤ 16 / (↑T ^ 2 * Δ ^ 2)

The detector reads -1 on the far part, up to 16/(T²Δ²) — the − target is a unit vector, so no witness norm enters.

theorem QuantumQueryComplexity.sqrt_qNormSq_uniformMinusError_le {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) {α : ℝ} (hα : α ≠ 0) {T : ℕ} (hT : 0 < T) {Δ : ℝ} (hΔ : 0 < Δ) (x : X) : √(qNormSq (uniformMinusError P α T x)) ≤ Δ * √(1 + c / (2 * α ^ 2)) + 4 / (↑T * Δ)

The negative conversion bound: ‖e₋‖ ≤ Δ·√(1 + c/(2α²)) + 4/(TΔ), by one near/far triangle inequality.

The combined conversion error

The end-to-end error runs the detector on the clocked input-independent common state against the clocked output-labelled target; by linearity it is (e₊ + e₋)/√2. The two signed errors are exactly orthogonal: the detector is self-adjoint (a reflection conjugated by a unitary) and unitary, so in

⟪e₊, e₋⟫ = ⟪Ds₊, Ds₋⟫ + ⟪Ds₊, s₋⟫ − ⟪s₊, Ds₋⟫ − ⟪s₊, s₋⟫

the outer terms cancel by unitarity and the middle terms by self-adjointness. The conversion error is therefore the exact half-sum ½(‖e₊‖² + ‖e₋‖²) — a triangle bound here would not support 8192.

theorem QuantumQueryComplexity.uniformDetector_run_conjTranspose {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) (a : ι → σ) : ((uniformDetector P α T).run a).conjTranspose = (uniformDetector P α T).run a

The detector is self-adjoint, inherited from clockPhaseRefl_run_conjTranspose.

theorem QuantumQueryComplexity.qInner_uniformPlusError_uniformMinusError {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) (x : X) : qInner (uniformPlusError P α T x) (uniformMinusError P α T x) = 0

The two signed errors are orthogonal — exactly, for every T and α.

noncomputable def QuantumQueryComplexity.uniformConvError {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) (x : X) : QBasis ι σ (ClockWork ι T (UWork (↑(Set.range f)) ι K)) → ℂ

The end-to-end conversion error: the detector applied to the clocked input-independent common state, against the clocked output-labelled target.

Equations

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

theorem QuantumQueryComplexity.uniformConvError_eq {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) (x : X) : uniformConvError P α T x = ↑(√2)⁻¹ • (uniformPlusError P α T x + uniformMinusError P α T x)

The conversion error is the scaled sum of the signed errors — pure linearity, no hypotheses at all.

theorem QuantumQueryComplexity.qNormSq_uniformConvError {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (T : ℕ) (x : X) : qNormSq (uniformConvError P α T x) = (qNormSq (uniformPlusError P α T x) + qNormSq (uniformMinusError P α T x)) / 2

The exact half-sum: with e₊ ⟂ e₋, ‖err‖² = (‖e₊‖² + ‖e₋‖²)/2 — an equality, not a triangle bound.

theorem QuantumQueryComplexity.qNormSq_uniformConvError_le {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) {α : ℝ} (hα : α ≠ 0) {T : ℕ} (hT : 0 < T) {Δ : ℝ} (hΔ : 0 < Δ) (x : X) : qNormSq (uniformConvError P α T x) ≤ (8 * α ^ 2 * c + (Δ * √(1 + c / (2 * α ^ 2)) + 4 / (↑T * Δ)) ^ 2) / 2

The combined conversion bound — the two component estimates through the exact half-sum; the only statement needing all three parameter hypotheses.

The parameters

With B = 1 + c:

α = (√(128B))⁻¹,   Δ = (64B)⁻¹,   T = ⌈2048B⌉.

Then 8α²c = c/(16B) ≤ 1/16; the near coefficient 1 + c/(2α²) = 1 + 64cB ≤ 64B² so the near term is at most Δ·8B = 1/8; TΔ ≥ 2048B/(64B) = 32 so the far term is at most 1/8; hence ‖e₋‖² ≤ 1/16 and the combined squared conversion distance is at most (1/16 + 1/16)/2 = 1/16 — at 4(T − 1) ≤ 8192(1 + c) queries — the uniformExtractionConstant, attained. Only Δ and α balance against c; the budget hypothesis is just 0 ≤ c.

noncomputable def QuantumQueryComplexity.uniformAlpha (c : ℝ) : ℝ

The witness scale: α = (√(128(1+c)))⁻¹.

Equations

• QuantumQueryComplexity.uniformAlpha c = (√(128 * (1 + c)))⁻¹

noncomputable def QuantumQueryComplexity.uniformDelta (c : ℝ) : ℝ

The window: Δ = (64(1+c))⁻¹.

Equations

• QuantumQueryComplexity.uniformDelta c = (64 * (1 + c))⁻¹

noncomputable def QuantumQueryComplexity.uniformT (c : ℝ) : ℕ

The clock: T = ⌈2048(1+c)⌉.

Equations

• QuantumQueryComplexity.uniformT c = ⌈2048 * (1 + c)⌉₊

theorem QuantumQueryComplexity.uniformAlpha_ne_zero {c : ℝ} (hc : 0 ≤ c) : uniformAlpha c ≠ 0

theorem QuantumQueryComplexity.uniformAlpha_sq {c : ℝ} (hc : 0 ≤ c) : uniformAlpha c ^ 2 = (128 * (1 + c))⁻¹

theorem QuantumQueryComplexity.uniformDelta_pos {c : ℝ} (hc : 0 ≤ c) : 0 < uniformDelta c

theorem QuantumQueryComplexity.uniformT_pos {c : ℝ} (hc : 0 ≤ c) : 0 < uniformT c

theorem QuantumQueryComplexity.qNormSq_uniformConvError_le_sixteenth {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) (hc : 0 ≤ c) (x : X) : qNormSq (uniformConvError P (uniformAlpha c) (uniformT c) x) ≤ 1 / 16

The instantiated conversion bound: at the chosen parameters the squared conversion distance is at most 1/16, for every promise input.

theorem QuantumQueryComplexity.uniformDetector_len_uniformT_le {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) {c : ℝ} (hc : 0 ≤ c) : ↑(uniformDetector P α (uniformT c)).len ≤ 8192 * (1 + c)

The detector at the chosen clock stays within the acceptance budget: 4(T − 1) ≤ 8192(1 + c) — the uniformExtractionConstant is attained.

The uniform extraction

The packaging of the cardinality-free construction: the detector run on the clocked input-independent common state, with the readout announcing the label held in the target register, is an algorithm computing f on the promise with error 1/16 — within 8192(1 + c) queries.

The acceptance statement exists_algorithm_of_dualPairOn_uniform has the required scope, every clause load-bearing:

• arbitrary decidable output O, no [Fintype O];
• uniformExtractionConstant = 8192, one fixed absolute constant — independent of |σ|, |O|, |range f|;
• [Nonempty O] (the readout needs a junk label off the target register) and 0 ≤ c are genuine hypotheses;
• promise-native, and no appeal to general-output strong duality.

The correctness chain is three moves: the algorithm's final state is D·clock(common), which is within squared distance 1/16 of clock(out(f x)) (qNormSq_uniformConvError_le_sixteenth); the clocked output state announces f x surely (its support carries the label in the target register — realizedOut_apply_of_ne through uniformClock_apply_eq_zero); and the distance-to-success bridge (le_qProb_of_qNormSq_sub_le, output-cardinality-free by design) converts the distance into the success probability ≥ 1 − 1/16.

def QuantumQueryComplexity.uniformExtractionConstant : ℝ

The uniform extraction constant — one fixed absolute constant, never a free variable.

Equations

• QuantumQueryComplexity.uniformExtractionConstant = 8192

The readout

def QuantumQueryComplexity.uniformLabel {ι K X O : Type} (f : X → O) (o₀ : O) : UWork (↑(Set.range f)) ι K → O

The label of one workspace coordinate: the output held in the target register, or the junk label o₀ anywhere else.

Equations

• QuantumQueryComplexity.uniformLabel f o₀ (Sum.inl (some r)) = ↑r
• QuantumQueryComplexity.uniformLabel f o₀ (Sum.inl none) = o₀
• QuantumQueryComplexity.uniformLabel f o₀ (Sum.inr val) = o₀

@[simp]

theorem QuantumQueryComplexity.uniformLabel_inl_some {ι K X O : Type} (f : X → O) (o₀ : O) (r : ↑(Set.range f)) : uniformLabel f o₀ (Sum.inl (some r)) = ↑r

def QuantumQueryComplexity.uniformReadout {ι σ K X O : Type} (f : X → O) (o₀ : O) (T : ℕ) : QBasis ι σ (ClockWork ι T (UWork (↑(Set.range f)) ι K)) → O

The readout: announce the label held in the target register of the clocked workspace.

Equations

• QuantumQueryComplexity.uniformReadout f o₀ T b = QuantumQueryComplexity.uniformLabel f o₀ b.2.2.2.2.2

theorem QuantumQueryComplexity.uniformReadout_apply {ι σ K X O : Type} (f : X → O) (o₀ : O) (T : ℕ) (b : QBasis ι σ (ClockWork ι T (UWork (↑(Set.range f)) ι K))) : uniformReadout f o₀ T b = uniformLabel f o₀ b.2.2.2.2.2

theorem QuantumQueryComplexity.qRestrict_uniformClock_realizedOut {ι σ K X O : Type} [DecidableEq ι] [DecidableEq O] {f : X → O} (o₀ : O) (T : ℕ) (x : X) : qRestrict (uniformReadout f o₀ T) (f x) (uniformClock T (realizedOut f x)) = uniformClock T (realizedOut f x)

The clocked output state announces its label surely: it is its own restriction to the f x-sector of the readout.

The algorithm

noncomputable def QuantumQueryComplexity.uniformAlg {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) (α : ℝ) (o₀ : O) (T : ℕ) (hT : 0 < T) : QAlg ι σ O (ClockWork ι T (UWork (↑(Set.range f)) ι K))

The uniform extraction algorithm: prepare the clocked common state, run the detector, read the target register.

Equations

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

theorem QuantumQueryComplexity.uniformAlg_computes {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [DecidableEq K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) (hc : 0 ≤ c) (o₀ : O) : ComputesWithErrorOn (uniformAlg P (uniformAlpha c) o₀ (uniformT c) ⋯) (4 * (uniformT c - 1)) read f (1 / 16)

The uniform algorithm computes f at the chosen parameters: error 1/16 on the promise, in exactly 4(T − 1) queries.

The acceptance statement

theorem QuantumQueryComplexity.exists_algorithm_of_dualPairOn_uniform {ι σ K X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype K] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} [Nonempty O] (P : DualPairOn read K f) {c : ℝ} (hP : P.IsCostLe c) (hc : 0 ≤ c) : ∃ q ∈ QueryCounts read f (1 / 16), ↑q ≤ uniformExtractionConstant * (1 + c)

A dual solution is an algorithm, with no cardinality anywhere: cost c yields error 1/16 within uniformExtractionConstant·(1 + c) queries — independent of |σ|, |O| and |range f|, for any decidable output type.

The dual-to-algorithm upper bound

The extraction: a feasible DualPairOn read K f for a Boolean f becomes a quantum query algorithm. The algorithm is nothing but the Hadamard test of the o = true detector on the target state,

scAlg = hadTest (scDetector read f P true T) (uniformClock T scTarget),

at exactly 4(T−1) queries, and its correctness is the two acceptance estimates of SourceQuantumDetection pushed through hadTest_prob_true/false:

• scAlg_computes — the parametric correctness: any (T, Δ, cu, cv, ε) satisfying the two explicit inequalities gives ComputesWithErrorOn (scAlg …) (4(T−1)) read f ε;

• exists_algorithm_of_dualPairOn — the endgame: a dual of cost c > 0 is compiled, after the scale balancing α² = (16|σ|c)⁻¹ and the choices Δ = (16√B)⁻¹, T = ⌈2048√B⌉ for B = 1 + 16|σ|c², into membership

  4(T−1) ∈ QueryCounts read f (1/16),   4(T−1) ≤ 8192·(1 + 4√|σ|·c),
  

  with the qQueryOn corollary qQueryOn_le_of_dualPairOn. For a Boolean alphabet √|σ| = √2, so the bound is O(c) with an explicit constant.

The error budget of the endgame, for the record: positive side s·cu = (|σ|−1)/(16|σ|) ≤ 1/16, so the acceptance is at least 1/(1 + 1/16) = 16/17 ≥ 15/16; negative side 1/64 + 1/64 + 1/2048 = 65/2048 ≤ 1/16. Nothing is tight — the constants are chosen round, not small.

The output convention: scAlg announces true on constructive interference (control 0), which is the f x = true side because scKer read f P true spans the positive witnesses of f⁻¹(true).

theorem QuantumQueryComplexity.isQState_uniformClock_scTarget {ι σ K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [Fintype K] {T : ℕ} (hT : 0 < T) : IsQState (uniformClock T scTarget)

noncomputable def QuantumQueryComplexity.scAlg {ι σ X K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → Bool) (P : DualPairOn read K f) (T : ℕ) (hT : 0 < T) : QAlg ι σ Bool (CtrlWork ι (ClockWork ι T (Option K)))

The extracted algorithm: the Hadamard test of the o = true detector on the target state. Cost: exactly 4(T−1) queries.

Equations

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

theorem QuantumQueryComplexity.scAlg_computes {ι σ X K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [Fintype K] [DecidableEq K] (read : X → ι → σ) (f : X → Bool) [Nonempty σ] (P : DualPairOn read K f) {T : ℕ} (hT : 0 < T) {Δ : ℝ} (hΔ : 0 < Δ) {cu cv ε : ℝ} (hcu : ∀ (x : X), ∑ i : ι, ∑ k : K, P.u x i k * P.u x i k ≤ cu) (hcv : ∀ (y : X), ∑ i : ι, ∑ k : K, P.v y i k * P.v y i k ≤ cv) (hpos : 1 - ε ≤ 1 / (1 + (↑(Fintype.card σ) - 1) * cu)) (hneg : Δ / 4 * √(1 + cv) + 2 / (↑T * Δ) + Δ ^ 2 / 8 * (1 + cv) ≤ ε) : ComputesWithErrorOn (scAlg read f P T hT) (4 * (T - 1)) read f ε

Parametric correctness of the extracted algorithm. The two hypotheses are exactly the two acceptance estimates' final forms; any parameter choice satisfying them gives a bounded-error algorithm.

The endgame: choosing the parameters

Balance with α² = (16|σ|c)⁻¹, detect at radius Δ = (16√B)⁻¹ with clock T = ⌈2048√B⌉, where B = 1 + 16|σ|c².

theorem QuantumQueryComplexity.exists_algorithm_of_dualPairOn {ι σ X K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [Fintype K] (read : X → ι → σ) (f : X → Bool) [Nonempty σ] {c : ℝ} (P : DualPairOn read K f) (hP : P.IsCostLe c) (hc : 0 < c) : ∃ q ∈ QueryCounts read f (1 / 16), ↑q ≤ 8192 * (1 + 4 * √↑(Fintype.card σ) * c)

A dual solution of cost c is an algorithm: error 1/16, at most 8192(1 + 4√|σ|·c) queries.

theorem QuantumQueryComplexity.qQueryOn_le_of_dualPairOn {ι σ X K : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [Fintype K] (read : X → ι → σ) (f : X → Bool) [Nonempty σ] {c : ℝ} (P : DualPairOn read K f) (hP : P.IsCostLe c) (hc : 0 < c) : ↑(qQueryOn read f (1 / 16)) ≤ 8192 * (1 + 4 * √↑(Fintype.card σ) * c)

The qQueryOn corollary: Q_{1/16}(f) ≤ 8192(1 + 4√|σ|·c) for any dual of cost c.

Uniform extraction: the HasDualOn wrappers

The bundled form of the cardinality-free extraction. HasDualOn hides the dual dimension type and is defined in SourcePromiseHasDual in Adversary. These wrappers connect it to the operational constructions in StateConversion.

Both wrappers are one destructuring away from exists_algorithm_of_dualPairOn_uniform: any bundled dual solution of cost c gives Q_{1/16}(f) ≤ 8192(1 + c), and Q_{1/3} by error monotonicity — for any decidable output type, with no |σ|, |O| or |range f| anywhere.

theorem QuantumQueryComplexity.qQueryOn_le_of_hasDualOn_uniform {ι σ X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} [Nonempty O] {c : ℝ} (h : HasDualOn read f c) (hc : 0 ≤ c) : ↑(qQueryOn read f (1 / 16)) ≤ uniformExtractionConstant * (1 + c)

Cardinality-free extraction from a bundled dual: Q_{1/16}(f) ≤ 8192(1 + c) for any decidable output type.

theorem QuantumQueryComplexity.qQueryOn_third_le_of_hasDualOn_uniform {ι σ X O : Type} [Fintype ι] [DecidableEq ι] [Fintype σ] [DecidableEq σ] [Fintype X] [DecidableEq O] {read : X → ι → σ} {f : X → O} [Nonempty O] {c : ℝ} (h : HasDualOn read f c) (hc : 0 ≤ c) : ↑(qQueryOn read f (1 / 3)) ≤ uniformExtractionConstant * (1 + c)

The bounded-error form, by error monotonicity.