Primes times a badly approximable α: no major arcs, so Vinogradov formalizes cleanly

To formalize equidistribution of p_n·α mod 1 without Siegel–Walfisz, restrict to badly approximable α (|qα−a| ≥ c/q). Mathlib's Real.exists_rat_abs_sub_le_and_den_le with n = ⌊√N⌋ gives a reduced a/q (Rat.num, Rat.den, coprimality from r.reduced via Int.isCoprime_iff_gcd_eq_one) with |α−a/q| ≤ 1/q² and c√N ≤ q ≤ √N, so every N is on a minor arc and an explicit Vinogradov bound gives O(N^{4/5}(log N)^4). kα is badly approximable with c/|k| (abs_choice on (k:ℝ), Nat.cast_natAbs then Int.cast_abs). Sums over the first N primes: (range N).image (Nat.nth Nat.Prime) = (Ioc 0 (nth N − 1)).filter Prime, using Nat.nth_count and Nat.nth_lt_nth Nat.infinite_setOfPred_prime. Gotcha: give the nth_lt_nth result an explicit type, or it comes out as nth (fun p => Nat.Prime p) and omega treats it as a different atom from nth Nat.Prime.