F = (9-k)^2 k x^2 y^2 z^2 (x y+x z+y z)+(3 k x y z (x+y+z)+(x y+x z+y z) (x^2-2 x y+y^2-2 x z-2 y z+z^2))^2;
只用考虑 s[y z]<=0，此时
F+ (k(9-k) )/(3+k) ((x-y)^2) ((y-z)^2) ((-x+z)^2) (x y+x z+y z) 对任意 0<=k<=9 是平方和，
F=(9-k)^2 k x^2 y^2 z^2 (x y+x z+y z)+(3 k x y z (x+y+z)+(x y+x z+y z) (x^2-2 x y+y^2-2 x z-2 y z+z^2))^2;
3(3+k)(F+(k(9-k) )/(3+k) (x-y)^2 (y-z)^2 (-x+z)^2 (x y+x z+y z) )== s[(3+k)^2 x^2 y z-2 (-3+k) y^2 z^2+(-3+k) x^3 (y+z)]^2+ k(9-k) s[((y-z)^2 (-x^2 (y+z)+y z (y+z)+x (y^2+(1+k) y z+z^2))^2)/2 ] //Factor
(* True *)
所以
((9-k)^2 k x^2 y^2 z^2+((9-k) k (x-y)^2 (y-z)^2 (-x+z)^2)/(3+k))F== ((9-k) k (x-y)^2 (y-z)^2 (-x+z)^2 (3 k x y z (x+y+z)+(x y+x z+y z) (x^2-2 x y+y^2-2 x z-2 y z+z^2))^2)/(3+k)+(9-k)^2 k x^2 y^2 z^2 ((-2 (-3+k) x^2 y^2+(3+k)^2 x^2 y z+(3+k)^2 x y^2 z-2 (-3+k) x^2 z^2+(3+k)^2 x y z^2-2 (-3+k) y^2 z^2+(-3+k) (x+y) z^3+(-3+k) y^3 (x+z)+(-3+k) x^3 (y+z))^2/(3 (3+k))+((9-k) k )/(6 (3+k)) s[ (x-y)^2 (x y (x+y)+(x^2+(1+k) x y+y^2) z-(x+y) z^2)^2]) //Factor
(* True *)
只用考虑 s[y z]<=0，此时
F+ (k(9-k) )/(3+k) ((x-y)^2) ((y-z)^2) ((-x+z)^2) (x y+x z+y z) 对任意 0<=k<=9 是平方和，
F=(9-k)^2 k x^2 y^2 z^2 (x y+x z+y z)+(3 k x y z (x+y+z)+(x y+x z+y z) (x^2-2 x y+y^2-2 x z-2 y z+z^2))^2;
3(3+k)(F+(k(9-k) )/(3+k) (x-y)^2 (y-z)^2 (-x+z)^2 (x y+x z+y z) )== s[(3+k)^2 x^2 y z-2 (-3+k) y^2 z^2+(-3+k) x^3 (y+z)]^2+ k(9-k) s[((y-z)^2 (-x^2 (y+z)+y z (y+z)+x (y^2+(1+k) y z+z^2))^2)/2 ] //Factor
(* True *)
所以
((9-k)^2 k x^2 y^2 z^2+((9-k) k (x-y)^2 (y-z)^2 (-x+z)^2)/(3+k))F== ((9-k) k (x-y)^2 (y-z)^2 (-x+z)^2 (3 k x y z (x+y+z)+(x y+x z+y z) (x^2-2 x y+y^2-2 x z-2 y z+z^2))^2)/(3+k)+(9-k)^2 k x^2 y^2 z^2 ((-2 (-3+k) x^2 y^2+(3+k)^2 x^2 y z+(3+k)^2 x y^2 z-2 (-3+k) x^2 z^2+(3+k)^2 x y z^2-2 (-3+k) y^2 z^2+(-3+k) (x+y) z^3+(-3+k) y^3 (x+z)+(-3+k) x^3 (y+z))^2/(3 (3+k))+((9-k) k )/(6 (3+k)) s[ (x-y)^2 (x y (x+y)+(x^2+(1+k) x y+y^2) z-(x+y) z^2)^2]) //Factor
(* True *)
