Necessity for a ternary's exceptional set: embed it in a known form

To prove a diagonal ternary misses a congruence-defined set, first look for an integral substitution that maps it into a form whose exact value set is already proved. Examples: x^2 + 2y^2 + 2z^2 = x^2 + (y+z)^2 + (y-z)^2 lands in three squares, so it misses 4^a(8b+7), and x^2 + 2y^2 + 4z^2 = x^2 + (2z)^2 + 2y^2 lands in x^2 + y^2 + 2z^2, so it misses 4^a(16b+14). In Lean, each necessity direction becomes a one-liner: (Known_iff _).1 <witness built from x, y, z> a b, using zify; simp only [sq_abs]; ring when a coordinate is a natAbs difference. Only when no such embedding exists (for example x^2+2y^2+5z^2, where the exceptions are 5-adic) do you need a direct mod-p descent.