lean_workbook_plus_25399

⚠️ Retired — mistyped fractional exponent

The exponent ^(1 / 2) in the Lean statement below is natural-number division, not a real exponent, so it collapses 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.

Let $\sqrt{x-2y}=t\ge 0.\ (1)$ Then the first equation gives $y=\frac{1}{2x^3}(3x+1-2xt). \ (2)$ From $(1)$ and $(2)$ we get $x^4-x^3t^2=3x+1-2xt. \ (3)$ Substituting $(2)$ into the second equation of the given system we get: $x^4+x^3=x^2(t^2+1)(3-2t)+x(t^2-2t+4)+1. \ (4)$ Substituting $x^4$ from $(3)$ into $(4)$ we get $x^3=x^2(3-2t)+x. \ (5)$ Multiplying $(5)$ by $x$ and substituting the resulting $x^4$ term into $(3)$ we get $x^3(t-1)(t+3)=x^2-(3-2t)x-1. \ (6)$ But the $RHS$ of $(6)$ is $=0$ because of $(5).$ Therefore $t=1.$ Now from $(5)$ we get that $x=\frac{1\pm\sqrt{5}}{2},$ and from $(1)$ we get $y=\frac{-1\pm\sqrt{5}}{4}.$

Why this node was retired

The posted statement is

theorem lean_workbook_plus_25399  (x y : ℝ)
  (h₀ : 0 ≤ x - 2 * y)
  (h₁ : (x - 2 * y)^(1 / 2) = x * y)
  (h₂ : x^4 + x^3 = x^2 * (x - 2 * y) + x * (x - 2 * y)^2 + 1) :
  x = (1 + Real.sqrt 5) / 2 ∧ y = (-1 + Real.sqrt 5) / 4 ∨ x = (1 - Real.sqrt 5) / 2 ∧ y = (-1 - Real.sqrt 5) / 4   :=  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 / 2) → ^0, so the radical is 1 for every base

The recorded counterexample refutes the collapsed statement. It says nothing about the exercise displayed on this page, which is a different proposition.

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.

Proposed corrected statement

Recover the original two equations from the full source record, use Real.sqrt(x−2y), and prove the complete solution classification. The supplied derivation does not justify the different stored equations.

From the public Prove2Me statement audit (wamlat/prove2me-errors). That proposal is natural-language mathematics and is not Lean-verified; it is a specification for a corrected node, not a drop-in replacement.