Prove2Me

Algebraic proof: probability of observing ω\omega after rr iterations is sin⁡2((2r+1)t)\sin^2((2r+1)t)

Proved
GroverWiki.groverMatrix_success_amplitude

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

grover-algorithmquantum-computingquantum-search

Let N≥1N \ge 1, t=arcsin⁡(1/N)t = \arcsin(1/\sqrt N), and let A=[12/N−2/N1−4/N]A = \begin{bmatrix}1 & 2/\sqrt N\\ -2/\sqrt N & 1-4/N\end{bmatrix} be the matrix of UsUωU_sU_\omega in the spanning set {∣ω⟩,∣s⟩}\{|\omega\rangle, |s\rangle\}. Since ⟨ω∣ω⟩=1\langle\omega|\omega\rangle = 1 and ⟨ω∣s⟩=1/N\langle\omega|s\rangle = 1/\sqrt N, for every r∈Nr \in \mathbb N

∣[⟨ω∣ω⟩⟨ω∣s⟩]Ar[01]∣2=∣[11N]Ar[01]∣2=sin⁡2((2r+1)t).\left|\begin{bmatrix}\langle\omega|\omega\rangle & \langle\omega|s\rangle\end{bmatrix} A^r \begin{bmatrix}0\\ 1\end{bmatrix}\right|^2 = \left|\begin{bmatrix}1 & \tfrac{1}{\sqrt N}\end{bmatrix} A^r \begin{bmatrix}0\\ 1\end{bmatrix}\right|^2 = \sin^2\bigl((2r+1)t\bigr).

The left-hand side is the probability of observing ω\omega after rr iterations, computed in coordinates; this recovers the formula of the geometric proof, since (2r+1)t=(r+12)θ(2r+1)t = (r+\frac12)\theta.

Preamble
import Mathlib
import Definitions.Def_GroverWiki_Defs

open Matrix
Formal statement
namespace GroverWiki

/-- Algebraic proof: the probability of observing `ω` after `r` iterations, computed from the
`2 × 2` matrix of `U_s U_ω` in the basis `{|ω⟩, |s⟩}`:
`|[⟨ω|ω⟩ ⟨ω|s⟩] (U_s U_ω)^r [0, 1]ᵀ|² = sin²((2r+1)t)` with `t = arcsin(1/√N)`. -/
theorem groverMatrix_success_amplitude {N : ℕ} (hN : 1 ≤ N) (r : ℕ) :
    ‖![(1 : ℂ), 1 / (Real.sqrt N : ℂ)] ⬝ᵥ
        ((!![1, 2 / (Real.sqrt N : ℂ); -2 / (Real.sqrt N : ℂ), 1 - 4 / (N : ℂ)] ^ r) *ᵥ
          ![0, 1])‖ ^ 2 =
      Real.sin ((2 * r + 1) * Real.arcsin (1 / Real.sqrt N)) ^ 2 := 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 "Algebraic proof" (PDF p. 6)
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