Amplitude estimation: the kickback marginal, the success bounds and BHMT's 8/π²

Category: 1-Mathlib (CSD-free).

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

The assembly of the three prepared layers (plan specs/amplitude-amplification-plan.md, AA-5b): phase estimation run on the amplification step Q estimates the rotation angle θ, hence the amplitude a = sin²θ.

• The kickback state kickbackState T φ G ψ = (1/√T) ∑_x |x⟩ ⊗ Qˣψ — the joint state a controlled-Q ladder prepares.

• ★ The two-branch phase form (kickbackState_ampState): on the rotation plane the kickback state is EXACTLY a sum of two product states, c₊·(phaseStateR (θ/π)) ⊗ v₊ + c₋·(phaseStateR (−θ/π)) ⊗ v₋, with orthogonal eigenvector companions v± and branch coefficients of modulus 1/2 — the eigen-decomposition of ampState threaded through the iterated eigen-action.

• ★ The exact marginal (amplitude_estimation_marginal): after the counting-register inverse QFT, the Born marginal at every index c is the half-half mixture (P₊(c) + P₋(c))/2 of the two single-phase counting distributions — every cross-term dead against ⟪v₊, v₋⟫ = 0 (probLeft_add_tensor_orthogonal).

• ★★ The success bound (amplitude_estimation): at any index c within the closest-index window of θ/π (the hypothesis of phase_estimation_lower_bound), the marginal carries at least 2/π².

• ★ The accuracy reading (amplitude_estimation_close): any index in that window yields the estimate ã = sin²(πc/T) with |ã − a| ≤ π√(a(1−a))/T + π²/(4T²) — the AA-5a error algebra at ε = π/(2T). (BHMT state 2π√(a(1−a))/T + π²/T² from ε = π/T; the closest-index window gives the sharper constant.)

• ★★ BHMT's literal 8/π² (their Theorem 11, k = 1) (amplitude_estimation_bhmt): with c the lower of the two grid points straddling Tθ/π, the accepted set straddleIndices T c = {c, c + 1, −c, −(c + 1)} carries at least 8/π² (amplitude_estimation_straddle) and every index in it decodes within 2π√(a(1−a))/T + π²/T² (amplitude_estimation_straddle_close) — the paper's constants.

Honest scope

amplitude_estimation is the single-branch, single-index 2/π². The mirror section doubles it: the − branch's distribution is the exact mirror image of the + branch's (prob_applyQFTinv_phaseStateR_neg, a conjugation symmetry), so the mirror index −c also carries 2/π² (amplitude_estimation_mirror), both indices yield the same estimate sin²(πc/T) (sin_sq_mirror), and the pair carries 4/π² (★ amplitude_estimation_pair); when c = −c (only c = 0, or c = T/2 for even T) that pair sum double-counts one index — the bound still holds literally, but the "measure c or −c" reading collapses to a single index there. The straddle section reaches the paper's 8/π² by counting both rounding directions: the two-index Dirichlet bound phase_estimation_two_index (the kernel inequality f(δ) + f(δ − 1/T) ≥ 8/π², PhaseEstimation.lean) on each branch, the accepted set a Finset so that coincidences merge rather than double-count. Query counting is by rounds of the abstract step; no controlled-gate decomposition is claimed. The construction takes the rotation-plane data (g, b, θ) as input — the plane exists for any state with 0 < goodProb < 1 (ampState_decomposition in AmplitudeAmplification.lean).

The kickback state

noncomputable def QuantumInfo.kickbackState {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) (φ : EuclideanSpace ℂ ι) (G : Finset ι) (ψ : EuclideanSpace ℂ ι) : EuclideanSpace ℂ (Fin T × ι)

The phase-kickback state of the amplification step: (1/√T) ∑_x |x⟩ ⊗ Qˣψ, the joint counting/work state a controlled-Q ladder prepares from |counting uniform⟩ ⊗ ψ.

Equations

• QuantumInfo.kickbackState T φ G ψ = (↑√↑T)⁻¹ • ∑ x : Fin T, QuantumInfo.tensorState (QuantumInfo.basisState x) ((QuantumInfo.ampStep φ G)^[↑x] ψ)

noncomputable def QuantumInfo.branchPlus (θ : ℝ) : ℂ

The + branch coefficient (−i/2)e^{iθ}.

Equations

• QuantumInfo.branchPlus θ = -Complex.I / 2 * Complex.exp (↑θ * Complex.I)

noncomputable def QuantumInfo.branchMinus (θ : ℝ) : ℂ

The − branch coefficient (i/2)e^{−iθ}.

Equations

• QuantumInfo.branchMinus θ = Complex.I / 2 * Complex.exp (↑(-θ) * Complex.I)

theorem QuantumInfo.norm_branchPlus (θ : ℝ) : ‖branchPlus θ‖ = 1 / 2

theorem QuantumInfo.norm_branchMinus (θ : ℝ) : ‖branchMinus θ‖ = 1 / 2

theorem QuantumInfo.kickbackState_ampState {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) {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) (θ : ℝ) : kickbackState T (ampState g b θ) G (ampState g b θ) = tensorState (branchPlus θ • phaseStateR T (θ / Real.pi)) (eigenPlus g b) + tensorState (branchMinus θ • phaseStateR T (-(θ / Real.pi))) (eigenMinus g b)

★ The two-branch phase form of the kickback state. On the rotation plane, the kickback state of Q = ampStep (ampState θ) G on ψ = ampState θ is exactly a sum of two product states: each eigen-branch picks up the geometric phase e^{±2ixθ}, which is the phase state phaseStateR T (±θ/π) on the counting register.

The exact counting marginal, and the success bound

theorem QuantumInfo.toEuclideanLin_qftInv (T : ℕ) (ψ : EuclideanSpace ℂ (Fin T)) : (Matrix.toEuclideanLin (qftMatrix T).conjTranspose) ψ = applyQFTinv T ψ

The inverse QFT as the first-factor kernel: definitional bridge.

theorem QuantumInfo.amplitude_estimation_marginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) {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) (θ : ℝ) (c : Fin T) : probLeft (matrixLeft (qftMatrix T).conjTranspose (kickbackState T (ampState g b θ) G (ampState g b θ))) c = (prob (applyQFTinv T (phaseStateR T (θ / Real.pi))) c + prob (applyQFTinv T (phaseStateR T (-(θ / Real.pi)))) c) / 2

★ The exact counting marginal of the processed kickback state: at every index c, the Born marginal after the counting-register inverse QFT is the half-half mixture of the two single-phase distributions. No cross-terms: the eigenvector companions are orthogonal.

theorem QuantumInfo.amplitude_estimation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) [NeZero T] {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) (θ : ℝ) (c : Fin T) (hclose : |θ / Real.pi - ↑↑c / ↑T| ≤ 1 / (2 * ↑T)) : 2 / Real.pi ^ 2 ≤ probLeft (matrixLeft (qftMatrix T).conjTranspose (kickbackState T (ampState g b θ) G (ampState g b θ))) c

★★ The amplitude-estimation success bound (BHMT Thm 12, per-index form). At any counting index c within the closest-index window of θ/π, the measured marginal carries at least 2/π²: the + branch's 4/π² phase-estimation weight, halved by the branch probability.

theorem QuantumInfo.amplitude_estimation_close (T : ℕ) [NeZero T] {a : ℝ} (ha0 : 0 ≤ a) {θ : ℝ} (hθ : Real.sin θ = √a) (hθc : Real.cos θ = √(1 - a)) (c : Fin T) (hclose : |θ / Real.pi - ↑↑c / ↑T| ≤ 1 / (2 * ↑T)) : |Real.sin (Real.pi * ↑↑c / ↑T) ^ 2 - a| ≤ Real.pi * √(a * (1 - a)) / ↑T + Real.pi ^ 2 / (4 * ↑T ^ 2)

★ The accuracy of the estimate (BHMT Lemma 7 instantiated). Any index in the closest-index window yields the amplitude estimate ã = sin²(πc/T) with |ã − a| ≤ π√(a(1−a))/T + π²/(4T²).

The mirror index: both branches counted

The − branch's counting distribution is the exact mirror image of the + branch's: negating the phase and the index conjugates every amplitude. So the mirror index −c carries the − branch's 4/π², it decodes to the same amplitude estimate, and accepting {c, −c} doubles the success bound to 4/π².

theorem QuantumInfo.val_neg_fin (T : ℕ) (c : Fin T) : ↑(-c) = (T - ↑c) % T

The ℕ-value of the negated index: (−c : Fin T) = (T − c) % T.

theorem QuantumInfo.applyQFTinv_phaseStateR_neg_neg (T : ℕ) [NeZero T] (φ : ℝ) (c : Fin T) : (applyQFTinv T (phaseStateR T (-φ))).ofLp (-c) = (starRingEnd ℂ) ((applyQFTinv T (phaseStateR T φ)).ofLp c)

The conjugation symmetry: negating both the phase and the counting index conjugates the processed amplitude.

theorem QuantumInfo.prob_applyQFTinv_phaseStateR_neg (T : ℕ) [NeZero T] (φ : ℝ) (c : Fin T) : prob (applyQFTinv T (phaseStateR T (-φ))) (-c) = prob (applyQFTinv T (phaseStateR T φ)) c

The mirror distribution: the − branch at the mirror index equals the + branch at the original index.

theorem QuantumInfo.sin_sq_mirror (T : ℕ) [NeZero T] (c : Fin T) : Real.sin (Real.pi * ↑↑(-c) / ↑T) ^ 2 = Real.sin (Real.pi * ↑↑c / ↑T) ^ 2

The mirror index decodes to the same estimate: sin²(π·(−c)/T) = sin²(π·c/T).

theorem QuantumInfo.amplitude_estimation_mirror {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) [NeZero T] {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) (θ : ℝ) (c : Fin T) (hclose : |θ / Real.pi - ↑↑c / ↑T| ≤ 1 / (2 * ↑T)) : 2 / Real.pi ^ 2 ≤ probLeft (matrixLeft (qftMatrix T).conjTranspose (kickbackState T (ampState g b θ) G (ampState g b θ))) (-c)

The mirror index also carries 2/π²: under the same closest-index hypothesis for θ/π, the − branch concentrates at −c.

theorem QuantumInfo.amplitude_estimation_pair {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) [NeZero T] {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) (θ : ℝ) (c : Fin T) (hclose : |θ / Real.pi - ↑↑c / ↑T| ≤ 1 / (2 * ↑T)) : 4 / Real.pi ^ 2 ≤ probLeft (matrixLeft (qftMatrix T).conjTranspose (kickbackState T (ampState g b θ) G (ampState g b θ))) c + probLeft (matrixLeft (qftMatrix T).conjTranspose (kickbackState T (ampState g b θ) G (ampState g b θ))) (-c)

★ The both-branch success bound (the mirror refinement): the pair {c, −c} — two indices decoding to the same estimate (sin_sq_mirror) — jointly carries at least 4/π². When c = −c (only c = 0, or c = T/2 for even T) the sum double-counts a single index; the inequality still holds literally. BHMT's 8/π² counts both rounding directions: amplitude_estimation_straddle below.

Both rounding directions: BHMT's literal 8/π² (Theorem 11, k = 1)

amplitude_estimation_pair counts one grid point per branch. Counting both grid points straddling Tθ/π — c at phase distance δ ∈ [0, 1/T] below and c + 1 at 1/T − δ above — and their mirrors for the − branch gives the paper's constant: the two-index Dirichlet bound phase_estimation_two_index on each branch, halved by the branch weight and summed. The accepted set is a Finset, so coincidences among the four indices are merged, never double-counted; every accepted index decodes within the paper's error 2π√(a(1−a))/T + π²/T².

def QuantumInfo.straddleIndices (T : ℕ) [NeZero T] (c : Fin T) : Finset (Fin T)

The accepted counting indices: both grid points straddling Tθ/π and their mirrors.

Equations

• QuantumInfo.straddleIndices T c = {c, c + 1, -c, -(c + 1)}

theorem QuantumInfo.ne_add_one_fin (T : ℕ) [NeZero T] (hT : 2 ≤ T) (c : Fin T) : c ≠ c + 1

For T ≥ 2 the two straddling indices are distinct.

theorem QuantumInfo.amplitude_estimation_straddle {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) [NeZero T] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hT : 2 ≤ T) (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) (θ : ℝ) (c : Fin T) (hlo : 0 ≤ θ / Real.pi - ↑↑c / ↑T) (hhi : θ / Real.pi - ↑↑c / ↑T ≤ 1 / ↑T) : 8 / Real.pi ^ 2 ≤ ∑ i ∈ straddleIndices T c, probLeft (matrixLeft (qftMatrix T).conjTranspose (kickbackState T (ampState g b θ) G (ampState g b θ))) i

★★ The both-rounding success bound (BHMT Theorem 11, k = 1, the probability half). If c sits at phase distance 0 ≤ θ/π − c/T ≤ 1/T below θ/π, the four accepted indices {c, c + 1, −c, −(c + 1)} jointly carry at least 8/π² of the measured marginal: each branch puts 8/π² on its own straddling pair (phase_estimation_two_index, the − branch through the mirror prob_applyQFTinv_phaseStateR_neg), and the branch weights are 1/2 each.

theorem QuantumInfo.amplitude_estimation_straddle_close (T : ℕ) [NeZero T] {a : ℝ} (ha0 : 0 ≤ a) {θ : ℝ} (hθ : Real.sin θ = √a) (hθc : Real.cos θ = √(1 - a)) (c : Fin T) (hlo : 0 ≤ θ / Real.pi - ↑↑c / ↑T) (hhi : θ / Real.pi - ↑↑c / ↑T ≤ 1 / ↑T) {i : Fin T} (hi : i ∈ straddleIndices T c) : |Real.sin (Real.pi * ↑↑i / ↑T) ^ 2 - a| ≤ 2 * Real.pi * √(a * (1 - a)) / ↑T + Real.pi ^ 2 / ↑T ^ 2

★ The accuracy of every accepted index (BHMT Lemma 7 at ε = π/T). Each index in straddleIndices T c decodes to ã = sin²(πi/T) with |ã − a| ≤ 2π√(a(1−a))/T + π²/T² — the paper's literal constants. The upper index c + 1 is read modulo T; at the wrap it decodes to sin²(0) = sin²(π) = 0.

theorem QuantumInfo.amplitude_estimation_bhmt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : ℕ) [NeZero T] {G : Finset ι} {g b : EuclideanSpace ℂ ι} (hT : 2 ≤ T) (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) {a : ℝ} (ha0 : 0 ≤ a) {θ : ℝ} (hθ : Real.sin θ = √a) (hθc : Real.cos θ = √(1 - a)) (c : Fin T) (hlo : 0 ≤ θ / Real.pi - ↑↑c / ↑T) (hhi : θ / Real.pi - ↑↑c / ↑T ≤ 1 / ↑T) : (∀ i ∈ straddleIndices T c, |Real.sin (Real.pi * ↑↑i / ↑T) ^ 2 - a| ≤ 2 * Real.pi * √(a * (1 - a)) / ↑T + Real.pi ^ 2 / ↑T ^ 2) ∧ 8 / Real.pi ^ 2 ≤ ∑ i ∈ straddleIndices T c, probLeft (matrixLeft (qftMatrix T).conjTranspose (kickbackState T (ampState g b θ) G (ampState g b θ))) i

★★ BHMT Theorem 11 (k = 1). For T ≥ 2 and a lower straddling index c of θ/π (one exists for every 0 ≤ θ/π < 1, exists_straddle_index), every accepted index decodes within 2π√(a(1−a))/T + π²/T² of a = sin²θ, and the accepted set carries probability at least 8/π².