The initial ket is close to $|s'\rangle$ : $\langle s'|s\rangle = \sqrt{(N-1)/N}$

Proved

GroverWiki.perpState_inner_uniformState

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

grover-algorithmquantum-computingquantum-search

Let $N \ge 2$ , let $\omega \in \{0,\dots,N-1\}$ , let $|s\rangle = \frac{1}{\sqrt N}\sum_x|x\rangle$ and $|s'\rangle = \frac{1}{\sqrt{N-1}}\sum_{x\ne\omega}|x\rangle$ . Then

\langle s'|s\rangle = \sqrt{\frac{N-1}{N}} .

Equivalently, the angle $\theta/2$ between $|s\rangle$ and $|s'\rangle$ satisfies $\cos\frac\theta2 = \sqrt{(N-1)/N}$ , i.e. $\sin\frac\theta2 = \frac{1}{\sqrt N}$ : the initial state is close to the state orthogonal to $|\omega\rangle$ .

Preamble

import Mathlib
import Definitions.Def_GroverWiki_Defs

open Matrix

Formal statement

namespace GroverWiki

/-- The initial ket is close to `|s'⟩`: `⟨s'|s⟩ = √((N-1)/N)`. -/
theorem perpState_inner_uniformState {N : ℕ} (hN : 2 ≤ N) (ω : Fin N) :
    star (perpState ω) ⬝ᵥ uniformState N = (Real.sqrt (((N : ℝ) - 1) / N) : ℂ) := 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

The initial ket is close to ∣s′⟩|s'\rangle∣s′⟩: ⟨s′∣s⟩=(N−1)/N\langle s'|s\rangle = \sqrt{(N-1)/N}⟨s′∣s⟩=(N−1)/N​

The initial ket is close to $|s'\rangle$ : $\langle s'|s\rangle = \sqrt{(N-1)/N}$