Quantum phase estimation: exact readout, the 4/π² bound and the two-index 8/π² 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.

• The two-index 8/π² bound. Both grid points straddling φ·T — c at phase distance 0 ≤ φ − c/T ≤ 1/T and c + 1 (read modulo T) — jointly carry at least 8/π² (phase_estimation_two_index, BHMT Theorem 11 at k = 1), from the two-index Dirichlet bound dirichlet_two_index and the elementary inequality sin²(πx)(1/x² + 1/(1−x)²) ≥ 8 (eight_mul_sq_le_sin_sq_pi_mul); a lower straddling index exists for every phase in [0, 1) (exists_straddle_index).

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.

Both grid points: the two-index 8/π² bound (BHMT Theorem 11, k = 1)

phase_estimation_lower_bound is the single-index 4/π². Counting both counting indices straddling φ·T — the lower one at phase distance δ ∈ [0, 1/T] and the upper one at 1/T − δ — the pair carries 8/π². This is a genuinely two-index inequality on the Dirichlet kernel: a single index at distance up to 1/T can carry probability 0. The analytic core is eight_mul_sq_le_sin_sq_pi_mul, the elementary inequality sin²(πx) (1/x² + 1/(1−x)²) ≥ 8 on (0, 1) (equality at x = 1/2).

theorem QuantumInfo.eight_mul_sq_le_sin_sq_pi_mul_of_le_quarter {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1 / 4) : 8 * (x * (1 - x)) ^ 2 ≤ Real.sin (Real.pi * x) ^ 2 * (x ^ 2 + (1 - x) ^ 2)

The cubic range 0 < x ≤ 1/4: sin t ≥ t − t³/6 at t = πx, then a polynomial estimate with 3.1415 < π < 3.1416.

theorem QuantumInfo.eight_mul_sq_le_sin_sq_pi_mul_of_quarter_le {x : ℝ} (hx : 1 / 4 ≤ x) (hx' : x ≤ 1 / 2) : 8 * (x * (1 - x)) ^ 2 ≤ Real.sin (Real.pi * x) ^ 2 * (x ^ 2 + (1 - x) ^ 2)

The cosine range 1/4 ≤ x ≤ 1/2: sin(πx) = cos(πy) with y = 1/2 − x, cos t ≥ 1 − t²/2, then a polynomial estimate in v = y² ≤ 1/16.

theorem QuantumInfo.eight_mul_sq_le_sin_sq_pi_mul_of_le_half {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1 / 2) : 8 * (x * (1 - x)) ^ 2 ≤ Real.sin (Real.pi * x) ^ 2 * (x ^ 2 + (1 - x) ^ 2)

The half range 0 < x ≤ 1/2, the two ranges joined at 1/4.

theorem QuantumInfo.eight_mul_sq_le_sin_sq_pi_mul {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : 8 * (x * (1 - x)) ^ 2 ≤ Real.sin (Real.pi * x) ^ 2 * (x ^ 2 + (1 - x) ^ 2)

★ The two-point kernel inequality. For 0 < x < 1, sin²(πx) · (x² + (1−x)²) ≥ 8 · (x(1−x))², i.e. sin²(πx)(1/x² + 1/(1−x)²) ≥ 8, with equality at x = 1/2. The bound BHMT assert by calculus in the proof of their Theorem 11.

theorem QuantumInfo.phaseStateR_add_one (T : ℕ) (φ : ℝ) : phaseStateR T (φ + 1) = phaseStateR T φ

The phase state is 1-periodic in the phase: e^{2πi(φ+1)x} = e^{2πiφx}.

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

Reading index c at phase φ is reading index 0 at phase φ − c/T: the Dirichlet amplitude depends only on the difference.

theorem QuantumInfo.prob_applyQFTinv_phaseStateR_zero (T : ℕ) [NeZero T] : prob (applyQFTinv T (phaseStateR T 0)) 0 = 1

On resonance the readout is certain: prob (phaseStateR T 0) 0 = 1.

theorem QuantumInfo.dirichlet_two_index (T : ℕ) [NeZero T] (δ : ℝ) (hlo : 0 ≤ δ) (hhi : δ ≤ 1 / ↑T) : 8 / Real.pi ^ 2 ≤ prob (applyQFTinv T (phaseStateR T δ)) 0 + prob (applyQFTinv T (phaseStateR T (δ - 1 / ↑T))) 0

★ The two-index Dirichlet bound. For 0 ≤ δ ≤ 1/T the two readouts at phase distance δ and δ − 1/T — the two grid points straddling the phase — jointly carry at least 8/π². On the boundary one of them is on resonance; inside, both closed forms (prob_phaseStateR_eq) share the numerator sin²(πδT), the denominators are bounded by |sin t| ≤ |t|, and eight_mul_sq_le_sin_sq_pi_mul at x = δT finishes.

theorem QuantumInfo.val_add_one_fin_of_lt (T : ℕ) [NeZero T] {c : Fin T} (h : ↑c + 1 < T) : ↑(c + 1) = ↑c + 1

(c + 1 : Fin T) below the wrap: its value is c + 1.

theorem QuantumInfo.val_add_one_fin_of_eq (T : ℕ) [NeZero T] {c : Fin T} (h : ↑c + 1 = T) : ↑(c + 1) = 0

(c + 1 : Fin T) at the wrap c = T − 1: its value is 0.

theorem QuantumInfo.exists_straddle_index (T : ℕ) [NeZero T] (φ : ℝ) (h0 : 0 ≤ φ) (h1 : φ < 1) : ∃ (c : Fin T), 0 ≤ φ - ↑↑c / ↑T ∧ φ - ↑↑c / ↑T ≤ 1 / ↑T

The lower straddling index exists: for 0 ≤ φ < 1 the index c = ⌊φT⌋ has 0 ≤ φ − c/T ≤ 1/T.

theorem QuantumInfo.phase_estimation_two_index (T : ℕ) [NeZero T] (φ : ℝ) (c : Fin T) (hlo : 0 ≤ φ - ↑↑c / ↑T) (hhi : φ - ↑↑c / ↑T ≤ 1 / ↑T) : 8 / Real.pi ^ 2 ≤ prob (applyQFTinv T (phaseStateR T φ)) c + prob (applyQFTinv T (phaseStateR T φ)) (c + 1)

★★ The two-index phase-estimation bound (BHMT Theorem 11, k = 1, one phase). If the counting index c sits at phase distance 0 ≤ φ − c/T ≤ 1/T below the phase, then c and c + 1 — the two grid points straddling φ·T, the second read modulo T — jointly carry at least 8/π².