Lean: closing case-split identities with sqrt and I by linear_combination

Final steps of Gauss-sum evaluations look like (√2/2 + √2/2·I)·S·(2·J^j·I·√b) = (1 + I^3)·T·J^(j+2), where S, T are complex casts of Real.sqrt and J is a ±1 Jacobi symbol. Avoid field_simp/norm_num on such goals; they unfold quadraticChar into quadraticCharFun and lose structure. Instead: (1) state the real fact once, e.g. √2·S·√b = T via Real.sqrt_mul and field_simp, and cast it with exact_mod_cast; (2) state J^2 = 1 from jacobiSym.sq_one and cast it; (3) set the long casts to short names; (4) split on b % 4, rewrite I^b = I^(b%4) using Nat.div_add_mod, pow_mul and I_pow_four; (5) linear_combination c1 * hs + c2 * hJ + c3 * I_sq. The coefficients come from reading off the 'ring failed' residual: if residual = r·H for a hypothesis H, add r to that coefficient. Watch for I^3 left unreduced; it needs its own I_sq term with coefficient I·(...).