Prove2Me

Jordan form of the Grover matrix: UsUω=M diag(e2it,e−2it) M−1U_sU_\omega = M\,\mathrm{diag}(e^{2it}, e^{-2it})\,M^{-1}

Proved
GroverWiki.groverMatrix_jordan_form

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

grover-algorithmquantum-computingquantum-search

Let N≥2N \ge 2, t=arcsin⁡(1/N)t = \arcsin(1/\sqrt N), and let

A=[12/N−2/N1−4/N],M=[−iieite−it]A = \begin{bmatrix}1 & 2/\sqrt N\\ -2/\sqrt N & 1-4/N\end{bmatrix}, \qquad M = \begin{bmatrix}-i & i\\ e^{it} & e^{-it}\end{bmatrix}

be the matrix of UsUωU_sU_\omega in the spanning set {∣ω⟩,∣s⟩}\{|\omega\rangle, |s\rangle\} and the change-of-basis matrix. Then MM is invertible and

  1. A=M[e2it00e−2it]M−1A = M\begin{bmatrix}e^{2it} & 0\\ 0 & e^{-2it}\end{bmatrix}M^{-1};
  2. for every r∈Nr \in \mathbb N, Ar=M[e2rit00e−2rit]M−1A^r = M\begin{bmatrix}e^{2rit} & 0\\ 0 & e^{-2rit}\end{bmatrix}M^{-1}.

The diagonal form gives a closed formula for the state after any number of Grover iterations.

Formalization Note M⁻¹ is Mathlib's matrix inverse, which is the zero matrix for a singular matrix; for N≥2N \ge 2 one has t<π/2t < \pi/2, so det⁡M=−2icos⁡t≠0\det M = -2i\cos t \ne 0. The hypothesis N≥2N \ge 2 excludes N=1N = 1, where MM is singular.

Preamble
import Mathlib
import Definitions.Def_GroverWiki_Defs

open Matrix
Formal statement
namespace GroverWiki

/-- Algebraic proof: Jordan form of the matrix of `U_s U_ω` in the basis `{|ω⟩, |s⟩}`, and of its
`r`-th power. With `t = arcsin(1/√N)` and `M = [[-i, i], [e^{it}, e^{-it}]]`,
`U_s U_ω = M diag(e^{2it}, e^{-2it}) M⁻¹` and `(U_s U_ω)^r = M diag(e^{2rit}, e^{-2rit}) M⁻¹`. -/
theorem groverMatrix_jordan_form {N : ℕ} (hN : 2 ≤ N) :
    let t : ℝ := Real.arcsin (1 / Real.sqrt N)
    let A : Matrix (Fin 2) (Fin 2) ℂ :=
      !![1, 2 / (Real.sqrt N : ℂ); -2 / (Real.sqrt N : ℂ), 1 - 4 / (N : ℂ)]
    let M : Matrix (Fin 2) (Fin 2) ℂ :=
      !![-Complex.I, Complex.I; Complex.exp (t * Complex.I), Complex.exp (-(t * Complex.I))]
    A = M * !![Complex.exp (2 * t * Complex.I), 0; 0, Complex.exp (-(2 * t * Complex.I))] * M⁻¹ ∧
      ∀ r : ℕ, A ^ r =
        M * !![Complex.exp (2 * r * t * Complex.I), 0;
              0, Complex.exp (-(2 * r * t * Complex.I))] * M⁻¹ := 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