Amplitude amplification: the closed form and the ⌊π/(4θ)⌋ bound (BHMT)

Category: 1-Mathlib (CSD-free).

Glossary: https://glossary.constraintsurfacedynamics.com/amplitude-amplification/ Plain-language, CSD-role and formal statements of amplitude amplification, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Brassard–Høyer–Mosca–Tapp amplitude amplification (quant-ph/0005055), the theorem Grover's algorithm is an instance of, on a register over an arbitrary finite computational basis ι with an arbitrary good set G : Finset ι:

• The two-reflection rotation. The amplification step ampStep φ G = reflect φ ∘ oracleFlip G — reflection about the initial state composed with the sign flip on the good coordinates — acts on the plane spanned by the (unit) good and bad components as a rotation by 2θ (ampStep_ampState), where sin θ = √(goodProb G φ).
• ★★ The closed form (amplitude_amplification): for any unit ψ with 0 < goodProb G ψ < 1, after j amplification rounds the success probability is exactly sin²((2j+1)·θ) with θ = arcsin √(goodProb G ψ). No asymptotics.
• ★ The optimal count (amplitude_amplification_succeeds): m = ⌊π/(4θ)⌋ rounds land the angle within θ of π/2, so the success probability is at least 1 − a.
• ★ The quadratic speedup (amplification_query_bound): m ≤ π/(4√a), since √a = sin θ ≤ θ.
• Non-vacuity at a closed instance (amplification_quarter): at a = 1/4 a single round succeeds with certainty (θ = π/6, 3θ = π/2).

Grover's algorithm is the instance φ = uniform superposition, G = {w} (Empirical/QM/Algorithms/Grover.lean re-derives its headline from this module), and the k-marked-items generalisation is the instance |G| = k (grover_multi_success, same file).

Honest scope

Query counting is by rounds of the abstract step; no oracle model or gate decomposition is claimed (the same matrix-level scope as Fourier.lean/PhaseEstimation.lean). The degenerate boundaries are real and excluded by hypothesis: goodProb = 0 leaves no plane to rotate and goodProb = 1 nothing to amplify. Amplitude estimation (BHMT Thm 12) is assembled in AmplitudeEstimation.lean from this module's eigenstructure section. For unknown a, the QSearch engine (BHMT Lemma 2) is the final section here: a uniformly random round count below M succeeds with average probability ≥ 1/4 once M·sin 2θ ≥ 1 (qsearch_average) — the paper's Thm 3 wraps this in an exponential-doubling schedule whose expected-runtime bookkeeping is a probabilistic-process argument, not formalised (⚠️ RESIDUE(R-002), specs/amplitude-amplification-plan.md AA-6).

The operators

noncomputable def QuantumInfo.goodProj {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The good-coordinate truncation P_G ψ: keep the amplitudes on G, zero elsewhere.

Equations

• QuantumInfo.goodProj G ψ = (WithLp.equiv 2 (ι → ℂ)).symm fun (i : ι) => if i ∈ G then ψ.ofLp i else 0

@[simp]

theorem QuantumInfo.goodProj_apply {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (i : ι) : (goodProj G ψ).ofLp i = if i ∈ G then ψ.ofLp i else 0

noncomputable def QuantumInfo.goodProb {ι : Type u_1} (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : ℝ

The success probability of ψ against the good set G: ∑_{i ∈ G} ‖ψ i‖².

Equations

• QuantumInfo.goodProb G ψ = ∑ i ∈ G, ‖ψ.ofLp i‖ ^ 2

theorem QuantumInfo.goodProb_nonneg {ι : Type u_1} (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : 0 ≤ goodProb G ψ

theorem QuantumInfo.goodProb_eq_sum_prob {ι : Type u_1} (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : goodProb G ψ = ∑ i ∈ G, prob ψ i

The success probability is the sum of the Born probabilities over the good set.

noncomputable def QuantumInfo.oracleFlip {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The oracle reflection I − 2 P_G: a phase flip on the good coordinates.

Equations

• QuantumInfo.oracleFlip G ψ = ψ - 2 • QuantumInfo.goodProj G ψ

theorem QuantumInfo.oracleFlip_apply {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (i : ι) : (oracleFlip G ψ).ofLp i = ψ.ofLp i - 2 * if i ∈ G then ψ.ofLp i else 0

noncomputable def QuantumInfo.reflect {ι : Type u_1} [Fintype ι] (φ ψ : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The reflection about a state 2|φ⟩⟨φ| − I (the generalised diffusion operator).

Equations

• QuantumInfo.reflect φ ψ = (2 * inner ℂ φ ψ) • φ - ψ

noncomputable def QuantumInfo.ampStep {ι : Type u_1} [Fintype ι] [DecidableEq ι] (φ : EuclideanSpace ℂ ι) (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

One amplification step: the oracle flip followed by reflection about φ.

Equations

• QuantumInfo.ampStep φ G ψ = QuantumInfo.reflect φ (QuantumInfo.oracleFlip G ψ)

The rotation plane

noncomputable def QuantumInfo.ampState {ι : Type u_1} (g b : EuclideanSpace ℂ ι) (γ : ℝ) : EuclideanSpace ℂ ι

The rotation-plane state at angle γ: (sin γ) g + (cos γ) b for a good unit component g and a bad unit component b.

Equations

• QuantumInfo.ampState g b γ = ↑(Real.sin γ) • g + ↑(Real.cos γ) • b

theorem QuantumInfo.ampState_apply {ι : Type u_1} (g b : EuclideanSpace ℂ ι) (γ : ℝ) (i : ι) : (ampState g b γ).ofLp i = ↑(Real.sin γ) * g.ofLp i + ↑(Real.cos γ) * b.ofLp i

theorem QuantumInfo.goodProj_ampState {ι : Type u_1} [DecidableEq ι] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hgsupp : ∀ i ∉ G, g.ofLp i = 0) (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (γ : ℝ) : goodProj G (ampState g b γ) = ↑(Real.sin γ) • g

Truncating the plane state to G keeps exactly the good component.

theorem QuantumInfo.oracleFlip_ampState {ι : Type u_1} [DecidableEq ι] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hgsupp : ∀ i ∉ G, g.ofLp i = 0) (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (γ : ℝ) : oracleFlip G (ampState g b γ) = ampState g b (-γ)

The oracle flip negates the angle: oracleFlip (ampState γ) = ampState (−γ).

theorem QuantumInfo.inner_ampState {ι : Type u_1} [Fintype ι] {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) (θ δ : ℝ) : inner ℂ (ampState g b θ) (ampState g b δ) = ↑(Real.cos (θ - δ))

The plane's inner-product law: ⟨ampState θ, ampState δ⟩ = cos (θ − δ) for orthonormal g, b.

The two product-to-sum identities that make two reflections a rotation

theorem QuantumInfo.two_cos_sub_mul_sin (θ δ : ℝ) : 2 * Real.cos (θ - δ) * Real.sin θ - Real.sin δ = Real.sin (2 * θ - δ)

theorem QuantumInfo.two_cos_sub_mul_cos (θ δ : ℝ) : 2 * Real.cos (θ - δ) * Real.cos θ - Real.cos δ = Real.cos (2 * θ - δ)

theorem QuantumInfo.reflect_ampState {ι : Type u_1} [Fintype ι] {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) (θ δ : ℝ) : reflect (ampState g b θ) (ampState g b δ) = ampState g b (2 * θ - δ)

Reflection about the θ-state reflects the plane angle: reflect (ampState θ) (ampState δ) = ampState (2θ − δ).

theorem QuantumInfo.ampStep_ampState {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) (hgsupp : ∀ i ∉ G, g.ofLp i = 0) (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (θ γ : ℝ) : ampStep (ampState g b θ) G (ampState g b γ) = ampState g b (γ + 2 * θ)

★ The two-reflection rotation (the heart of BHMT): one amplification step advances the plane angle by 2θ, where θ is the angle of the reflecting state φ = ampState θ.

theorem QuantumInfo.ampStep_iterate {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) (hgsupp : ∀ i ∉ G, g.ofLp i = 0) (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (θ : ℝ) (j : ℕ) : (ampStep (ampState g b θ) G)^[j] (ampState g b θ) = ampState g b ((2 * ↑j + 1) * θ)

The iterated rotation: j amplification steps from the θ-state reach the (2j+1)θ-state.

theorem QuantumInfo.goodProb_ampState {ι : Type u_1} {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (hgood : ∑ i ∈ G, ‖g.ofLp i‖ ^ 2 = 1) (γ : ℝ) : goodProb G (ampState g b γ) = Real.sin γ ^ 2

The plane state's success probability is sin² γ (the bad component vanishes on G and the good component carries unit weight there).

The decomposition of a state into its good and bad unit components

noncomputable def QuantumInfo.goodUnit {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The good unit component of ψ against G.

Equations

• QuantumInfo.goodUnit G ψ = (↑√(QuantumInfo.goodProb G ψ))⁻¹ • QuantumInfo.goodProj G ψ

noncomputable def QuantumInfo.badUnit {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The bad unit component of ψ against G.

Equations

• QuantumInfo.badUnit G ψ = (↑√(1 - QuantumInfo.goodProb G ψ))⁻¹ • (ψ - QuantumInfo.goodProj G ψ)

theorem QuantumInfo.goodUnit_apply {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (i : ι) : (goodUnit G ψ).ofLp i = (↑√(goodProb G ψ))⁻¹ * if i ∈ G then ψ.ofLp i else 0

theorem QuantumInfo.badUnit_apply {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (i : ι) : (badUnit G ψ).ofLp i = (↑√(1 - goodProb G ψ))⁻¹ * (ψ.ofLp i - if i ∈ G then ψ.ofLp i else 0)

theorem QuantumInfo.goodUnit_supp {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (i : ι) : i ∉ G → (goodUnit G ψ).ofLp i = 0

theorem QuantumInfo.badUnit_supp {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (i : ι) : i ∈ G → (badUnit G ψ).ofLp i = 0

theorem QuantumInfo.goodUnit_weight {ι : Type u_1} [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (ha0 : 0 < goodProb G ψ) : ∑ i ∈ G, ‖(goodUnit G ψ).ofLp i‖ ^ 2 = 1

The good unit component carries unit weight on G.

theorem QuantumInfo.inner_goodUnit_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (ha0 : 0 < goodProb G ψ) : inner ℂ (goodUnit G ψ) (goodUnit G ψ) = 1

⟨g, g⟩ = 1 for the good unit component.

theorem QuantumInfo.inner_badUnit_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (ha1 : goodProb G ψ < 1) : inner ℂ (badUnit G ψ) (badUnit G ψ) = 1

⟨b, b⟩ = 1 for the bad unit component (unit ψ).

theorem QuantumInfo.inner_goodUnit_badUnit {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} : inner ℂ (goodUnit G ψ) (badUnit G ψ) = 0

⟨g, b⟩ = 0: the components live on disjoint coordinates.

theorem QuantumInfo.ampState_decomposition {ι : Type u_1} [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) : ψ = ampState (goodUnit G ψ) (badUnit G ψ) (Real.arcsin √(goodProb G ψ))

The decomposition: ψ = ampState (goodUnit) (badUnit) (arcsin √a).

The headline

theorem QuantumInfo.amplitude_amplification {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) (j : ℕ) : goodProb G ((ampStep ψ G)^[j] ψ) = Real.sin ((2 * ↑j + 1) * Real.arcsin √(goodProb G ψ)) ^ 2

★★ Amplitude amplification (BHMT), the closed form. For a unit state ψ with success probability a = goodProb G ψ strictly between 0 and 1, j rounds of the amplification step ampStep ψ G — reflect about ψ after flipping the good-coordinate signs — yield success probability exactly sin²((2j+1)·θ), θ = arcsin √a. Grover's algorithm and its k-marked generalisation are instances (Empirical/QM/Algorithms/Grover.lean).

The optimal count and the quadratic speedup

theorem QuantumInfo.amplitude_amplification_succeeds {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) : 1 - goodProb G ψ ≤ goodProb G ((ampStep ψ G)^[⌊Real.pi / (4 * Real.arcsin √(goodProb G ψ))⌋₊] ψ)

★ The ⌊π/(4θ)⌋ round count succeeds with probability at least 1 − a. The chosen count lands the accumulated angle within θ of π/2, where the success probability is at least cos²θ = 1 − a. This is the bound Grover analyses defer to "downstream arithmetic": here it is a theorem about the closed form.

theorem QuantumInfo.amplification_query_bound {ι : Type u_1} {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) : ↑⌊Real.pi / (4 * Real.arcsin √(goodProb G ψ))⌋₊ ≤ Real.pi / (4 * √(goodProb G ψ))

★ The quadratic speedup as an inequality: the chosen round count is at most π/(4√a), since √a = sin θ ≤ θ.

theorem QuantumInfo.amplification_quarter {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (ha : goodProb G ψ = 1 / 4) : goodProb G (ampStep ψ G ψ) = 1

Non-vacuity at a closed instance: at success probability exactly 1/4 a single amplification round succeeds with certainty — θ = π/6, and 3θ = π/2.

The eigenstructure of the amplification step (AA-5a)

On the rotation plane the step Q = ampStep (ampState θ) G is a rotation by 2θ, so its eigenvectors there are g ± i·b with eigenvalues e^{±2iθ} — the fact amplitude estimation (BHMT Thm 12) feeds to phase estimation. This section delivers the eigenstructure and the estimate's error algebra; the two-register kickback marginal is AA-5b (specs/amplitude-amplification-plan.md).

theorem QuantumInfo.goodProj_add {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ χ : EuclideanSpace ℂ ι) : goodProj G (ψ + χ) = goodProj G ψ + goodProj G χ

theorem QuantumInfo.goodProj_smul {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (c : ℂ) (ψ : EuclideanSpace ℂ ι) : goodProj G (c • ψ) = c • goodProj G ψ

theorem QuantumInfo.oracleFlip_add {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (ψ χ : EuclideanSpace ℂ ι) : oracleFlip G (ψ + χ) = oracleFlip G ψ + oracleFlip G χ

theorem QuantumInfo.oracleFlip_smul {ι : Type u_1} [DecidableEq ι] (G : Finset ι) (c : ℂ) (ψ : EuclideanSpace ℂ ι) : oracleFlip G (c • ψ) = c • oracleFlip G ψ

theorem QuantumInfo.reflect_add {ι : Type u_1} [Fintype ι] (φ ψ χ : EuclideanSpace ℂ ι) : reflect φ (ψ + χ) = reflect φ ψ + reflect φ χ

theorem QuantumInfo.reflect_smul {ι : Type u_1} [Fintype ι] (φ : EuclideanSpace ℂ ι) (c : ℂ) (ψ : EuclideanSpace ℂ ι) : reflect φ (c • ψ) = c • reflect φ ψ

theorem QuantumInfo.ampStep_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (φ : EuclideanSpace ℂ ι) (G : Finset ι) (ψ χ : EuclideanSpace ℂ ι) : ampStep φ G (ψ + χ) = ampStep φ G ψ + ampStep φ G χ

The amplification step is additive.

theorem QuantumInfo.ampStep_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (φ : EuclideanSpace ℂ ι) (G : Finset ι) (c : ℂ) (ψ : EuclideanSpace ℂ ι) : ampStep φ G (c • ψ) = c • ampStep φ G ψ

The amplification step is ℂ-homogeneous.

theorem QuantumInfo.ampState_zero {ι : Type u_1} (g b : EuclideanSpace ℂ ι) : ampState g b 0 = b

theorem QuantumInfo.ampState_pi_div_two {ι : Type u_1} (g b : EuclideanSpace ℂ ι) : ampState g b (Real.pi / 2) = g

theorem QuantumInfo.exp_ofReal_mul_I (x : ℝ) : Complex.exp (↑x * Complex.I) = ↑(Real.cos x) + ↑(Real.sin x) * Complex.I

e^{ix} = cos x + (sin x)·i with the real trigonometric functions, coerced.

noncomputable def QuantumInfo.eigenPlus {ι : Type u_1} (g b : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The e^{+2iθ} eigenvector of the amplification step on the rotation plane: g + i·b.

Equations

• QuantumInfo.eigenPlus g b = g + Complex.I • b

noncomputable def QuantumInfo.eigenMinus {ι : Type u_1} (g b : EuclideanSpace ℂ ι) : EuclideanSpace ℂ ι

The e^{−2iθ} eigenvector: g − i·b.

Equations

• QuantumInfo.eigenMinus g b = g - Complex.I • b

theorem QuantumInfo.eigenPlus_add_eigenMinus {ι : Type u_1} (g b : EuclideanSpace ℂ ι) : eigenPlus g b + eigenMinus g b = 2 • g

The eigenvectors recombine to the good component: v₊ + v₋ = 2g.

theorem QuantumInfo.eigenPlus_sub_eigenMinus {ι : Type u_1} (g b : EuclideanSpace ℂ ι) : eigenPlus g b - eigenMinus g b = (2 * Complex.I) • b

The eigenvectors recombine to the bad component: v₊ − v₋ = 2i·b.

theorem QuantumInfo.ampStep_eigenPlus {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) (hgsupp : ∀ i ∉ G, g.ofLp i = 0) (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (θ : ℝ) : ampStep (ampState g b θ) G (eigenPlus g b) = Complex.exp (↑(2 * θ) * Complex.I) • eigenPlus g b

★ The + eigenvector equation: on the rotation plane the amplification step has g + i·b as an eigenvector with eigenvalue e^{2iθ}. This is the spectral fact amplitude estimation hands to phase estimation.

theorem QuantumInfo.ampStep_eigenMinus {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) (hgsupp : ∀ i ∉ G, g.ofLp i = 0) (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (θ : ℝ) : ampStep (ampState g b θ) G (eigenMinus g b) = Complex.exp (↑(-(2 * θ)) * Complex.I) • eigenMinus g b

★ The − eigenvector equation: g − i·b carries eigenvalue e^{−2iθ}.

theorem QuantumInfo.ampStep_iterate_eigenPlus {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) (hgsupp : ∀ i ∉ G, g.ofLp i = 0) (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (θ : ℝ) (j : ℕ) : (ampStep (ampState g b θ) G)^[j] (eigenPlus g b) = Complex.exp (↑(2 * ↑j * θ) * Complex.I) • eigenPlus g b

Iterated eigen-action: j amplification steps scale the + eigenvector by e^{2ijθ} — the phase a counting register would estimate.

theorem QuantumInfo.ampStep_iterate_eigenMinus {ι : Type u_1} [Fintype ι] [DecidableEq ι] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) (hgsupp : ∀ i ∉ G, g.ofLp i = 0) (hbsupp : ∀ i ∈ G, b.ofLp i = 0) (θ : ℝ) (j : ℕ) : (ampStep (ampState g b θ) G)^[j] (eigenMinus g b) = Complex.exp (↑(-(2 * ↑j * θ)) * Complex.I) • eigenMinus g b

Iterated eigen-action, − branch: j steps scale the − eigenvector by e^{−2ijθ}.

theorem QuantumInfo.ampStep_iterate_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (φ : EuclideanSpace ℂ ι) (G : Finset ι) (j : ℕ) (ψ χ : EuclideanSpace ℂ ι) : (ampStep φ G)^[j] (ψ + χ) = (ampStep φ G)^[j] ψ + (ampStep φ G)^[j] χ

The iterated amplification step is additive.

theorem QuantumInfo.ampStep_iterate_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (φ : EuclideanSpace ℂ ι) (G : Finset ι) (j : ℕ) (k : ℂ) (ψ : EuclideanSpace ℂ ι) : (ampStep φ G)^[j] (k • ψ) = k • (ampStep φ G)^[j] ψ

The iterated amplification step is ℂ-homogeneous.

theorem QuantumInfo.ampState_eq_eigen {ι : Type u_1} (g b : EuclideanSpace ℂ ι) (γ : ℝ) : ampState g b γ = (-Complex.I / 2 * Complex.exp (↑γ * Complex.I)) • eigenPlus g b + (Complex.I / 2 * Complex.exp (↑(-γ) * Complex.I)) • eigenMinus g b

The eigen-decomposition of the rotation-plane state: ampState γ = (−i/2)e^{iγ}·v₊ + (i/2)e^{−iγ}·v₋ — branch weights 1/4·‖v₊‖² = 1/2 each. The bridge from the amplification plane to the phase-estimation branches.

theorem QuantumInfo.inner_eigenPlus_eigenMinus {ι : Type u_1} [Fintype ι] {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) : inner ℂ (eigenPlus g b) (eigenMinus g b) = 0

The two eigenvectors are orthogonal.

theorem QuantumInfo.inner_eigenPlus_self {ι : Type u_1} [Fintype ι] {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) : inner ℂ (eigenPlus g b) (eigenPlus g b) = 2

‖v₊‖² = 2.

theorem QuantumInfo.inner_eigenMinus_self {ι : Type u_1} [Fintype ι] {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) : inner ℂ (eigenMinus g b) (eigenMinus g b) = 2

‖v₋‖² = 2.

theorem QuantumInfo.sum_sq_eigenPlus {ι : Type u_1} [Fintype ι] {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) : ∑ y : ι, ‖(eigenPlus g b).ofLp y‖ ^ 2 = 2

The coordinate-sum form of ‖v₊‖² = 2.

theorem QuantumInfo.sum_sq_eigenMinus {ι : Type u_1} [Fintype ι] {g b : EuclideanSpace ℂ ι} (hgg : inner ℂ g g = 1) (hbb : inner ℂ b b = 1) (hgb : inner ℂ g b = 0) : ∑ y : ι, ‖(eigenMinus g b).ofLp y‖ ^ 2 = 2

The coordinate-sum form of ‖v₋‖² = 2.

The estimate's error algebra (BHMT Lemma 7 shape)

theorem QuantumInfo.sin_sq_sub_sin_sq (x y : ℝ) : Real.sin x ^ 2 - Real.sin y ^ 2 = Real.sin (x + y) * Real.sin (x - y)

The sin² difference in product form: sin²x − sin²y = sin(x+y)·sin(x−y).

theorem QuantumInfo.abs_sin_sq_sub_sin_sq_le (x y : ℝ) : |Real.sin x ^ 2 - Real.sin y ^ 2| ≤ |Real.sin (2 * y)| * |x - y| + |x - y| ^ 2

★ The sin² perturbation bound: |sin²x − sin²y| ≤ |sin 2y|·|x−y| + |x−y|² — the Lipschitz-plus-quadratic control that turns a phase-estimate error into an amplitude-estimate error.

theorem QuantumInfo.amplitude_estimation_error {a : ℝ} (ha0 : 0 ≤ a) {θ θ' : ℝ} (hθ : Real.sin θ = √a) (hθc : Real.cos θ = √(1 - a)) {ε : ℝ} (hδ : |θ' - θ| ≤ ε) : |Real.sin θ' ^ 2 - a| ≤ 2 * √(a * (1 - a)) * ε + ε ^ 2

★ The amplitude-estimation error bound (BHMT Lemma 7). If the true amplitude is a = sin²θ (with cos θ = √(1−a)) and the estimated angle θ' is within ε of θ, then the estimated amplitude sin²θ' is within 2√(a(1−a))·ε + ε² of a. With the phase-estimation window ε = π/T this is the standard |ã − a| ≤ 2π√(a(1−a))/T + π²/T²; instantiating it on the two-register kickback marginal is AA-5b.

Unknown amplitude: the averaged rotation (QSearch engine, BHMT Lemma 2)

When a is unknown the optimal count ⌊π/(4θ)⌋ cannot be computed. BHMT's remedy: pick the round count uniformly at random below a guess M. The average success probability has an exact closed form — the odd-angle sin² sum telescopes — and once M·sin 2θ ≥ 1 it is at least 1/4, independent of a. The exponential-doubling schedule built on this (BHMT Thm 3) is algorithmic bookkeeping and not formalised.

theorem QuantumInfo.cos_two_mul_odd (t : ℝ) : Real.cos (2 * t) = 1 - 2 * Real.sin t ^ 2

The double angle of the odd angle: cos(2·(2m+1)θ) = 1 − 2 sin²((2m+1)θ).

theorem QuantumInfo.sum_sin_sq_odd_mul (θ : ℝ) (M : ℕ) : 4 * Real.sin (2 * θ) * ∑ m ∈ Finset.range M, Real.sin ((2 * ↑m + 1) * θ) ^ 2 = 2 * ↑M * Real.sin (2 * θ) - Real.sin (4 * ↑M * θ)

The telescoped average (product form, BHMT Lemma 2): 4 sin(2θ) · ∑_{m<M} sin²((2m+1)θ) = 2M sin(2θ) − sin(4Mθ) — exactly, for every θ. The sin² sum telescopes through sin(2A+2θ) − sin(2A−2θ) = 2 cos(2A) sin(2θ) at the odd angles A = (2m+1)θ.

theorem QuantumInfo.sum_sin_sq_odd_ge (θ : ℝ) (M : ℕ) (hpos : 0 < Real.sin (2 * θ)) (hM : 1 ≤ ↑M * Real.sin (2 * θ)) : ↑M / 4 ≤ ∑ m ∈ Finset.range M, Real.sin ((2 * ↑m + 1) * θ) ^ 2

The quarter bound: once the guess M satisfies M·sin 2θ ≥ 1, the average success probability of a uniformly random round count below M is at least 1/4 (the sum is at least M/4).

theorem QuantumInfo.qsearch_average {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Finset ι) (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) (ha0 : 0 < goodProb G ψ) (ha1 : goodProb G ψ < 1) (M : ℕ) (hM : 1 ≤ ↑M * (2 * √(goodProb G ψ * (1 - goodProb G ψ)))) : ↑M / 4 ≤ ∑ m ∈ Finset.range M, goodProb G ((ampStep ψ G)^[m] ψ)

★ The QSearch engine (BHMT Lemma 2 on the register): for any unit state with unknown success probability 0 < a < 1, as soon as the guess M satisfies M · 2√(a(1−a)) ≥ 1, the amplification rounds 0, …, M−1 have total success probability at least M/4 — i.e., a uniformly random round count below M succeeds with average probability ≥ 1/4, with no knowledge of a. This is the engine of BHMT's unknown-a search; the exponential-doubling schedule wrapping it (their Thm 3) is not formalised.