$|\psi_j\rangle$ is an eigenvector of $U$ with eigenvalue $\omega_r^j$

Proved

ShorWiki.mulModGate_mulVec_eigState

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

quantum-computingshor-algorithm

Let $1 < a < N$ with $\gcd(a,N)=1$ , $r = \operatorname{ord}_N(a)$ , $n = \lceil\log_2 N\rceil$ , and let $U$ be the modular-multiplication gate. For every integer $j \ge 0$ the state

|\psi_j\rangle = \frac{1}{\sqrt r}\sum_{k=0}^{r-1} \omega_r^{-kj}\,|a^k \bmod N\rangle

is nonzero and satisfies

U|\psi_j\rangle = \omega_r^{j}\,|\psi_j\rangle .

These are the eigenstates to which phase estimation is applied; the eigenvalue $\omega_r^j = e^{2\pi i j/r}$ carries the phase $j/r$ .

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem mulModGate_mulVec_eigState (N a : ℕ) (ha : 1 < a) (haN : a < N)
    (hcop : Nat.Coprime a N) (j : ℕ) :
    eigState N a (regBits N) j ≠ 0 ∧
      mulModGate N a (regBits N) *ᵥ eigState N a (regBits N) j
        = omega (ord N a) ^ j • eigState N a (regBits N) j := by sorry

end ShorWiki

Source

Wikipedia, "Shor's algorithm", revision oldid=1378862216, https://en.wikipedia.org/w/index.php?title=Shor%27s_algorithm&oldid=1378862216, section "Quantum phase estimation" (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

∣ψj⟩|\psi_j\rangle∣ψj​⟩ is an eigenvector of UUU with eigenvalue ωrj\omega_r^jωrj​

$|\psi_j\rangle$ is an eigenvector of $U$ with eigenvalue $\omega_r^j$