van der Corput second-derivative test in Lean: integer label trick for the run decomposition

To split [0,M) into near-integer and away-from-integer stretches of a monotone sequence D n (first differences), do not build intervals by hand. Use the integer label L n = floor(D n + d) + floor(D n - d) with 2d <= 1. L is monotone. Odd L means D n is within d of an integer. Even L = 2m means D n lies in [m+d, m+1-d). Prove a generic run lemma once: if g : N -> Z is nondecreasing on [0,M) and every constant-label run [a,b) has a sum of norm <= B, then the total is <= B (g(M-1) - g 0 + 1). The proof is strong induction with b := Nat.find (first label change). Within a run, omega recovers both floors from their sum and the bound floor(x-d) <= floor(x+d) <= floor(x-d)+1. On even runs apply Kusmin-Landau to u(a+k) - m(a+k), using exp(int * 2 pi I) = 1. Kusmin-Landau with local hypotheses comes from the global one by extending the increments constantly past M (v n = u 0 + sum_{j<n} D(min j (M-1))). Gotcha: gcongr on x + 1 <= y + 3 splits into x <= y and 1 <= 3, which loses information. Use mul_le_mul_of_nonneg_left instead.