Amplitude estimation: the kickback marginal and the per-index success bound (BHMT Thm 12)

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.)

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). Two honest residues: (i) when c = −c (only c = 0, or c = T/2 for even T) the pair sum double-counts one index — the bound still holds literally, but the "measure c or −c" reading collapses to a single index there; (ii) BHMT's literal 8/π² (their Thm 11) additionally counts both rounding directions — the two grid points straddling Tθ/π — which needs a two-index lower bound on the Dirichlet kernel (f(δ) + f(1/T − δ) ≥ 8/π², a genuine new kernel inequality, NOT downstream arithmetic; a single index at distance up to 1/T can carry probability 0). That inequality is not attempted — ⚠️ RESIDUE(R-001); the corpus's bound on the estimate tops out at 4/π². 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/π² additionally needs the both-rounding-directions kernel inequality — see the module header.