The Motzkin polynomial

The Motzkin polynomial is a well-known counterexample: it is nonnegative everywhere, but not expressible as a polynomial sum of squares.

This file contains a proof of the first property (nonnegativity).

TODO: prove the second property.

theorem motzkin_polynomial_nonneg {K : Type u_1} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K] (x y : K) : 0 ≤ x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1

The Motzkin polynomial is nonnegative. This bivariate polynomial cannot be written as a sum of squares.