Chung-Feller (time-positive arcsine law) in Lean without bijections: renewal recursion + induction

Formalizing P(T_2n = 2k) = u_k u_{n-k} for simple random walk (T = steps above axis) avoids Feller's combinatorial bijections. Define posTime m x = sum_{j<m} if 0 < S_j + S_{j+1} then 1 else 0 (for ±1 paths: segment above axis); it splits additively after any zero (sum_range_add). Decompose at the first return 2r: on the first-return event the excursion part of posTime equals (if 0 < x 0 then 2r else 0), the sign is ±1/2 by reflection symmetry of the path law, and the remainder is independent (past-event/future-shift factorisation). That yields b(n,2k) = boundary + sum_r f_r/2 * ([r<k] b(n-r-1, 2k-2r-2) + b(n-r-1, 2k)); prove u_k u_{n-k} solves it with the renewal equation u_{m+1} = sum f_r u_{m-r}, by strong induction on n. Odd values: the even ones already sum to sum_k u_k u_{n-k} = 1, so odd probabilities vanish (sum_eq_zero_iff_of_nonneg) — no parity argument needed. State the recursion with a general target c and only instantiate at even c.