Grover's search algorithm (R5+) — as an instance of amplitude amplification

Category: 3-Local (QM-validity).

Grover's algorithm: search for a single marked item w : Fin n → Fin 2 in an unstructured database of N = 2ⁿ items. The search step is the composition of the oracle (phase flip on w, I - 2|w⟩⟨w|) and the diffusion operator (inversion about the mean, 2|s⟩⟨s| - I, where |s⟩ is the uniform superposition).

Rebuilt 2026-08-29 (plan specs/amplitude-amplification-plan.md, brick AA-3): the step operators are proved to be the BHMT amplification step of Mathlib/QuantumInfo/AmplitudeAmplification.lean — oracle w = oracleFlip {w} (oracle_eq_oracleFlip) and diffusion = reflect uniformState (diffusion_eq_reflect) — and the headline is re-derived from the general theorem: the uniform state is the rotation-plane state at the Grover angle (uniformState_eq_ampState), so ampStep_iterate gives

grover_success : prob ((groverStep w)^[k] uniformState) w = sin²((2k+1)·θ),

sin θ = 1/√N. The file's previous self-contained rotation development (the symState coefficient family and its operator-action lemmas) is retired — the general two-reflection rotation now carries it, and keeping both would be exactly the parallel-development duplication the Algorithm Atlas assessment (RESULT 4) documents. New at the same stroke, free from the general theorem: the k-marked-items distribution grover_multi_success, which the single-marked file could not state.

Honest scope. QM-validity breadth: genuine reflection operators on the EuclideanSpace inner-product structure; amplitudes real, carried as ℂ-coercions. The optimal iteration count and the success bound live with the general theorem (amplitude_amplification_succeeds, amplification_query_bound) — the deferral the earlier version of this file recorded is closed there, not here. Round counting is abstract-step counting; no oracle model is claimed.

Extraction cost record (the atlas assessment's priced pilot, AA-3): the rebuild of this file on the general theorem — bridge lemmas, plane instantiation, re-derived headlines, deleted parallel development — took ≈25 minutes wall-clock including two build-fix iterations (2026-08-29, 14:22–14:47 session segment). The full AA-1..AA-3 session (general module written and debugged + this refactor) was ≈90 minutes. See specs/amplitude-amplification-plan.md.

noncomputable def CSD.Empirical.QM.Grover.databaseSize (n : ℕ) : ℝ

The database size N = 2ⁿ as a real number.

Equations

• CSD.Empirical.QM.Grover.databaseSize n = 2 ^ n

noncomputable def CSD.Empirical.QM.Grover.J (n : ℕ) : QuantumInfo.QReg n

The all-ones vector J = ∑ z |z⟩: amplitude 1 on every basis state.

Equations

• CSD.Empirical.QM.Grover.J n = ∑ z : Fin n → Fin 2, QuantumInfo.basisState z

theorem CSD.Empirical.QM.Grover.J_coord {n : ℕ} (z : Fin n → Fin 2) : (J n).ofLp z = ∑ x : Fin n → Fin 2, (QuantumInfo.basisState x).ofLp z

@[simp]

theorem CSD.Empirical.QM.Grover.J_apply {n : ℕ} (z : Fin n → Fin 2) : (J n).ofLp z = 1

noncomputable def CSD.Empirical.QM.Grover.uniformState {n : ℕ} : QuantumInfo.QReg n

The uniform superposition |s⟩ = (1/√N) ∑ z |z⟩.

Equations

• CSD.Empirical.QM.Grover.uniformState = (√(CSD.Empirical.QM.Grover.databaseSize n))⁻¹ • CSD.Empirical.QM.Grover.J n

@[simp]

theorem CSD.Empirical.QM.Grover.uniformState_apply {n : ℕ} (z : Fin n → Fin 2) : uniformState.ofLp z = (↑√(databaseSize n))⁻¹

theorem CSD.Empirical.QM.Grover.sqrt_two_pow_eq (n : ℕ) : √(2 ^ n) = √2 ^ n

√(2ⁿ) = (√2)ⁿ (the principal root commutes with the nonnegative power).

theorem CSD.Empirical.QM.Grover.uniformState_eq_hadamard {n : ℕ} : uniformState = QuantumInfo.applyHn (QuantumInfo.basisState 0)

The Grover entry point is the Hadamard output: uniformState = H^⊗n |0ⁿ⟩. This ties the uniform superposition (defined here as the normalized all-ones vector) to the R2 Hadamard layer, where Hn_apply_zero gives the same amplitude (√2⁻¹)ⁿ = (√(2ⁿ))⁻¹ on every basis state.

noncomputable def CSD.Empirical.QM.Grover.oracle {n : ℕ} (w : Fin n → Fin 2) (ψ : QuantumInfo.QReg n) : QuantumInfo.QReg n

The oracle O_w = I - 2|w⟩⟨w|: a phase flip on the marked item w.

Equations

• CSD.Empirical.QM.Grover.oracle w ψ = ψ - (2 * ψ.ofLp w) • QuantumInfo.basisState w

noncomputable def CSD.Empirical.QM.Grover.diffusion {n : ℕ} (ψ : QuantumInfo.QReg n) : QuantumInfo.QReg n

The diffusion operator 2|s⟩⟨s| - I: inversion about the mean.

Equations

• CSD.Empirical.QM.Grover.diffusion ψ = (2 * inner ℂ CSD.Empirical.QM.Grover.uniformState ψ) • CSD.Empirical.QM.Grover.uniformState - ψ

noncomputable def CSD.Empirical.QM.Grover.groverStep {n : ℕ} (w : Fin n → Fin 2) (ψ : QuantumInfo.QReg n) : QuantumInfo.QReg n

One Grover step: oracle then diffusion.

Equations

• CSD.Empirical.QM.Grover.groverStep w ψ = CSD.Empirical.QM.Grover.diffusion (CSD.Empirical.QM.Grover.oracle w ψ)

The bridge: Grover's operators ARE the BHMT amplification step

theorem CSD.Empirical.QM.Grover.oracle_eq_oracleFlip {n : ℕ} (w : Fin n → Fin 2) (ψ : QuantumInfo.QReg n) : oracle w ψ = QuantumInfo.oracleFlip {w} ψ

The oracle is the good-set reflection at G = {w}.

theorem CSD.Empirical.QM.Grover.diffusion_eq_reflect {n : ℕ} (ψ : QuantumInfo.QReg n) : diffusion ψ = QuantumInfo.reflect uniformState ψ

The diffusion is the reflection about the uniform state.

theorem CSD.Empirical.QM.Grover.groverStep_eq_ampStep {n : ℕ} (w : Fin n → Fin 2) : groverStep w = QuantumInfo.ampStep uniformState {w}

One Grover step is one amplification step at φ = uniformState, G = {w}.

The rotation plane: |w⟩ and the normalized rest

theorem CSD.Empirical.QM.Grover.one_le_two_pow {n : ℕ} : 1 ≤ 2 ^ n

1 ≤ 2ⁿ as a real, hence 0 ≤ 2ⁿ - 1.

theorem CSD.Empirical.QM.Grover.two_le_two_pow {n : ℕ} (hn : 1 ≤ n) : 2 ≤ 2 ^ n

For n ≥ 1, 2 ≤ 2ⁿ as a real, hence 1 ≤ 2ⁿ - 1.

theorem CSD.Empirical.QM.Grover.sqrt_sub_one_mul_self {n : ℕ} : √(2 ^ n - 1) * √(2 ^ n - 1) = 2 ^ n - 1

√(N-1) · √(N-1) = N - 1.

theorem CSD.Empirical.QM.Grover.sqrt_sub_one_ne {n : ℕ} (hn : 1 ≤ n) : √(2 ^ n - 1) ≠ 0

noncomputable def CSD.Empirical.QM.Grover.restState {n : ℕ} (w : Fin n → Fin 2) : QuantumInfo.QReg n

The normalized rest state (√(N-1))⁻¹ (J − |w⟩): the bad unit component of the uniform state against {w}.

Equations

• CSD.Empirical.QM.Grover.restState w = (↑√(2 ^ n - 1))⁻¹ • (CSD.Empirical.QM.Grover.J n - QuantumInfo.basisState w)

theorem CSD.Empirical.QM.Grover.restState_apply {n : ℕ} (w z : Fin n → Fin 2) : (restState w).ofLp z = (↑√(2 ^ n - 1))⁻¹ * (1 - if z = w then 1 else 0)

theorem CSD.Empirical.QM.Grover.sum_ite_single {n : ℕ} (w : Fin n → Fin 2) (a b : ℂ) : (∑ z : Fin n → Fin 2, if z = w then a else b) = a + (2 ^ n - 1) * b

∑ z, (if z = w then a else b) = a + (N-1)·b.

theorem CSD.Empirical.QM.Grover.basisState_supp {n : ℕ} (w z : Fin n → Fin 2) : z ∉ {w} → (QuantumInfo.basisState w).ofLp z = 0

The marked basis state is supported on {w}.

theorem CSD.Empirical.QM.Grover.restState_supp {n : ℕ} (w z : Fin n → Fin 2) : z ∈ {w} → (restState w).ofLp z = 0

The rest state vanishes on {w}.

theorem CSD.Empirical.QM.Grover.inner_basis_self {n : ℕ} (w : Fin n → Fin 2) : inner ℂ (QuantumInfo.basisState w) (QuantumInfo.basisState w) = 1

⟨|w⟩, |w⟩⟩ = 1.

theorem CSD.Empirical.QM.Grover.inner_rest_self {n : ℕ} (hn : 1 ≤ n) (w : Fin n → Fin 2) : inner ℂ (restState w) (restState w) = 1

⟨rest, rest⟩ = 1 for n ≥ 1.

theorem CSD.Empirical.QM.Grover.inner_basis_rest {n : ℕ} (w : Fin n → Fin 2) : inner ℂ (QuantumInfo.basisState w) (restState w) = 0

⟨|w⟩, rest⟩ = 0.

theorem CSD.Empirical.QM.Grover.uniformState_eq_ampState {n : ℕ} (hn : 1 ≤ n) (w : Fin n → Fin 2) {θ : ℝ} (hsin : Real.sin θ = (√(2 ^ n))⁻¹) (hcos : Real.cos θ = √(2 ^ n - 1) / √(2 ^ n)) : uniformState = QuantumInfo.ampState (QuantumInfo.basisState w) (restState w) θ

The uniform state is the rotation-plane state at the Grover angle: given sin θ = 1/√N, cos θ = √(N-1)/√N, uniformState = ampState |w⟩ rest θ.

theorem CSD.Empirical.QM.Grover.basisState_weight {n : ℕ} (w : Fin n → Fin 2) : ∑ z ∈ {w}, ‖(QuantumInfo.basisState w).ofLp z‖ ^ 2 = 1

∑ z ∈ {w}, ‖(basisState w) z‖² = 1.

The headline, re-derived from the general theorem

theorem CSD.Empirical.QM.Grover.grover_success {n : ℕ} (hn : 1 ≤ n) (w : Fin n → Fin 2) (k : ℕ) (θ : ℝ) (hsin : Real.sin θ = (√(2 ^ n))⁻¹) (hcos : Real.cos θ = √(2 ^ n - 1) / √(2 ^ n)) : QuantumInfo.prob ((groverStep w)^[k] uniformState) w = Real.sin ((2 * ↑k + 1) * θ) ^ 2

Grover success probability (headline): after k Grover steps from the uniform superposition, the probability of measuring the marked item w is sin²((2k+1)·θ), where θ is the Grover rotation half-angle (sin θ = 1/√N, cos θ = √(N-1)/√N). Re-derived from ampStep_iterate (BHMT) via the operator identity groverStep_eq_ampStep.

theorem CSD.Empirical.QM.Grover.grover_certain {n : ℕ} (hn : 1 ≤ n) (w : Fin n → Fin 2) (k : ℕ) (θ : ℝ) (hsin : Real.sin θ = (√(2 ^ n))⁻¹) (hcos : Real.cos θ = √(2 ^ n - 1) / √(2 ^ n)) (hopt : (2 * ↑k + 1) * θ = Real.pi / 2) : QuantumInfo.prob ((groverStep w)^[k] uniformState) w = 1

Optimal iteration gives certainty: when the accumulated angle hits π/2, i.e. (2k+1)·θ = π/2, the marked item is measured with probability 1. (The general closest-integer bound is amplitude_amplification_succeeds in Mathlib/QuantumInfo/AmplitudeAmplification.lean.)

The k-marked generalisation — free from the general theorem

theorem CSD.Empirical.QM.Grover.uniform_amp_sq {n : ℕ} (z : Fin n → Fin 2) : ‖uniformState.ofLp z‖ ^ 2 = (2 ^ n)⁻¹

Each uniform amplitude has squared norm N⁻¹.

theorem CSD.Empirical.QM.Grover.uniformState_norm {n : ℕ} : ‖uniformState‖ = 1

The uniform state is a unit vector.

theorem CSD.Empirical.QM.Grover.goodProb_uniform {n : ℕ} (G : Finset (Fin n → Fin 2)) : QuantumInfo.goodProb G uniformState = ↑G.card / 2 ^ n

The uniform success probability against a good set of size k is k/N.

theorem CSD.Empirical.QM.Grover.grover_multi_success {n : ℕ} (G : Finset (Fin n → Fin 2)) (hG0 : 0 < G.card) (hG1 : G.card < 2 ^ n) (j : ℕ) : QuantumInfo.goodProb G ((QuantumInfo.ampStep uniformState G)^[j] uniformState) = Real.sin ((2 * ↑j + 1) * Real.arcsin √(↑G.card / 2 ^ n)) ^ 2

★ The k-marked-items Grover distribution. For a good set G of size strictly between 0 and N on the uniform start, j amplification rounds give success probability exactly sin²((2j+1)·arcsin √(|G|/N)) — the generalisation the single-marked development could not state, obtained as a direct instance of amplitude_amplification.