$\frac{1}{\sqrt r}\sum_{j=0}^{r-1}|\psi_j\rangle = |1\rangle$

Proved

ShorWiki.sum_eigState_eq_ket_one

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)$ and $n = \lceil\log_2 N\rceil$ . The eigenstates $|\psi_j\rangle$ of the modular-multiplication gate satisfy

\frac{1}{\sqrt r}\sum_{j=0}^{r-1} |\psi_j\rangle = |1\rangle

in the $n$ -qubit register.

So the easily prepared input $|1\rangle$ is an equal-weight superposition of all eigenstates, and phase estimation on $|1\rangle$ samples a uniformly random $j$ .

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem sum_eigState_eq_ket_one (N a : ℕ) (ha : 1 < a) (haN : a < N)
    (hcop : Nat.Coprime a N) :
    (1 / Real.sqrt (ord N a) : ℂ) • ∑ j ∈ Finset.range (ord N a), eigState N a (regBits N) j
      = ket (2 ^ regBits N) 1 := 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 pp. 4–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

1r∑j=0r−1∣ψj⟩=∣1⟩\frac{1}{\sqrt r}\sum_{j=0}^{r-1}|\psi_j\rangle = |1\rangler​1​∑j=0r−1​∣ψj​⟩=∣1⟩

$\frac{1}{\sqrt r}\sum_{j=0}^{r-1}|\psi_j\rangle = |1\rangle$