Point phase estimation at the amplitude-amplification rotation and the success probability itself becomes measurable, quadratically faster than sampling could ever learn it.
amplitude_estimationAmplitude amplification boosts a success probability a; amplitude estimation MEASURES it. Classically, learning a to precision 1/T costs about T-squared samples. The quantum route: the amplification step rotates its two-dimensional stage by an angle whose sine squared IS a, so the angle is sitting in the eigenvalues -- and eigenvalue angles are exactly what phase estimation reads out.
Run the rotation a controlled number of times, Fourier-read the control register, and the measured index lands near the angle with fixed odds; squaring its sine gives the estimate of a, accurate to about 1/T after only T rounds. That quadratic saving is what makes quantum counting and Monte Carlo speedups tick.
The state splits into exactly two clean branches -- clockwise and counterclockwise rotation -- and because their companions are perpendicular, the readout is an honest 50/50 mixture of two well-understood distributions, with no interference between them.
The AA-5b assembly, where three prepared layers meet in one theorem: the eigenstructure of the amplification step (its rotation plane carries eigenvectors g +- i b with eigenvalues e^(+-2 i theta)), the joint-register mixture law (orthogonal second factors kill every cross-term in a Born marginal), and the 4/pi^2 phase-estimation bound. The kickback state is proved EQUAL to a two-branch phase form, so the counting marginal is an exact half-half mixture -- an equality, not an estimate.
The stated bounds: any index in the closest-index window carries probability at least 2/pi^2; its mirror index -c carries the other branch's 2/pi^2 and decodes to the SAME estimate, so the pair jointly carries 4/pi^2; and the estimate lands within pi sqrt(a(1-a))/T + pi^2/(4 T^2) of the truth. Honest scope: the paper's literal 8/pi^2 additionally counts both rounding directions, which needs a two-index Dirichlet -kernel inequality recorded in the plan and not attempted. The standing disclaimer applies: the algorithm layer consumes the unitary pillar and does not support foundations.
With Q the amplification step at angle theta (sin theta = sqrt a) on the rotation plane, the kickback state (1/sqrt T) sum_x |x> tensor Q^x psi decomposes exactly as c_+ phaseState(theta/pi) tensor v_+ + c_- phaseState(-theta/pi) tensor v_-, where v_+- = g +- i b are the orthogonal eigenvectors, Q^x v_+- = e^(+-2 i x theta) v_+-, and |c_+-| = 1/2.
Applying the inverse QFT to the counting register and taking the Born marginal gives exactly (P_+(c) + P_-(c))/2, the half-half mixture of the two single-phase counting distributions. At any c with |theta/pi - c/T| <= 1/(2T), the plus branch contributes at least 4/pi^2, so the marginal carries at least 2/pi^2; and sin^2(pi c / T) estimates a = sin^2 theta within 2 sqrt(a(1-a)) eps + eps^2 at eps = pi/(2T), the product-form sin^2 difference identity plus the Lipschitz bound on sin.
The same four authors as amplitude amplification -- Brassard, Hoyer, Mosca and Tapp -- in the same 2000 paper, "Quantum Amplitude Amplification and Estimation". The estimation half is the paper's Theorem 12, feeding their quantum counting results: estimating how many marked items a database holds without ever listing them.
The technique is the meeting point of the field's two workhorse subroutines -- Grover's rotation geometry (1996) and Kitaev-style phase estimation (1995) -- and later became the engine of quantum Monte Carlo speedups via Montanaro's 2015 work.
CsdLean4/Mathlib/QuantumInfo/AmplitudeEstimation.leanSource links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.
Part of Constraint-Surface Dynamics · Formalised in csd-lean4.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.