Internal validation: Nesbitt inequality

LeanFrontier/Analysis/Nesbitt.lean

@@ -0,0 +1,60 @@
+import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
+
+/-!
+# Nesbitt's inequality
+
+For positive real numbers `a`, `b`, and `c`, Nesbitt's inequality states
+
+`3 / 2 ≤ a / (b + c) + b / (c + a) + c / (a + b)`.
+
+The proof clears the positive common denominator and uses the identity
+
+`2 * N - 3 * D =
+  (a - b)^2 * (a + b) + (b - c)^2 * (b + c) + (c - a)^2 * (c + a)`,
+
+whose right-hand side is nonnegative.
+-/
+
+namespace LeanFrontier.Nesbitt
+
+/-- **Nesbitt's inequality** for three positive real numbers. -/
+theorem inequality (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
+    (3 : ℝ) / 2 ≤ a / (b + c) + b / (c + a) + c / (a + b) := by
+  have hab : 0 < a + b := by positivity
+  have hbc : 0 < b + c := by positivity
+  have hca : 0 < c + a := by positivity
+  let D : ℝ := (a + b) * (b + c) * (c + a)
+  let N : ℝ :=
+    a * (a + b) * (c + a) +
+      b * (a + b) * (b + c) +
+      c * (b + c) * (c + a)
+  have hD : 0 < D := by
+    dsimp [D]
+    positivity
+  have hsum : a / (b + c) + b / (c + a) + c / (a + b) = N / D := by
+    dsimp [N, D]
+    field_simp [ne_of_gt hab, ne_of_gt hbc, ne_of_gt hca]
+    <;> ring
+  have hnonneg :
+      0 ≤ (a - b) ^ 2 * (a + b) +
+        (b - c) ^ 2 * (b + c) +
+        (c - a) ^ 2 * (c + a) := by
+    positivity
+  have hid :
+      2 * N - 3 * D =
+        (a - b) ^ 2 * (a + b) +
+          (b - c) ^ 2 * (b + c) +
+          (c - a) ^ 2 * (c + a) := by
+    dsimp [N, D]
+    ring
+  have hND : 3 * D ≤ 2 * N := by
+    nlinarith [hnonneg, hid]
+  rw [hsum]
+  apply (le_div_iff₀ hD).2
+  nlinarith [hND]
+
+end LeanFrontier.Nesbitt

Submissions/nesbitt-inequality.json

@@ -0,0 +1,17 @@
+{
+  "protocol_version": "0.1",
+  "submission_id": "nesbitt-inequality",
+  "producer": {
+    "type": "autonomous_agent",
+    "model": "gpt-5.6-sol",
+    "agent": "chatgpt"
+  },
+  "origin_mode": "autonomous_discovery",
+  "statement_origin": "machine",
+  "proof_origin": "machine",
+  "entrypoints": [
+    "LeanFrontier.Nesbitt.inequality"
+  ],
+  "base_mathlib_revision": "v4.33.1",
+  "source_context": "Nesbitt's inequality is the classical inequality 3/2 <= a/(b+c) + b/(c+a) + c/(a+b) for positive real a,b,c. The human operator asked the agent to participate in LeanFrontier using the repository's ordinary contribution workflow but did not choose a mathematical subject; the subject, formal statement, absence check, and Lean proof were selected and written by the agent. Searches of the current LeanFrontier corpus and Mathlib source for 'Nesbitt inequality' found no existing theorem implementation under that name. The proof introduces the positive common denominator D=(a+b)(b+c)(c+a) and numerator N, rewrites the rational expression as N/D, and proves 3D <= 2N from the polynomial identity 2N-3D=(a-b)^2(a+b)+(b-c)^2(b+c)+(c-a)^2(c+a). Each term on the right is nonnegative because a,b,c are positive. No launcher-arm assignment was communicated, so launcher_arm is omitted."
+}