lean_workbook_plus_79596

⚠️ Retired — mistyped fractional exponent

The exponents ^(1 / 3), ^(1 / 6) in the Lean statement below are natural-number division, not a real exponent, so they collapse to an integer power and the displayed radical is not what is being asserted. Do not import this node or use it as a dependency.

prove that: $\sqrt[6]{\frac{(a+b)(b+c)(c+a)(a+d)(d+b)(d+c)}{64}} \geq \sqrt[3]{\frac{abc+bcd+cda+adb}{4}}$, where $a;b;c;d>0$

Why this node was retired

The posted statement is

theorem lean_workbook_plus_79596 (a b c d : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) : ((a + b) * (b + c) * (c + a) * (a + d) * (d + b) * (d + c) / 64)^(1 / 6) ≥ (a * b * c + b * c * d + c * d * a + d * a * b / 4)^(1 / 3)   :=  by sorry

A numeric-literal exponent carrying no type ascription is elaborated at type ℕ (via HPow ℝ ℕ ℝ, Monoid.npow), and natural-number division truncates. Each occurrence therefore collapses:

• ^(1 / 3) → ^0, so the radical is 1 for every base
• ^(1 / 6) → ^0, so the radical is 1 for every base

What the accepted submission established is therefore a proof of the collapsed statement, not of the exercise displayed on this page. The submission is not thereby invalid — a proof of a malformed proposition can be a correct proof of that proposition — but its Proved status must not be read as settling the source problem.

What a faithful statement would require

Every fractional exponent must be given a real type, e.g. x ^ ((1 : ℝ) / 3) using Real.rpow, or be written with the intended root operation (Real.sqrt, or the signed real cube root where the radicand may be negative). Real powers also need their own domain hypotheses: rpow is only the intended root for a nonnegative base.

No corrected replacement node exists yet, and this target has no record in the public Prove2Me statement audit — the defect above was identified directly from the Lean text.