{"claim":{"bundle":{"code":"","commit":"a418ada038eee5693edab01366053e16caf6e1bb","config":null,"environment":"lemma/0.5.0 agent","logs":"","seeds":[]},"candidate":{"proofs":{"Lemma.am_gm":"import Mathlib.Data.Real.Basic\nimport Mathlib.Algebra.BigOperators.Fin\n\nlemma amgm_bern (c d : ℝ) (hc : 0 ≤ c) (hcd : 0 ≤ c + d) :\n    ∀ m : ℕ, c ^ m * (c + m * d) ≤ c * (c + d) ^ m := by\n  intro m\n  induction m with\n  | zero => simp\n  | succ m ih =>\n    have h1 : c ^ m * (c + m * d) * (c + d) ≤ c * (c + d) ^ m * (c + d) :=\n      mul_le_mul_of_nonneg_right ih hcd\n    have h2 : 0 ≤ c ^ m * ((m : ℝ) * (d * d)) :=\n      mul_nonneg (pow_nonneg hc m) (mul_nonneg (Nat.cast_nonneg m) (mul_self_nonneg d))\n    have e1 : c ^ m * (c + m * d) * (c + d)\n        = c ^ (m + 1) * (c + ((m + 1 : ℕ) : ℝ) * d) + c ^ m * ((m : ℝ) * (d * d)) := by\n      push_cast; grind\n    have e2 : c * (c + d) ^ m * (c + d) = c * (c + d) ^ (m + 1) := by grind\n    grind\n\nlemma amgm_step (A x : ℝ) (hA : 0 ≤ A) (hx : 0 ≤ x) (n : ℕ) :\n    A ^ n * x ≤ ((n * A + x) / (n + 1)) ^ (n + 1) := by\n  have hn : (0 : ℝ) < n + 1 := by\n    have := Nat.cast_nonneg (α := ℝ) n\n    grind\n  have hB : 0 ≤ (n * A + x) / (n + 1) :=\n    div_nonneg (add_nonneg (mul_nonneg (Nat.cast_nonneg n) hA) hx) hn.le\n  have hmul : ((n : ℝ) + 1) * ((n * A + x) / (n + 1)) = n * A + x := by\n    rw [mul_div_assoc']\n    exact mul_div_cancel_left₀ _ hn.ne'\n  rcases hA.lt_or_eq with hA' | hA'\n  · have h := amgm_bern A ((n * A + x) / (n + 1) - A) hA (by grind) (n + 1)\n    have e : A + ((n + 1 : ℕ) : ℝ) * ((n * A + x) / (n + 1) - A) = x := by\n      push_cast; grind\n    rw [e, show A + ((n * A + x) / (n + 1) - A) = (n * A + x) / (n + 1) by grind] at h\n    have : A * (A ^ n * x) ≤ A * ((n * A + x) / (n + 1)) ^ (n + 1) := by\n      calc A * (A ^ n * x) = A ^ (n + 1) * x := by grind\n        _ ≤ _ := h\n    exact le_of_mul_le_mul_left this hA'\n  · subst hA'\n    rcases n with _ | n\n    · simp\n    · simp only [ne_eq, Nat.add_one_ne_zero, not_false_eq_true, zero_pow, zero_mul]\n      exact pow_nonneg hB _\n\nlemma amgm_sum_nonneg : ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → 0 ≤ ∑ i, x i := by\n  intro n\n  induction n with\n  | zero => intro x _; simp\n  | succ n ih =>\n    intro x hx\n    rw [Fin.sum_univ_castSucc]\n    exact add_nonneg (ih _ (fun i => hx _)) (hx _)\n\ntheorem Lemma.am_gm : ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → ∏ i, x i ≤ ((∑ i, x i) / n) ^ n := by\n  intro n\n  induction n with\n  | zero => intro x _; simp\n  | succ n ih =>\n    intro x hx\n    rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]\n    have hS0 : 0 ≤ ∑ i : Fin n, x i.castSucc := amgm_sum_nonneg n _ (fun i => hx _)\n    have hih := ih (fun i => x i.castSucc) (fun i => hx _)\n    have hS00 : n = 0 → ∑ i : Fin n, x i.castSucc = 0 := by rintro rfl; simp\n    generalize ∑ i : Fin n, x i.castSucc = S at hS0 hih hS00 ⊢\n    have hSA : S = n * (S / n) := by\n      rcases Nat.eq_zero_or_pos n with h | h\n      · simp [hS00 h, h]\n      · have : (n : ℝ) ≠ 0 := by exact_mod_cast h.ne'\n        rw [mul_div_assoc']\n        exact (mul_div_cancel_left₀ _ this).symm\n    have hA : 0 ≤ S / n := div_nonneg hS0 (Nat.cast_nonneg n)\n    have key := amgm_step (S / n) (x (Fin.last n)) hA (hx _) n\n    rw [← hSA] at key\n    push_cast\n    calc (∏ i : Fin n, x i.castSucc) * x (Fin.last n)\n        ≤ (S / n) ^ n * x (Fin.last n) := mul_le_mul_of_nonneg_right hih (hx _)\n      _ ≤ _ := key\n"}},"flags":[],"id":1,"label":"network-best","measured":1.0,"reason":null,"score":1.0,"significance":[],"status":"verified","verdicts":[]},"entry":{"body":"Prove Lemma.am_gm under its imports\nMethod: Write a complete Lean proof of Lemma.am_gm: ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → ∏ i, x i ≤ ((∑ i, x i) / n) ^ n. The AM-GM inequality without analysis. Mathlib derives it from the concavity of the logarithm; here there is no log, exp or convexity. Cauchy's forward-backward induction, or smoothing (replace two unequal values by their mean). Start from proofs/Lemma.am_gm.lean. If it is out of reach in the budget, prove a useful lemma toward it, post what blocks you to the chat, and submit what you have verified.\nThreshold: 0 (must beat). Result 1; checked by the coordinator (tier 1, exact).\nSubmitter notes (data): AM-GM by induction on n via Fin.prod_univ_castSucc. Step: A^n x ≤ ((nA+x)/(n+1))^(n+1), from homogeneous Bernoulli c^m(c+md) ≤ c(c+d)^m (c≥0, c+d≥0) with c=A, d=B-A, cancel A>0; A=0 handled separately. Imports lack ring/linarith/positivity/field_simp; grind does the ring/linear steps.","claim":1,"created":1791790181,"credit":[2],"id":1,"kind":"result","label":"network-best","parent":null,"program":"lean-ablations","score":1.0,"title":"Network best: theorems proved 1","unit":4},"followups":[{"hypothesis":"Prove Lemma.fermat_little under its imports","status":"succeeded","unit":1},{"hypothesis":"Vary it: small perturbations of the C1 result (1) lead somewhere better","status":"closed","unit":20},{"hypothesis":"Scale it: a longer search seeded from C1 (1) improves further","status":"closed","unit":21},{"hypothesis":"Combine it: merging C1 (1) with other strong results beats it","status":"closed","unit":22},{"hypothesis":"Prove Lemma.four_squares under its imports","status":"open","unit":23}]}