symbolic functions and bool

savecancel

The answer will not be a one liner bool eval, that results into True.

Instead, it is the same explanation done many, many times in such situations, that:

• When sage bool-evaluates such an expression to False it does not mean, that the relation is a false one, instead it means that sage cannot prove the relation is true.
• And that we have to help sage find the True. Sometimes this help is a long story, sometimes a short one. (Sometimes the programmers are not satisfied by this "need to help", but then they should try to improve the algorithm...)

In this case, we have some factors, we will show that each factor is positive for a real number $d>4$.

First of all, the factor $(d+1)$...

sage: var( 'd' );
sage: assume( d>4 )
sage: bool( d+1>0 )
True

OK, this was simple. Now let us consider the factor d - sqrt(d^2 + 8*d - 8) + 4 . We try successively...

sage: var( 'd' );
sage: assume( d, 'real' )
sage: assume( d>4 )
sage: bool( d - sqrt(d^2 + 8*d - 8) + 4 > 0 )
False
sage: bool( d+4 > sqrt(d^2 + 8*d - 8) )
False
sage: bool( (d+4)^2 > sqrt(d^2 + 8*d - 8)^2 )
True

OK, this was not obvious for the computer... Then we will have more to fight with the last parenthesis.

sage: var( 'd' );
sage: assume( d>4 )
sage: assume( d, 'real' )
sage: bool( d^2 - sqrt(d^2 + 8*d - 8)*d + 23*d - sqrt(d^2 + 8*d - 8) - 26 > 0 )
False
sage: bool( d^2 + 23*d - 26 - sqrt(d^2 + 8*d - 8)*d - sqrt(d^2 + 8*d - 8) > 0 )
False
sage: bool( d^2 + 23*d - 26 - sqrt(d^2 + 8*d - 8)*(d+1) > 0 )
False
sage: bool( d^2 + 23*d - 26 > sqrt(d^2 + 8*d - 8)*(d+1) )
False
sage: bool( (d^2 + 23*d - 26)^2 > sqrt(d^2 + 8*d - 8)^2 * (d+1)^2 )
True

This is a possible way to use sage and the minimal human sense for progress while rearranging inequalites. If this is not acceptable, then i have to resign, please ignore the answer.

To give a different point of view on @dan_fulea's answer, note that even Boolean satisfiability is NP-complete. If you include some transcendentals it isn't solvable at all. So it's not surprising that even with better algorithms some combination of $\sqrt{stuff}$ and polynomials might be hard to solve in this fashion.