Prove2Me

§6, p. 1504 — each good cc is observed with probability at least (p−1)/(20q2)≥1/(40q)(p-1)/(20q^2)\ge 1/(40q)

Proved
ShorAlgorithms.DiscreteLog.good_c_prob_ge

by mikedeng1 · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-logarithmp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-algorithms

Throughout, pp is a prime, gg is a generator of the multiplicative group (Z/pZ)×(\mathbb Z/p\mathbb Z)^\times (an element of order p−1p-1), rr is an integer with 0≤r<p−10\le r<p-1 and x=grx=g^r (so rr is the discrete logarithm of xx), and q=2lq=2^l is a power of 22 with p<q<2pp<q<2p.

Call 0≤c<q0\le c<q good if (c,d)(c,d) satisfies (6.10) and (6.11) for some 0≤d<q0\le d<q. Then, when the final state (6.3) is measured, the first register shows a good cc with probability at least (p−1)/(20q2)(p-1)/(20q^2), and this is at least 1/(40q)1/(40q):

∑d=0q−1 ∑y∈(Z/p)×Pr⁡[c,d,y] ≥ p−120q2 ≥ 140q.\sum_{d=0}^{q-1}\ \sum_{y\in(\mathbb Z/p)^\times}\Pr[c,d,y]\ \ge\ \frac{p-1}{20q^2}\ \ge\ \frac{1}{40q}.

This is the form of the success probability used when recovering rr from several good values cc.

Preamble
import Mathlib
import Definitions.Def_ShorAlgorithms_DiscreteLog_outcomeProb
import Definitions.Def_ShorAlgorithms_DiscreteLog_IsGood
Formal statement
namespace ShorAlgorithms.DiscreteLog

/-- Shor (1997), §6, p. 1504 ("Note that each good `c`"): under the hypotheses of §6, a value
`c` that forms a good pair `(c, d)` with some `d` is observed in the first register with
probability (summed over all `d` and `y`) at least `(p - 1)/(20 q²)`, and `(p - 1)/(20 q²) ≥ 1/(40 q)`. -/
theorem good_c_prob_ge (p : ℕ) [hp : Fact p.Prime] (g : (ZMod p)ˣ) (hg : orderOf g = p - 1)
    (r : ℕ) (hr : r < p - 1) (q l : ℕ) (hq : q = 2 ^ l) (hpq : p < q) (hqp : q < 2 * p)
    (c : Fin q) (hc : ∃ d : Fin q, IsGood p q r c d) :
    ((p : ℝ) - 1) / (20 * (q : ℝ) ^ 2) ≤
        ∑ d : Fin q, ∑ y : (ZMod p)ˣ, outcomeProb p g (g ^ r) q c d y ∧
      1 / (40 * (q : ℝ)) ≤ ((p : ℝ) - 1) / (20 * (q : ℝ) ^ 2) := by sorry

end ShorAlgorithms.DiscreteLog
Source
Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5) (1997), p. 1504, §6 ("Note that each good cc has a probability of at least …")
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph