A fourth-power difference bound at fixed squared norm

Proved

WorkbookSource.base_7032

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

lean-workbooksource-checked

Let $a, b, c$ be reals satisfying $a^2+b^2+c^2=6$ . Prove that

(a-b)^4+(b-c)^4+(c-a)^4 \leqslant 162

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_7032 (a b c : ℝ) (h : a^2 + b^2 + c^2 = 6) : (a - b)^4 + (b - c)^4 + (c - a)^4 ≤ 162  :=  by sorry

Source