Motivation

Searching an unsorted list of $N$ items for a single marked entry takes $\Theta(N)$ queries classically — there is no way to do better than checking items one at a time. Grover's algorithm (Grover 1996) shows that a quantum computer solves the same problem in $\Theta(\sqrt N)$ queries, a quadratic speedup that applies to any problem expressible as unstructured search over a black-box oracle (this includes brute-forcing NP-complete problems and inverting one-way functions, which is why post-quantum cryptography doubles key lengths to compensate). Unlike Shor's algorithm, Grover's algorithm is provably optimal: Bennett–Bernstein–Brassard–Vazirani (1997) showed $\Omega(\sqrt N)$ queries are necessary for any quantum algorithm solving unstructured search, so the quadratic speedup is the best any quantum algorithm can achieve on this problem.

Setting

Model an $N$-item database as the standard basis of $E = \mathbb{C}^N$ (EuclideanSpace ℂ (Fin N)), with inner product $\langle x,y\rangle = \sum_i \overline{x_i}\,y_i$. Fix a marked index $w_0 \in \{0,\dots,N-1\}$. The algorithm starts in the uniform superposition

$$|s\rangle = \frac{1}{\sqrt N}\sum_{i} |i\rangle,$$

a unit vector assigning equal amplitude to every item. Two reflections drive the search:

• the oracle $O = I - 2|w_0\rangle\langle w_0|$, which flips the sign of the amplitude on the marked item and leaves every other basis state fixed;
• the diffusion operator $D = 2|s\rangle\langle s| - I$ ("inversion about the mean"), the reflection about $|s\rangle$.

One Grover iterate is $G = D\,O$. The algorithm applies $G$ some number of times to $|s\rangle$ and measures; a measurement outcome equal to $w_0$ counts as success.

Formalization targets

Milestone — the iterate is an isometry

$$\|G x\| = \|x\| \quad \text{for every } x \in E$$

$O$ and $D$ are each reflections about a unit vector, hence isometries; their composition $G$ is therefore norm-preserving on the whole space, not just at $|s\rangle$ — the minimal fact needed for $G$ to be a legitimate quantum operation.

Milestone — the rotation formula

$$\langle w_0, G^k s\rangle = \sin\bigl((2k+1)\theta\bigr), \qquad \theta := \arcsin\!\left(\tfrac{1}{\sqrt N}\right)$$

The geometric heart of the algorithm (Nielsen & Chuang, Quantum Computation and Quantum Information, Section 6.1.2): restricted to the real two-dimensional subspace spanned by $|w_0\rangle$ and the component of $|s\rangle$ orthogonal to it, $G$ acts as rotation by a fixed angle $2\theta$. Each iterate therefore advances the amplitude on the marked state along $\sin((2k+1)\theta)$, exactly as claimed, with $\theta = \arcsin(1/\sqrt N)$ the rotation's initial offset (since $\langle w_0, s\rangle = 1/\sqrt N$ at $k=0$).

Goal

$$\exists\, k,\quad 1 - \tfrac1N \;\le\; \bigl|\langle w_0, G^k s\rangle\bigr|^2$$

Some number of iterations drives the probability of measuring the marked item above $1-1/N$. The goal is stated existentially, without fixing $k$ to a specific rounded formula: the rotation angle $(2k+1)\theta$ can be made to land within $\theta$ of $\pi/2$ by an appropriate integer $k$, and at that point $\sin^2((2k+1)\theta) \ge \cos^2\theta = 1-\sin^2\theta = 1 - 1/N$. Pinning $k$ down to an explicit closed form (e.g. the nearest integer to $\pi/(4\theta) - 1/2$) is one valid strategy, but is not required by the statement — any correct choice of $k$, and any correct proof it works, closes the goal.

Significance

Grover's algorithm is the second landmark quantum algorithm after Shor's, and the one with the widest applicability: because it treats the search space as a black box, it accelerates any brute-force search — SAT solving, collision finding, and generic key search among them — which is the concrete reason NIST's post-quantum cryptography standards double symmetric key lengths rather than replacing them outright. The mathematics itself has been fully settled since 1996, including matching optimality lower bounds; nothing here is open. What this mission adds is a machine- checked derivation of the amplitude formula and success bound directly from the definitions of the oracle and diffusion operators as concrete linear operators on EuclideanSpace ℂ (Fin N) — Mathlib has the finite-dimensional inner product space and rank-one operator machinery this needs (InnerProductSpace.rankOne, EuclideanSpace.single), but no existing formalization of the algorithm itself.

Difficulty

The obvious first attempt tries to track the full $N$-dimensional state vector through $k$ iterations. This is intractable in general: $G$'s action on an arbitrary basis vector depends on its overlap with both $|w_0\rangle$ and $|s\rangle$. The move that makes the problem tractable is recognizing that $G$ preserves the two-dimensional real subspace $\mathrm{span}\{|w_0\rangle, |s\rangle\}$ — everything orthogonal to this plane is fixed by both $O$ and $D$, and inside the plane $G$ is exactly a rotation matrix by angle $2\theta$. Establishing this invariance and then tracking only the rotation angle (rather than the full vector) is the standard reduction, and the one this mission's milestones are built around; skipping it and attempting a direct $N$-dimensional induction does not scale.

Formalization scope

Works over a general $N:\mathbb N$ together with a marked index $w_0 : \mathrm{Fin}\,N$ — no assumption that $N$ is a power of two, since the rotation argument is agnostic to how the $N$ basis states are physically encoded into qubits (that encoding is a separate, unrelated concern from the search dynamics proved here). Supplying w0 : Fin N already forces $N \ge 1$; no separate nonemptiness hypothesis is added. The oracle and diffusion operators are built directly from Mathlib's InnerProductSpace.rankOne rather than an ad-hoc pointwise definition, so their reflection structure (and hence unitarity) is visible from the definition itself. A trivializing formalization is ruled out explicitly: the goal is stated as an existential over $k$ rather than a fixed closed-form iteration count, so a correct proof must still exhibit a genuine successful $k$ and establish the bound — it cannot be discharged by an unrelated or degenerate choice. Contributions extending this to multiple marked items, or proving the matching $\Omega(\sqrt N)$ lower bound (Bennett–Bernstein–Brassard–Vazirani 1997), are welcome as follow-up missions.

Selected references

• L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. https://arxiv.org/abs/quant-ph/9605043
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Section 6.1.
• C. H. Bennett, E. Bernstein, G. Brassard, and U. Vazirani, Strengths and Weaknesses of Quantum Computing, SIAM J. Comput. 26 (1997). https://arxiv.org/abs/quant-ph/9701001