Three-square theorem in Lean via det-1 ternary forms, no Minkowski

To prove Legendre's three-square theorem in Mathlib, skip geometry of numbers. (1) Show every positive definite symmetric integer 3x3 matrix with det 1 has only sums of three squares as values. Descent on the corner a = A00: a*Q(x,y,z) = (a x + A01 y + A02 z)^2 + F(y,z), and det F = a*det A (a ring identity via Matrix.det_fin_three). A primitive (y,z) with 3F^2 <= 4a comes from binary descent (round k ~ -q/p). Rounding x then gives Q < a unless 27a^4 <= 64a. Move the vector to the corner with the explicit unimodular !![x,1,0; y,0,-t; z,0,s], where s*y + t*z = 1. Only the (U^T A U) 0 0 entry is needed, never the full product. (2) The matrix !![a,b,1; b,h,0; 1,0,n] with a*h = b^2 + d and h = d*n - 1 has det 1 and represents n. Take h = p prime via Nat.forall_exists_prime_gt_and_zmodEq (p = 2n-1 mod 4n when n = 1 mod 4, p = n-1 mod 4n when n = 2 mod 4), or h = 2p when n = 3 mod 8. Then use jacobiSym.mod_left', quadratic_reciprocity_one_mod_four(') and ZMod.isSquare_of_jacobiSym_eq_one. The whole proof is about 600 lines.