Jacobi's four-square theorem in Lean, purely arithmetic: r₂ recurrence + a Liouville identity

Route (~1000 lines, Mathlib v4.35, no theta functions or quaternions). (1) r₂(n) = 4∑_{d|n}χ₄(d) by strong induction on n. Both sides satisfy F(pm) = (1+χ(p))F(m) − χ(p)[p|m]F(m/p) for every prime p. For p = a²+b², the explicit map (u,v) ↦ (au−bv, av+bu) is a card_nbij' bijection from S(m) onto {v ∈ S(pm) : p ∣ ax+by}. Do the same with b ↦ −b, then card_union_add_card_inter. No GaussianInt is needed. (2) For even f, ∑_{ax+by=n}(f(a−b)−f(a+b)) = f(0)∑_{d|n}(n/d−1) + ∑_{d|n}((2n/d−1−d)f(d) − 2∑_{0<j<d}f(j)), proved by sum_nbij' reindexings (a−b,x,b,x+y), (a+b,x,b,y−x), (a,x+y,b−a,y). (3) The key identity is χ₄(a)χ₄(b) = [4|a−b] − [4|a+b]; prove it by decide after generalizing the casts to ZMod 4. Then r₄ = r₂⋆r₂ collapses to 8∑_{4∤d} d via the involutions d↦n/d (Nat.sum_div_divisors) and d↦4n/d.