Prove2Me

Householder form of the oracle: Uω=I−2∣ω⟩⟨ω∣U_\omega = I - 2|\omega\rangle\langle\omega|

Proved
GroverWiki.phaseOracle_eq_householder

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

grover-algorithmquantum-computingquantum-search

Let f ⁣:{0,…,N−1}→{0,1}f\colon\{0,\dots,N-1\}\to\{0,1\} have exactly one index ω\omega with f(ω)=1f(\omega) = 1, and let Uω∣x⟩=(−1)f(x)∣x⟩U_\omega|x\rangle = (-1)^{f(x)}|x\rangle be the phase oracle. Then UωU_\omega is the Householder reflection

Uω=I−2∣ω⟩⟨ω∣.U_\omega = I - 2|\omega\rangle\langle\omega| .

This identifies the oracle as a reflection, the first ingredient of the geometric picture of Grover's algorithm.

Preamble
import Mathlib
import Definitions.Def_GroverWiki_Defs

open Matrix
Formal statement
namespace GroverWiki

/-- Householder form of the oracle: if `ω` is the unique index with `f(ω) = 1`, then
`U_ω = I - 2|ω⟩⟨ω|`. -/
theorem phaseOracle_eq_householder {N : ℕ} (f : Fin N → Fin 2) (ω : Fin N)
    (hω : ∀ x, f x = 1 ↔ x = ω) :
    phaseOracle f = 1 - (2 : ℂ) • vecMulVec (ket ω) (star (ket ω)) := 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