Quantum phase estimation: exact readout and the 4/π² lower bound

Category: 1-Mathlib (CSD-free).

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

Phase estimation on a T-level counting register EuclideanSpace ℂ (Fin T), entirely generic in T — the standard textbook results (Nielsen–Chuang §5.2), machine-checked:

• The exact case. The inverse QFT inverts the QFT (applyQFTinv_phaseColumn), so the phase state carrying an exact phase j₀/T — the QFT column phaseColumn T j₀ — is read out as |j₀⟩ with certainty (phase_estimation_exact).

• The 4/π² bound (the headline). For an arbitrary real phase φ, the phase state phaseStateR T φ = (1/√T) ∑_x e^{2πiφx} |x⟩ read at the counting index c closest to φ·T (|φ − c/T| ≤ 1/(2T)) succeeds with probability at least 4/π² (phase_estimation_lower_bound). The amplitude is the Dirichlet sum (1/T) ∑_{x<T} e^{2πi(φ−c/T)x} (applyQFTinv_phaseStateR_apply), closed by geom_sum_eq and reduced to a ratio of sines via Complex.norm_exp_I_mul_ofReal_sub_one (prob_phaseStateR_eq); the bound is the Jordan inequality (Real.mul_abs_le_abs_sin) on the numerator against |sin t| ≤ |t| (Real.abs_sin_le_abs) on the denominator.

Support: applyQFT/applyQFTinv (the QFT action on the register, with the coordinate lemmas applyQFT_apply/applyQFTinv_apply), on the Register.lean primitives basisState/prob.

Honest scope

This is the single-phase statement: one phase state, one readout, the per-index bound. A consumer racing several eigenvalue branches (Shor's r eigenvectors, say) must control the cross-terms of its own joint state — that composition is the consumer's affair and is not done here (Empirical/QM/Algorithms/ShorCore.lean documents the deferred two-register marginal).

Provenance: extracted verbatim from ShorCore.lean (S3 + S4, 2026-08-29) — the statements never mentioned orders, orbits, or ZMod; no new mathematics. The Shor-specific bridge (qftω_div, eigenPhase_eq_phaseColumn, shor_order_readout, shor_phase_estimation_lower_bound) stays in ShorCore.lean.

The QFT action on the counting register

noncomputable def QuantumInfo.applyQFT (T : ℕ) (ψ : EuclideanSpace ℂ (Fin T)) : EuclideanSpace ℂ (Fin T)

The QFT action on the counting register.

Equations

• QuantumInfo.applyQFT T ψ = (Matrix.toEuclideanLin (QuantumInfo.qftMatrix T)) ψ

noncomputable def QuantumInfo.applyQFTinv (T : ℕ) (ψ : EuclideanSpace ℂ (Fin T)) : EuclideanSpace ℂ (Fin T)

The inverse-QFT action on the counting register (Fᴴ).

Equations

• QuantumInfo.applyQFTinv T ψ = (Matrix.toEuclideanLin (QuantumInfo.qftMatrix T).conjTranspose) ψ

theorem QuantumInfo.applyQFT_apply (T : ℕ) (ψ : EuclideanSpace ℂ (Fin T)) (y : Fin T) : (applyQFT T ψ).ofLp y = ∑ x : Fin T, qftMatrix T y x * ψ.ofLp x

theorem QuantumInfo.applyQFTinv_apply (T : ℕ) (ψ : EuclideanSpace ℂ (Fin T)) (y : Fin T) : (applyQFTinv T ψ).ofLp y = ∑ x : Fin T, (qftMatrix T).conjTranspose y x * ψ.ofLp x

The exact case: a QFT column is read with certainty

noncomputable def QuantumInfo.phaseColumn (T : ℕ) (j₀ : Fin T) : EuclideanSpace ℂ (Fin T)

The QFT column j₀: the phase state (1/√T) ∑_x ω_T^{x j₀} |x⟩.

Equations

• QuantumInfo.phaseColumn T j₀ = QuantumInfo.applyQFT T (QuantumInfo.basisState j₀)

@[simp]

theorem QuantumInfo.phaseColumn_apply (T : ℕ) (j₀ x : Fin T) : (phaseColumn T j₀).ofLp x = (↑√↑T)⁻¹ * qftω T ^ (↑x * ↑j₀)

theorem QuantumInfo.applyQFTinv_phaseColumn (T : ℕ) [NeZero T] (j₀ : Fin T) : applyQFTinv T (phaseColumn T j₀) = basisState j₀

Phase-estimation exactness: the inverse QFT inverts the QFT, so the QFT column j₀ is sent back to the basis state |j₀⟩.

theorem QuantumInfo.phase_estimation_exact (T : ℕ) [NeZero T] (j₀ : Fin T) : prob (applyQFTinv T (phaseColumn T j₀)) j₀ = 1

The exact case: phase estimation reads the QFT column j₀ with certainty.

The general case: the 4/π² lower bound (Dirichlet kernel)

For a phase state carrying a real phase φ, inverse-QFT concentrates the amplitude near c ≈ φ·T. When c is the closest counting index to φ·T (|φ − c/T| ≤ 1/(2T)), the readout probability is at least 4/π², the Dirichlet-kernel constant.

noncomputable def QuantumInfo.phaseStateR (T : ℕ) (φ : ℝ) : EuclideanSpace ℂ (Fin T)

The counting-register phase state carrying a real phase φ: phaseStateR φ = (1/√T) ∑_x e^{2πi φ x} |x⟩. For φ = j₀/T this is phaseColumn T j₀, no longer required to land on an exact QFT column.

Equations

• QuantumInfo.phaseStateR T φ = (↑√↑T)⁻¹ • ∑ x : Fin T, Complex.exp (2 * ↑Real.pi * Complex.I * ↑φ * ↑↑x) • QuantumInfo.basisState x

theorem QuantumInfo.applyQFTinv_phaseStateR_apply (T : ℕ) (φ : ℝ) (c : Fin T) : (applyQFTinv T (phaseStateR T φ)).ofLp c = (↑T)⁻¹ * ∑ x : Fin T, Complex.exp (2 * ↑Real.pi * Complex.I * ↑(φ - ↑↑c / ↑T) * ↑↑x)

The inverse-QFT amplitude of the phase state. Reading out index c, the amplitude is the Dirichlet sum (1/T) ∑_{x<T} e^{2πi (φ − c/T) x}. The two (√T)⁻¹ factors (one from the phase state, one from Fᴴ) collapse to T⁻¹; the per-term phases e^{2πiφx} and conj(ω_T)^{xc} merge into e^{2πi(φ − c/T)x}.

theorem QuantumInfo.prob_phaseStateR_eq (T : ℕ) [NeZero T] (φ : ℝ) (c : Fin T) (hsin : Real.sin (Real.pi * (φ - ↑↑c / ↑T)) ≠ 0) : prob (applyQFTinv T (phaseStateR T φ)) c = (↑T)⁻¹ ^ 2 * (Real.sin (Real.pi * (φ - ↑↑c / ↑T) * ↑T) ^ 2 / Real.sin (Real.pi * (φ - ↑↑c / ↑T)) ^ 2)

The closed-form readout probability. With δ = φ − c/T and z = e^{2πiδ}: in the on-resonance case δ = 0 the amplitude is 1 (so prob = 1); off resonance with sin(πδ) ≠ 0 the geometric sum collapses (geom_sum_eq) and the norm reduces, via Complex.norm_exp_I_mul_ofReal_sub_one, to prob = T⁻² · sin²(πδT) / sin²(πδ).

theorem QuantumInfo.phase_estimation_lower_bound (T : ℕ) [NeZero T] (φ : ℝ) (c : Fin T) (hδ : |φ - ↑↑c / ↑T| ≤ 1 / (2 * ↑T)) : 4 / Real.pi ^ 2 ≤ prob (applyQFTinv T (phaseStateR T φ)) c

The 4/π² phase-estimation lower bound (HEADLINE). For any real phase φ and a counting index c that is the closest index to φ·T (|φ − c/T| ≤ 1/(2T)), inverse-QFT reads out c with probability at least 4/π². On resonance (φ = c/T) the probability is 1; otherwise the Jordan inequality bounds the Dirichlet numerator from below and |sin t| ≤ |t| the denominator from above. Nielsen–Chuang §5.2.