Prove2Me

Us=2∣s⟩⟨s∣−IU_s = 2|s\rangle\langle s| - I is the reflection through ∣s⟩|s\rangle

Proved
GroverWiki.diffusion_reflection

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

grover-algorithmquantum-computingquantum-search

Let ∣s⟩=1N∑x=0N−1∣x⟩|s\rangle = \frac{1}{\sqrt N}\sum_{x=0}^{N-1}|x\rangle and Us=2∣s⟩⟨s∣−IU_s = 2|s\rangle\langle s| - I. Then UsU_s is the reflection through ∣s⟩|s\rangle:

  1. Us∣s⟩=∣s⟩U_s|s\rangle = |s\rangle;
  2. Us∣v⟩=−∣v⟩U_s|v\rangle = -|v\rangle for every ∣v⟩∈CN|v\rangle \in \mathbb C^N with ⟨s∣v⟩=0\langle s|v\rangle = 0.

Together with the oracle's reflection property, this is what keeps the state of Grover's algorithm in a two-dimensional plane.

Preamble
import Mathlib
import Definitions.Def_GroverWiki_Defs

open Matrix
Formal statement
namespace GroverWiki

/-- `U_s = 2|s⟩⟨s| - I` is the reflection through `|s⟩`: it fixes `|s⟩` and negates every
vector orthogonal to `|s⟩`. -/
theorem diffusion_reflection (N : ℕ) :
    diffusion N *ᵥ uniformState N = uniformState N ∧
      ∀ v : Fin N → ℂ, star (uniformState N) ⬝ᵥ v = 0 → diffusion N *ᵥ v = -v := 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. 4)
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