A small r with o_r(n) > log^2 n (Lemma 4.3)
ProvedAKS.r_existsLemma 4.3 of the paper: for n > 1 there exists an r, bounded by the fifth power of the logarithm of n, such that the multiplicative order of n modulo r exceeds the square of the logarithm of n. The proof is a counting argument: every r whose order of n is at most log^2 n, and every r dividing n, divides the single product of n with the numbers n^i - 1 for i up to log^2 n, a product below the power 2^(log^5 n); the lcm of the first log^5 n numbers is at least 2^(log^5 n) by Lemma 3.1, so some r in the window escapes the bad list.
Formalization Note The statement uses the generous integer encoding logUp n = floor(log2 n) + 1, strictly greater than log2 n, in place of the paper's real-valued logarithm, both in the threshold and in the bound: r exists with 1 < r at most max 3 (logUp n)^5 and ordR r n greater than (logUp n)^2. The generosity is one-sided in the safe direction: the algorithm's search for r happens inside exactly this window, and the larger threshold only strengthens the group bound that the correctness proof needs.
import Mathlib import Definitions.Def_AKS_poly import Definitions.Def_AKS_alg
namespace AKS
/-! Lemma 4.3 of the paper: a small r with o_r(n) > log^2 n. -/
theorem r_exists (n : ℕ) (hn : 1 < n) :
∃ r, 1 < r ∧ r ≤ max 3 ((logUp n) ^ 5) ∧ (logUp n) ^ 2 < ordR r n := by sorry
end AKS
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every n > 1 there is an r with 1 < r, r at most max 3 (logUp n)^5, and (logUp n)^2 < ordR r n, where logUp n = Nat.log2 n + 1 and ordR r n is the multiplicative order of n modulo r, taken as 0 when n and r are not coprime. No other hypotheses appear.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.