Order finding (exact, dyadic period r ∣ 2^t)

Order finding is the quantum core of Shor's factoring algorithm. This module formalizes the exact regime where the period divides the register size, r ∣ 2^t. In that regime the eigenphase s/r is dyadic, quantum phase estimation returns the basis index j = s * (2^t / r) exactly, and a classical gcd recovers the order.

Classical order recovery

theorem QuantumAlg.OrderFinding.main_recovery {t s r : ℕ} (hr : 0 < r) (hrt : r ∣ 2 ^ t) (hsr : s.Coprime r) : 2 ^ t / (s * (2 ^ t / r)).gcd (2 ^ t) = r

Exact order recovery from the dyadic phase-estimation output.

Exact order finding via phase estimation

theorem QuantumAlg.OrderFinding.main_exact_dyadic {t s r : ℕ} (hr : 0 < r) (hrt : r ∣ 2 ^ t) (hsr : s.Coprime r) (j : Fin (2 ^ t)) (hj : ↑j = s * (2 ^ t / r)) : (invQFT t).applyVec (phaseState t (↑s / ↑r)) = (PureState.ket j).vec ∧ 2 ^ t / (↑j).gcd (2 ^ t) = r

Exact order finding through the decoupled QPE interface. The inverse-QFT readout is stated at the raw-vector layer because the phase superposition is a linear combination before it is packaged as a PureState.

def QuantumAlg.OrderFinding.orderFindingExactResourceProfile (t : ℕ) : ResourceProfile

Trusted decoupled resource profile for exact order finding: one modular- exponentiation oracle call feeding an inverse-QFT/readout layer.

Equations

• QuantumAlg.OrderFinding.orderFindingExactResourceProfile t = { oracleQueries := 1, hadamardGates := t, elementaryGates := t ^ 2, classicalOps := 1 }

theorem QuantumAlg.OrderFinding.orderFindingExactResourceProfile_exact (t : ℕ) : (orderFindingExactResourceProfile t).HasExactCounts 1 t (t ^ 2) 1

structure QuantumAlg.OrderFinding.ModExpOracleAccess (N x t m : ℕ) : Prop

Register assumptions for the modular-exponentiation oracle used in exact order finding. The target register has m qubits, large enough to hold residues modulo N.

• modulus_pos : 0 < N
• register_fits : N ≤ 2 ^ m

def QuantumAlg.OrderFinding.modExpOracleTarget {N x t m : ℕ} (A : ModExpOracleAccess N x t m) (a : Fin (2 ^ t)) (y : Fin (2 ^ m)) : Fin (2 ^ m)

Target-register update for the modular-exponentiation oracle: y ↦ y xor (x^a mod N).

Equations

• QuantumAlg.OrderFinding.modExpOracleTarget A a y = ⟨(↑y).xor (x ^ ↑a % N), ⋯⟩

@[simp]

theorem QuantumAlg.OrderFinding.modExpOracleTarget_val {N x t m : ℕ} (A : ModExpOracleAccess N x t m) (a : Fin (2 ^ t)) (y : Fin (2 ^ m)) : ↑(modExpOracleTarget A a y) = (↑y).xor (x ^ ↑a % N)

def QuantumAlg.OrderFinding.modExpOraclePerm {N x t m : ℕ} (A : ModExpOracleAccess N x t m) : Equiv.Perm (Fin (2 ^ t) × Fin (2 ^ m))

The basis permutation underlying the modular-exponentiation oracle.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumAlg.OrderFinding.modExpOraclePerm_apply {N x t m : ℕ} (A : ModExpOracleAccess N x t m) (p : Fin (2 ^ t) × Fin (2 ^ m)) : (modExpOraclePerm A) p = (p.1, modExpOracleTarget A p.1 p.2)

@[simp]

theorem QuantumAlg.OrderFinding.modExpOraclePerm_symm {N x t m : ℕ} (A : ModExpOracleAccess N x t m) : Equiv.symm (modExpOraclePerm A) = modExpOraclePerm A

def QuantumAlg.OrderFinding.modExpOracle {N x t m : ℕ} (A : ModExpOracleAccess N x t m) : Gate (t + m)

The modular-exponentiation oracle gate in the public access model: U_x |a,y> = |a, y xor (x^a mod N)>.

Equations

• QuantumAlg.OrderFinding.modExpOracle A = QuantumAlg.Gate.ofPerm (QuantumAlg.prodEquiv.permCongr (QuantumAlg.OrderFinding.modExpOraclePerm A))

theorem QuantumAlg.OrderFinding.modExpOracle_mem_unitaryGroup {N x t m : ℕ} (A : ModExpOracleAccess N x t m) : (modExpOracle A).op ∈ Matrix.unitaryGroup (Fin (2 ^ (t + m))) ℂ

theorem QuantumAlg.OrderFinding.modExpOracle_apply_ket {N x t m : ℕ} (A : ModExpOracleAccess N x t m) (a : Fin (2 ^ t)) (y : Fin (2 ^ m)) : (modExpOracle A).apply (PureState.ket (prodEquiv (a, y))) = PureState.ket (prodEquiv (a, modExpOracleTarget A a y))

Basis action of the modular-exponentiation oracle.

theorem QuantumAlg.OrderFinding.main_exact_dyadic_with_resources {t s r : ℕ} (hr : 0 < r) (hrt : r ∣ 2 ^ t) (hsr : s.Coprime r) (j : Fin (2 ^ t)) (hj : ↑j = s * (2 ^ t / r)) : ((invQFT t).applyVec (phaseState t (↑s / ↑r)) = (PureState.ket j).vec ∧ 2 ^ t / (↑j).gcd (2 ^ t) = r) ∧ (orderFindingExactResourceProfile t).HasExactCounts 1 t (t ^ 2) 1

Exact order finding paired with the decoupled resource profile.

structure QuantumAlg.OrderFinding.Input (N x r : ℕ) : Prop

Source-level number-theoretic assumptions for exact order finding: N ≥ 2, x is coprime to N, and r is the least positive exponent with x^r ≡ 1 (mod N).

• modulus_ge_two : 2 ≤ N
• coprime : x.Coprime N
• order_pos : 0 < r
• order_eq_one : x ^ r % N = 1
• minimal (m : ℕ) : 0 < m → x ^ m % N = 1 → r ≤ m

theorem QuantumAlg.OrderFinding.main_output_with_resources {N x t r s : ℕ} (hinput : Input N x r) (hrt : r ∣ 2 ^ t) (hs : s < r) : ∃ (j : Fin (2 ^ t)), ↑j = s * (2 ^ t / r) ∧ (orderFindingExactResourceProfile t).HasExactCounts 1 t (t ^ 2) 1

Exact order-finding output index paired with the public one-query resource claim. If q = 2^t is a multiple of the order r, then every s ∈ {0, ..., r-1} gives a valid phase-register output index j = s(q/r). The modular-exponentiation oracle body is treated as one oracle call in this resource profile.

theorem QuantumAlg.OrderFinding.main {N x t m r s : ℕ} (hinput : Input N x r) (A : ModExpOracleAccess N x t m) (hrt : r ∣ 2 ^ t) (hs : s < r) : ((modExpOracle A).op ∈ Matrix.unitaryGroup (Fin (2 ^ (t + m))) ℂ ∧ ∀ (a : Fin (2 ^ t)) (y : Fin (2 ^ m)), (modExpOracle A).apply (PureState.ket (prodEquiv (a, y))) = PureState.ket (prodEquiv (a, modExpOracleTarget A a y))) ∧ ∃ (j : Fin (2 ^ t)), ↑j = s * (2 ^ t / r) ∧ (orderFindingExactResourceProfile t).HasExactCounts 1 t (t ^ 2) 1

Integrated exact order-finding access theorem: the modular-exponentiation oracle is a unitary gate with the public basis action, and the exact divisible case has a phase-register output index with the trusted one-query resource profile.

Classical factoring reduction (gcd step)

theorem QuantumAlg.OrderFinding.main_factor_reduction {N a b : ℕ} (hN : 1 < N) (hdvd : N ∣ a * b) (ha : ¬N ∣ a) (hb : ¬N ∣ b) : 1 < a.gcd N ∧ a.gcd N < N

Factoring-reduction gcd step. If N ∣ a * b while N divides neither a nor b, then gcd(a, N) is a nontrivial factor of N.