A small modulus of large order

The AKS algorithm needs a modulus r of size polynomial in log n such that the multiplicative order of n modulo r exceeds log₂² n. With c = ⌈log₂ n⌉, some r ≤ 4 c⁵ has order above c² (Cslib.AKS.exists_lt_orderOf), so r ≤ 128 log₂⁵ n and the order exceeds log₂² n (Cslib.AKS.exists_lt_orderOf_logb). This is Agrawal, Kayal, Saxena, Lemma 4.3 up to the constant: they prove r ≤ max(3, ⌈log₂⁵ n⌉) using Nair's bound lcm(1, …, m) ≥ 2^m, while this file uses the weaker bound C(2m, m) ≥ 4^m / (2m + 1) for numbers divisible by 1, …, 2m (Cslib.AKS.centralBinom_dvd_of_forall_dvd).

The proof takes the least s not dividing X = n^K ∏_{i = 1}^{c²} (n^i - 1), where K = ⌊log₂ (4c⁵)⌋; it exists since C(4c⁵, 2c⁵) > X. Such an s is coprime to n: a prime p ∣ gcd(s, n) would give s = p^v s' with p^v ∣ n^K and s' < s, so s ∣ X. If the order o of n modulo s were at most c², then s ∣ n^o - 1 ∣ X. The published proof passes from s to s / gcd(s, n); here the factor n^K in X and the minimality of s give coprimality directly.

Main results

• Cslib.AKS.centralBinom_dvd_of_forall_dvd: C(2m, m) divides every number divisible by 1, …, 2m.
• Cslib.AKS.exists_lt_orderOf: some r ≤ 4 ⌈log₂ n⌉⁵ has ord_r(n) > ⌈log₂ n⌉².
• Cslib.AKS.exists_lt_orderOf_logb: some r ≤ 128 log₂⁵ n has ord_r(n) > log₂² n.

References

• M. Agrawal, N. Kayal, N. Saxena, PRIMES is in P

theorem Cslib.AKS.centralBinom_dvd_of_forall_dvd {m X : ℕ} (hX : X ≠ 0) (h : ∀ (s : ℕ), 1 ≤ s → s ≤ 2 * m → s ∣ X) : m.centralBinom ∣ X

The central binomial coefficient divides every common multiple of 1, …, 2m: each prime power p^v exactly dividing C(2m, m) is at most 2m.

theorem Cslib.AKS.exists_lt_orderOf {n : ℕ} (hn : 2 ≤ n) : ∃ (r : ℕ), 2 ≤ r ∧ r ≤ 4 * Nat.clog 2 n ^ 5 ∧ Nat.clog 2 n ^ 2 < orderOf ↑n

A small modulus of large order: for n ≥ 2 and c = ⌈log₂ n⌉, some 2 ≤ r ≤ 4 c⁵ has ord_r(n) > c² Agrawal, Kayal, Saxena, Lemma 4.3, up to the constant.

theorem Cslib.AKS.exists_lt_orderOf_logb {n : ℕ} (hn : 2 ≤ n) : ∃ (r : ℕ), 2 ≤ r ∧ ↑r ≤ 128 * Real.logb 2 ↑n ^ 5 ∧ Real.logb 2 ↑n ^ 2 < ↑(orderOf ↑n)

A small modulus of large order, with logarithms: for n ≥ 2, some 2 ≤ r ≤ 128 log₂⁵ n has ord_r(n) > log₂² n Agrawal, Kayal, Saxena, Lemma 4.3, up to the constant.