Prove2Me

Each Grover iteration UsUωU_sU_\omega rotates the plane by θ=2arcsin⁡(1/N)\theta = 2\arcsin(1/\sqrt N)

Proved
GroverWiki.groverIteration_rotation

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

grover-algorithmquantum-computingquantum-search

Let N≥2N \ge 2, let f ⁣:{0,…,N−1}→{0,1}f\colon\{0,\dots,N-1\}\to\{0,1\} have exactly one index ω\omega with f(ω)=1f(\omega) = 1, let ∣s′⟩=1N−1∑x≠ω∣x⟩|s'\rangle = \frac{1}{\sqrt{N-1}}\sum_{x\ne\omega}|x\rangle, and let θ=2arcsin⁡1N\theta = 2\arcsin\frac{1}{\sqrt N}. Then for every angle φ∈R\varphi \in \mathbb R,

UsUω(cos⁡φ ∣s′⟩+sin⁡φ ∣ω⟩)=cos⁡(φ+θ) ∣s′⟩+sin⁡(φ+θ) ∣ω⟩.U_sU_\omega\bigl(\cos\varphi\,|s'\rangle + \sin\varphi\,|\omega\rangle\bigr) = \cos(\varphi+\theta)\,|s'\rangle + \sin(\varphi+\theta)\,|\omega\rangle .

In the orthonormal basis {∣s′⟩,∣ω⟩}\{|s'\rangle, |\omega\rangle\} of the plane, one Grover iteration is the rotation by the angle θ\theta towards ∣ω⟩|\omega\rangle.

Preamble
import Mathlib
import Definitions.Def_GroverWiki_Defs

open Matrix
Formal statement
namespace GroverWiki

/-- The Grover iteration `U_s U_ω` rotates every state `cos φ |s'⟩ + sin φ |ω⟩` of the plane
by the angle `θ = 2 arcsin(1/√N)`. -/
theorem groverIteration_rotation {N : ℕ} (hN : 2 ≤ N) (f : Fin N → Fin 2) (ω : Fin N)
    (hω : ∀ x, f x = 1 ↔ x = ω) (φ : ℝ) :
    groverIteration f *ᵥ
        ((Real.cos φ : ℂ) • perpState ω + (Real.sin φ : ℂ) • ket ω) =
      (Real.cos (φ + 2 * Real.arcsin (1 / Real.sqrt N)) : ℂ) • perpState ω +
        (Real.sin (φ + 2 * Real.arcsin (1 / Real.sqrt N)) : ℂ) • ket ω := by sorry

end GroverWiki
Source
Wikipedia, "Grover's algorithm", revision oldid=1373498442, https://en.wikipedia.org/w/index.php?title=Grover%27s_algorithm&oldid=1373498442, section "Geometric proof" (PDF p. 5)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph