Every eigenvalue of $U$ is an $r$ -th root of unity $\omega_r^k$

Proved

ShorWiki.mulModGate_eigenvalue_root_of_unity

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 on $n$ qubits. If $\mu \in \mathbb C$ is an eigenvalue of $U$ , then

\mu = \omega_r^k = e^{2\pi i k / r} \quad \text{for some } 0 \le k < r .

The phases that phase estimation can return are therefore exactly the fractions $k/r$ , which is what makes the order $r$ visible in the measurement.

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem mulModGate_eigenvalue_root_of_unity (N a : ℕ) (ha : 1 < a) (haN : a < N)
    (hcop : Nat.Coprime a N) (μ : ℂ)
    (hμ : Module.End.HasEigenvalue (Matrix.toLin' (mulModGate N a (regBits N))) μ) :
    ∃ k < ord N a, μ = omega (ord N a) ^ k := 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

Every eigenvalue of UUU is an rrr-th root of unity ωrk\omega_r^kωrk​

Every eigenvalue of $U$ is an $r$ -th root of unity $\omega_r^k$