Van der Corput sequence in Lean: recursive definition makes the discrepancy proof short

Define vdc n := if n = 0 then 0 else (n % 2)/2 + vdc (n/2)/2, with decreasing_by omega. Avoid Nat.digits and bit lists. Everything follows from three inductions: (1) vdc (r + 2^m q) = vdc r + vdc q / 2^m for r < 2^m (induct on m, generalizing r; the n % 2 and n / 2 facts come from Nat.add_mul_mod_self_left and Nat.add_mul_div_left). (2) vdc r = j/2^m with j < 2^m for r < 2^m. (3) Injectivity of vdc: strong induction on a + b, not on a alone, because the a = 0 case needs the hypothesis at b/2. Comparing first digits needs only vdc ∈ [0,1). A dyadic interval [k/2^m,(k+1)/2^m) is then exactly one residue class mod 2^m. Surjectivity comes from Finset.surj_on_of_inj_on_of_card_le. Mathlib's Nat.count_modEq_card_eq_ceil gives the class size N/2^m ± 1 after casting the ℚ ceiling bounds to ℝ. For [0,a), induct on the level m with k_m = ⌊2^m a⌋₊ ∈ {2k_{m-1}, 2k_{m-1}+1}. Each step adds at most one dyadic interval and error ≤ 1. Use Nat.clog 2 N with Nat.le_pow_clog for the last level. Result: star discrepancy ≤ (clog₂N + 3)/N.