§1 example 1: multiplicative order from a stabilizer

Proved

QAlgorithms.Papers.Independent.Intakethird100.P03.order_reduction

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $q\ge2$ and let $g$ be a unit modulo $q$ . For integer $m$ , set $F_g(m,x)=g^m x$ on $\mathbb Z/q\mathbb Z$ , and let $r=\operatorname{ord}(g)$ . Then

r>0,\qquad \{m\in\mathbb Z:F_g(m,1)=1\}=r\mathbb Z.

Moreover, $F_g(r,1)=1$ , and every positive natural number $s$ with $F_g(s,1)=1$ satisfies $r\le s$ . Thus the positive canonical stabilizer generator is precisely the multiplicative order.

This is the algebraic reduction to a stabilizer, without importing the separately cited randomized factoring reduction.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P03

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate Kronecker

namespace QAlgorithms.Papers.Independent.Intakethird100.P03

open QAlgorithms.Papers.Independent.Renew46.P01 (cleanVector)

attribute [local instance] Classical.propDecidable

/-- PDF p.4, example 1: the stabilizer at one is (orderOf g) Z, whose positive
canonical generator is exactly the multiplicative order. No factoring reduction is added. -/
theorem order_reduction (q : ℕ) (hq : 2 ≤ q) (g : (ZMod q)ˣ) :
    0 < orderOf g ∧
    (∀ m : ℤ, orderAction g m 1 = 1 ↔ ∃ t : ℤ, m = (orderOf g : ℤ) * t) ∧
    orderAction g (orderOf g : ℤ) 1 = 1 ∧
    ∀ r : ℕ, 0 < r → orderAction g (r : ℤ) 1 = 1 → orderOf g ≤ r := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P03

end

Source

Quantum measurements and the Abelian Stabilizer Problem, arXiv:quant-ph/9511026v1, PDF p. 4, §1 example 1: multiplicative order from a stabilizer

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number $q$ satisfying $2\leq q$ and every unit $g\in(\mathbb Z/q\mathbb Z)^\times$ , let $o$ be the group-theoretic order of $g$ . Then $o>0$ ; for every integer $m$ , the ring equality $g^m\cdot1=1$ holds if and only if there exists an integer $t$ with $m=ot$ ; one has $g^o\cdot1=1$ ; and, for every natural number $r$ , if $r>0$ and $g^r\cdot1=1$ , then $o\leq r$ . Integer powers here are taken in the unit group, including inverse powers for negative $m$ , and then interpreted in $\mathbb Z/q\mathbb Z$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph