![]() | 1 | initial version |
The following code reproduces the issue.
s0 = 2^(3/4) * sqrt( sqrt(2) + 2 ) + sqrt(2) + 2
s = ( 1 - 8*sqrt(2)*(sqrt(2) - 2)
/
( s0^2 * (2*sqrt(2)/s0 - 4/s0) * (sqrt(2)/s0 - 2/s0) ) )
S = ( 1 - 8*sqrt(2)*(sqrt(2) - 2)
/
( s0^2 * (2*sqrt(2)-4)/s0 * (sqrt(2)-2)/s0 ) )
l = arccosh( s )
n = cosh( l )
L = arccosh( S )
N = cosh( L )
bool( n == 5+4*sqrt(2) )
bool( l == arccosh( n ) )
bool( l == arccosh( 5+4*sqrt(2) ) )
bool( N == 5+4*sqrt(2) )
bool( L == arccosh( N ) )
bool( L == arccosh( 5+4*sqrt(2) ) )
I'm just using a new variable s0
for the repeatedly used denominator. In the posted code, there is some expression (2*sqrt(2)/s0 - 4/s0)
that can be humanly immediately rephrased as (2*sqrt(2)-4)/s0
. Same for the half values. But let us make distinction between the two expressions. So we have two distinct expressions s
and S
. We propagate the change for l
and n
, getting capitalized variables. Running the boolean evaluations against N
and L
we have (in the sage interpreter, started from the linux console):
sage: bool( N == 5+4*sqrt(2) )
....: bool( L == arccosh( N ) )
....: bool( L == arccosh( 5+4*sqrt(2) ) )
....:
True
True
True
Doing the same job for the lower case variables...
sage: bool( n == 5+4*sqrt(2) )
....: bool( l == arccosh( n ) )
....: bool( l == arccosh( 5+4*sqrt(2) ) )
....:
True
True
False
As said in the above comment to the post (and in so many other places), the last False
means that the "standard program/plan" started by sage to test equality did not lead to "the same". The False should be considered as a "can not prove it is true by doing the usual check operations". We can of course help sage simplify one more step...
sage: bool( l.simplify_full() == arccosh( 5+4*sqrt(2) ) )
True