Discrete logarithm as a hidden subgroup problem: $f(a,b) = g^a x^{-b}$ is a homomorphism with kernel the multiples of $(r,1)$

Proved

ShorWiki.discreteLog_hiddenSubgroup

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

quantum-computingshor-algorithm

Let $G$ be a finite group of order $p$ generated by $g$ , let $r$ be an integer, and let $x = g^r$ . Define

f : \mathbb Z_p \times \mathbb Z_p \to G, \qquad f(a, b) = g^a x^{-b}.

Then

$f$ is a group homomorphism: $f(a + a', b + b') = f(a,b)\,f(a',b')$ for all $a, b, a', b' \in \mathbb Z_p$ ;
the kernel of $f$ consists exactly of the multiples of $(r, 1)$ : $f(a,b) = 1$ if and only if $(a,b) = t\,(r,1)$ for some $t \in \mathbb Z_p$ .

Hence finding the hidden subgroup $\ker f$ determines the discrete logarithm $r = \log_g x$ modulo $p$ .

Formalization Note Elements of $\mathbb Z_p$ are ZMod p with $p$ the cardinality of $G$ , and $g^a$ means $g$ raised to the least nonnegative representative of $a$ . The group is not assumed commutative; it is cyclic because $g$ generates it.

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem discreteLog_hiddenSubgroup {G : Type*} [Group G] [Fintype G] (g : G)
    (hg : ∀ h : G, h ∈ Subgroup.zpowers g) (r : ℕ) :
    (∀ a b a' b' : ZMod (Fintype.card G),
        g ^ (a + a').val * ((g ^ r) ^ (b + b').val)⁻¹
          = (g ^ a.val * ((g ^ r) ^ b.val)⁻¹) * (g ^ a'.val * ((g ^ r) ^ b'.val)⁻¹)) ∧
    ∀ a b : ZMod (Fintype.card G),
      g ^ a.val * ((g ^ r) ^ b.val)⁻¹ = 1 ↔
        ∃ t : ZMod (Fintype.card G), a = t * (r : ZMod (Fintype.card G)) ∧ b = t := 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 "Shor's algorithm for discrete logarithms" (PDF p. 7)

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

Discrete logarithm as a hidden subgroup problem: f(a,b)=gax−bf(a,b) = g^a x^{-b}f(a,b)=gax−b is a homomorphism with kernel the multiples of (r,1)(r,1)(r,1)

Discrete logarithm as a hidden subgroup problem: $f(a,b) = g^a x^{-b}$ is a homomorphism with kernel the multiples of $(r,1)$