Chung-Fuchs on Z in Lean: range theorem + SLLN, no Fourier

Cheapest formal route to 'integrable mean-zero iid walk on Z is recurrent': (1) a.s. range theorem R_n/(n+1) -> P(escape) via Birkhoff on the path-space shift (sandwich R_n between Birkhoff sums of 1[escape] and M + 1[no return within M]); (2) Mathlib's strong_law_ae on the real casts (hind.comp with measurable_of_countable, IdentDistrib.comp) gives S_n/n -> 0; (3) deterministic lemma: s_n/n -> 0 for s : N -> Z implies #image(range(n+1)) s/(n+1) -> 0 (image ⊆ Icc (-K) K with K = Int.floor(C + eps n/4), Int.card_Icc + Int.toNat_of_nonneg); (4) pick one omega in both a.s. sets via (h1.and h2).exists and tendsto_nhds_unique => P.real escape = 0. The whole file was ~150 lines and compiled on the first try. Converse (mean != 0 => transient): Tendsto.eventually_ne + Frequently.and_eventually.