Simplified43.5
\[\leadsto \color{blue}{\frac{b - \sqrt{\mathsf{fma}\left(a, c \cdot -3, b \cdot b\right)}}{a} \cdot -0.3333333333333333}
\]
Proof
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b)))) a) -1/3): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (fma.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 3))) (*.f64 b b)))) a) -1/3): 25 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (*.f64 c (neg.f64 3))) (*.f64 b b))))) a) -1/3): 0 points increase in error, 25 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 c (neg.f64 3)) a)) (*.f64 b b)))) a) -1/3): 25 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 (neg.f64 3) a))) (*.f64 b b)))) a) -1/3): 0 points increase in error, 25 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (+.f64 (*.f64 c (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 3 a)))) (*.f64 b b)))) a) -1/3): 0 points increase in error, 25 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 3 a)) c)) (*.f64 b b)))) a) -1/3): 25 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (*.f64 (neg.f64 (*.f64 3 a)) c))))) a) -1/3): 25 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 b (sqrt.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) a) -1/3): 0 points increase in error, 25 points decrease in error
(*.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) a))) -1/3): 0 points increase in error, 25 points decrease in error
(*.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) a)) -1/3): 25 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (*.f64 -1 a))) -1/3): 0 points increase in error, 25 points decrease in error
(*.f64 (/.f64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (Rewrite<= neg-mul-1_binary64 (neg.f64 a))) -1/3): 25 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) (neg.f64 a)) -1/3): 25 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) (neg.f64 a)) -1/3): 0 points increase in error, 25 points decrease in error
(*.f64 (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (neg.f64 a)) -1/3): 0 points increase in error, 25 points decrease in error
(*.f64 (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 a)) -1/3): 25 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 a)) (Rewrite<= metadata-eval (/.f64 -1 3))): 25 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 -1 3) (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 a)))): 0 points increase in error, 25 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (*.f64 3 (neg.f64 a)))): 25 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 3 a)))): 0 points increase in error, 25 points decrease in error
(/.f64 (*.f64 -1 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 3 a)))): 0 points increase in error, 25 points decrease in error
(Rewrite=> times-frac_binary64 (*.f64 (/.f64 -1 -1) (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)))): 25 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> metadata-eval 1) (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a))): 25 points increase in error, 0 points decrease in error
(Rewrite=> *-lft-identity_binary64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a))): 0 points increase in error, 25 points decrease in error
Simplified43.1
\[\leadsto \color{blue}{\frac{\frac{b}{a} \cdot \frac{b}{a} - \frac{\frac{\mathsf{fma}\left(a, c \cdot -3, b \cdot b\right)}{a}}{a}}{\frac{b}{a} + \frac{\sqrt{\mathsf{fma}\left(a, c \cdot -3, b \cdot b\right)}}{a}} \cdot -0.3333333333333333}
\]
Proof
(*.f64 (/.f64 (-.f64 (*.f64 (/.f64 b a) (/.f64 b a)) (/.f64 (/.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b)) a) a)) (+.f64 (/.f64 b a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a))) -1/3): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (-.f64 (*.f64 (/.f64 b a) (/.f64 b a)) (/.f64 (/.f64 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))))) a) a)) (+.f64 (/.f64 b a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a))) -1/3): 4 points increase in error, 2 points decrease in error
(*.f64 (/.f64 (-.f64 (*.f64 (/.f64 b a) (/.f64 b a)) (/.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a))) a)) (+.f64 (/.f64 b a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a))) -1/3): 0 points increase in error, 6 points decrease in error
(*.f64 (/.f64 (-.f64 (*.f64 (/.f64 b a) (/.f64 b a)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a)))) (+.f64 (/.f64 b a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a))) -1/3): 6 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 (*.f64 (/.f64 b a) (/.f64 b a)) (*.f64 (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a))) (/.f64 (+.f64 (/.f64 b a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a)) -1/3))): 2 points increase in error, 4 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 (*.f64 (/.f64 b a) (/.f64 b a)) (*.f64 (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a))) -1/3) (+.f64 (/.f64 b a) (/.f64 (sqrt.f64 (fma.f64 a (*.f64 c -3) (*.f64 b b))) a)))): 0 points increase in error, 6 points decrease in error