chore: more elementary Motzkin polynomial proof (leanprover-community#28482)

In leanprover-community#23170 @Parcly-Taxel proved that the Motzkin polynomial over the reals is nonnegative. This PR switches the proof to a more elementary one that works over all linearly ordered commutative rings.

Also move out of `Analysis/MeanInequalities` (since it no longer uses that tool).

Author: hrmacbeth

Counterexamples.lean

@@ -12,6 +12,7 @@ import Counterexamples.IrrationalPowerOfIrrational
 import Counterexamples.LinearOrderWithPosMulPosEqZero
 import Counterexamples.MapFloor
 import Counterexamples.MonicNonRegular
+import Counterexamples.Motzkin
 import Counterexamples.OrderedCancelAddCommMonoidWithBounds
 import Counterexamples.Phillips
 import Counterexamples.Pseudoelement

Counterexamples/Motzkin.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 Jeremy Tan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Tan, Heather Macbeth
+-/
+import Mathlib.Tactic.LinearCombination
+import Mathlib.Tactic.Positivity
+
+/-!
+# 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.
+-/
+
+variable {K : Type*} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K]
+
+/-- The **Motzkin polynomial** is nonnegative.
+This bivariate polynomial cannot be written as a sum of squares. -/
+lemma motzkin_polynomial_nonneg (x y : K) :
+    0 ≤ x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1 := by
+  by_cases hx : x = 0
+  · simp [hx]
+  have h : 0 < (x ^ 2 + y ^ 2) ^ 2 := by positivity
+  refine nonneg_of_mul_nonneg_left ?_ h
+  have H : 0 ≤ (x ^ 3 * y + x * y ^ 3 - 2 * x * y) ^ 2 * (1 + x ^ 2 + y ^ 2)
+    + (x ^ 2 - y ^ 2) ^ 2 := by positivity
+  linear_combination H

Mathlib/Analysis/MeanInequalities.lean

@@ -327,21 +327,6 @@ theorem geom_mean_le_arith_mean4_weighted {w₁ w₂ w₃ w₄ p₁ p₂ p₃ p
       ⟨p₂, hp₂⟩ ⟨p₃, hp₃⟩ ⟨p₄, hp₄⟩ <|
     NNReal.coe_inj.1 <| by assumption
 
-/-- As an example application of AM-GM we prove that the **Motzkin polynomial** is nonnegative.
-This bivariate polynomial cannot be written as a sum of squares. -/
-lemma motzkin_polynomial_nonneg (x y : ℝ) :
-    0 ≤ x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1 := by
-  have nn₁ : 0 ≤ x ^ 4 * y ^ 2 := by positivity
-  have nn₂ : 0 ≤ x ^ 2 * y ^ 4 := by positivity
-  have key := geom_mean_le_arith_mean3_weighted (by simp) (by simp) (by simp)
-    nn₁ nn₂ zero_le_one (add_thirds 1)
-  rw [one_rpow, mul_one, ← mul_rpow nn₁ nn₂, ← mul_add, ← mul_add,
-    show x ^ 4 * y ^ 2 * (x ^ 2 * y ^ 4) = (x ^ 2) ^ 3 * (y ^ 2) ^ 3 by ring,
-    mul_rpow (by positivity) (by positivity),
-    ← rpow_natCast _ 3, ← rpow_mul (sq_nonneg x), ← rpow_natCast _ 3, ← rpow_mul (sq_nonneg y),
-    show ((3 : ℕ) * ((1 : ℝ) / 3)) = 1 by simp, rpow_one, rpow_one] at key
-  linarith
-
 end Real
 
 end GeomMeanLEArithMean