A quartic constraint bounds the first coordinate by sixteen

Proved

LeanWorkbookFaithful.quartic_constraint_bound

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

inequalitieslean-workbookreal-analysis

Let $a,b,c,d$ be strictly positive real numbers satisfying

a+2(b^4+c^4+d^4)+\frac{1}{abcd}=\frac{135}{8}.

Then $a\le16$ . No separate condition $abcd=1$ is assumed.

This is the full inequality from the natural-language statement of Lean Workbook record lean_workbook_plus_27229. It supplies a uniform bound under the original constraint and can be applied without any additional product normalization. The existing formal record includes such an extra hypothesis; this declaration intentionally restores the source statement.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

namespace LeanWorkbookFaithful
theorem quartic_constraint_bound (a b c d : ℝ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d)
    (h : a + 2 * (b ^ 4 + c ^ 4 + d ^ 4) + 1 / (a * b * c * d) = 135 / 8) :
    a ≤ 16 := by sorry
end LeanWorkbookFaithful

Source

https://huggingface.co/datasets/internlm/Lean-Workbook — exact record lean_workbook_plus_27229, natural_language_statement field

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

For all real numbers $a,b,c,d$ with $a>0$ , $b>0$ , $c>0$ , and $d>0$ , if $a+2(b^4+c^4+d^4)+\frac{1}{abcd}=\frac{135}{8}$ , then $a\le 16$ . The positivity assumptions ensure that the denominator $abcd$ is nonzero.

Human review

Flagged by Shuze Chen · Sep 6, 2026
Thank you for the submission. The statement is cleanly prepared, but a single isolated competition style inequality is too narrow to carry a mission. Missions work best when they target a coherent body of connected material.

View graph