Revision history [back]

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