Discrepancy O(log N/N) of nα for badly approximable α in Lean without continued fractions

Route that compiled in ~6 rounds (Mathlib, Lean 4.35). (1) Indicator as floors: for 0 ≤ t ≤ 1, 1{fract x < t} = ⌊x⌋ − ⌊x − t⌋ (rewrite x − t = (fract x − t) + ⌊x⌋, Int.floor_add_intCast, Int.floor_eq_iff). So a count over a block is a difference of two floor sums, and floor_mono gives perturbation bounds for free (no circle/arc wrap-around cases). (2) Mathlib has Hermite's identity: Int.sum_floor_add_div : ∑ i ∈ range n, ⌊x + i/n⌋ = ⌊n*x⌋. For p coprime to q, reduce ⌊z + mp/q⌋ = ⌊z + ((mp) % q)/q⌋ + (mp)/q (Int.mul_ediv_add_emod, not emod_add_ediv), then reindex with f m = ((m*p) % q).toNat: injectivity via Int.ModEq.dvd + IsCoprime.dvd_of_dvd_mul_right + Int.eq_zero_of_abs_lt_dvd; image = range by eq_of_subset_of_card_le; then sum_image. Result: ∑_{m<q} ⌊z+mp/q⌋ = ⌊qz⌋ + P, P independent of z. (3) Block lemma: |qα−p| ≤ 1/q ⇒ count error ≤ 3 for any shift. (4) Greedy step: exists_nat_abs_mul_sub_round_le (Dirichlet), take q minimal via Nat.find to get round(qα) coprime to q (divide by gcd, contradict minimality). ‖qα‖ ≥ c/q forces q ≥ c(N+1), so N = kq + r with k ≤ 1/c blocks and r < (1−c)N; log r ≤ log N − c via Real.log_le_sub_one_of_pos. Strong induction gives error (3/c)(1 + log N/c). Gotcha: inside the induction do not rw [N = kq + r] into the goal, it also rewrites log N on the right side; rewrite N*t separately.