Using the Matlab symbolic toolkit, consider a square root formula like the following:
syms c; assume(c,'real'); assumeAlso(c > 0);
syms d; assume(d,'real'); assumeAlso(d > 0);
N = (d^2 + 8*c)^0.5 - d
So And I would like to show if this is always positve.
? No, this is ambiguous according to Matlab given these assumptions. Matlab points out that this is ambiguous. And it is, because the root could be positive or negative. If d were 9 and c were 19/8, then the solutions are: -10 - 9 = -19 and +10-9 = 1.
Perhaps I can solve a problem by taking only the positive root? If I take the absolute value of the root, this doesn't fix the problem:
N2 = abs((d^2 + 8*c)^0.5) - d
isAlways(N2 > 0)
The result is still ambiguous. Therefore maybe the root is already positive and I'm misunderstanding what the problem is. If I ask:
isAlways((d^2 + 8*c)^0.5 > 0)
This is always true, so maybe I'm already getting the positive root. But if so, why isn't N2 always greater than 0? Given that c and d are assumed to be real numbers and positive, doesn't d^2 + 8*c have to be greater than d^2? And since the square root is a strictly increasing function, doesn't this imply that sqrt(d^2 + 8*c ) > d?
What I can't do is assume that that . In my more complex non-minimum-working example setting, what's inside the square root is changing but always greater than d^2 (so I want to show , where d itself is potentially a function of multiple inputs but positive and real).
For what it is worth, when I set this up in Mathematica (Mathematica, not Matlab code below), I don't get an ambiguous result, I get that N is always larger than 0.
cond3 = c > 0 && c \[Element] Reals && d > 0 && d \[Element] Reals
Numer = (d^2 + 8*c)^0.5 - d
inequality = ForAll[{b, c}, cond3, Numer > 0]
I fear that I am missing something very basic. Thank you for any help you can provide.