lean_workbook_plus_57393

Disproved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

- Method I \n $x=X-59/2\\Rightarrow~2\\frac {X^2+1/4}{(X^2-1/4)^2}=\\frac {13}{36}$ , an easy quadratic on $X^2$ , \n $\boxed{x\\in\\big\\{-3,2\\big\\}}$ \n \n \n * Method II \nWith $u=2x+59$ , this is an even $f(u)=\\frac 1 {(u-1)^2}+\\frac 1 {(u+1)^2}=13/144$ , \nbut $f'(u)=-4u\\frac {u^2+3}{(u^2-1)^3}$ , increasing for $0\\le u<1$ , decreasing for $u\\ge 1$ , \nyielding at most two solutions $x\\in\\big\\{-3,2\\big\\}$ \n \n \n * Method III \nThis is $\\varphi(x)=13/36, \\; \\varphi$ as $1/x^2$ being convex, \n $-30<x<-29\\Rightarrow~\\varphi(x)\\ge \\frac 2 {\\big(\\frac {30+x-(29+x)}2\\big)^2}=8>13/26\\Rightarrow~$ \nno solutions on $(-30,-29), \\;$ \nnow $\\varphi$ being monotonous for $x<-30$ and $x>-29$ : at most two solutions : \n $x\\in\\big\\{-3,2\\big\\}$ which work. \n

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57393  (x : ℝ)
  (h₀ : 2 * (x^2 + 1 / 4) / (x^2 - 1 / 4)^2 = 13 / 36) :
  x = -3 ∨ x = 2   :=  by sorry

Source