A quartic bound under a quartic relation

Proved

WorkbookSource.base_30734

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that if $(a^2-2b)^2+4b^2=2a$ , then $(a^2-4b)^2<=3$

Source: InternLM Lean-Workbook, record lean_workbook_30734 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_30734 (a b : ℝ) (h : (a^2 - 2 * b)^2 + 4 * b^2 = 2 * a) :
  (a^2 - 4 * b)^2 ≤ 3  :=  by sorry

Source