Prove2Me

The modular-multiplication gate satisfies Ur=IU^r = I

Proved
ShorWiki.mulModGate_pow_ord

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

quantum-computingshor-algorithm

Let 1<a<N1 < a < N with gcd⁡(a,N)=1\gcd(a,N)=1, let r=ord⁡N(a)r = \operatorname{ord}_N(a) and n=⌈log⁡2N⌉n = \lceil\log_2 N\rceil. The nn-qubit gate

U∣k⟩={∣ak mod N⟩0≤k<N,∣k⟩N≤k<2nU|k\rangle = \begin{cases} |ak \bmod N\rangle & 0 \le k < N,\\ |k\rangle & N \le k < 2^n\end{cases}

satisfies

Ur=I.U^r = I .

This periodicity of the gate is what quantum phase estimation exploits: it determines the spectrum of UU.

Preamble
import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker
Formal statement
namespace ShorWiki

theorem mulModGate_pow_ord (N a : ℕ) (ha : 1 < a) (haN : a < N)
    (hcop : Nat.Coprime a N) :
    mulModGate N a (regBits N) ^ ord N a = 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 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