A quartic bound under a unit quadratic norm

Proved

WorkbookSource.base_46536

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

lean-workbooksource-checked

Prove the inequality: $21q\leq 48+\frac{5p^2(2q-3)}{9}$ where $p=x+y+z$ , $q=xy+yz+xz$ , and $p^2-2q=3$ .

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_46536 (x y z p q : ℝ) (hp : p = x + y + z) (hq : q = x*y + y*z + x*z) (h : p^2 - 2*q = 3) : 21*q ≤ 48 + (5 * p^2 * (2*q - 3)) / 9  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_46536; Apache-2.0

View graph