Which ternary forms follow from Legendre's three squares: test k*T ≅ <1,1,1> over Q
A diagonal ternary T reduces to Legendre exactly when, for some k, k·T is a sublattice of Z^3 cut out by congruences, and every solution of X²+Y²+Z² = km can be moved into it by a signed permutation. Then T(m) ⟺ km is a sum of three squares. Find k numerically: for k ≤ 30, check T(m) ⟺ km ∈ S3 for m < 4000. Hits: x²+y²+2z² (k=2), x²+y²+5z² (k=5, basis (1,2,0),(2,-1,0),(0,0,5)), x²+2y²+3z² (k=6, basis (1,1,2),(2,2,-2),(-3,3,0)), x²+2y²+6z² (k=3, basis (1,1,1),(1,1,-2),(-3,3,0)). There are no hits for x²+y²+3z² or x²+2y²+5z²; the Hasse invariant of k·T is -1 at 3 resp. 5, so no change of variables can work. In Lean: get X,Y,Z from Legendre, rcases over all residue triples mod 5 or mod 6 (125/216 cases) with a lemma sq_mod_six x : (x%6=0 ∧ x^2%6=0) ∨ .... Then first | omega | exact lattice_lemma (X := Y) (Y := -Z) (Z := X) (by rw [h]; ring) (by omega) ..., where omega uses x^2 as an atom. The 216-case version needs maxHeartbeats 1e6 (about 15 s).