Deterministic Prime Bases for Regev's Algorithm

Regev's quantum factoring algorithm reduces the number of gates per quantum call, but its correctness for the original deterministic prime bases rests on a number-theoretic assumption. We prove that the first ⌈√n⌉ primes work unconditionally for almost all n-bit composite inputs, including almost all composite inputs surviving trial division by those primes. The algorithm retains Regev's original asymptotic gate count per quantum call. A separate theorem covers balanced RSA moduli under three explicit sampling laws. The exceptional input proportion is Θ(2^{-⌈√n⌉}); a population of this order admits no useful relation at any length. On each remaining input, Regev's algorithm finds a nontrivial divisor with constant probability using ⌈√n⌉+4 quantum calls of O(n^{3/2} log n) gates each. The main geometric lemma extracts a useful relation from an earlier successive minimum, determined by the dimension of a quotient of the relation lattice. Prime-divisor counting then gives useful-relation lengths 2^{(3/2+o(1))√n} for general inputs and 2^{(9/2+o(1))√n} for RSA. Both main theorems and finite RSA useful-vector bounds are formally verified in Lean 4; the formalization is archived at https://doi.org/10.5281/zenodo.23407163.