Establish the equivalence of two inverse trigonometric function based formulas

Question

In a comment to

3D5D

user JimB provided an answer to the question posed there of finding the "two-quater[nionic]bit" absolute separability Hilbert-Schmidt probability. (Previously, in TwoQubit, he had obtained the "two-qubit" counterpart.)

The answer now took the form

327574875999612773528659/95105071448064 - 2951081236201839/(524288 Sqrt[2]) - (15390446918294583135 \[Pi])/(17179869184 Sqrt[2]) + (15390446918294583135 ArcCsc[18/Sqrt[50 + 17 Sqrt[2]]])/(2147483648 Sqrt[2])

An earlier answer,

-((13 (-216449750678398795533760757497856 + 
   176860737736399592490919645937664 Sqrt[2] + 
   279292548969739228073088142369304501839785 Sqrt[2] \[Pi] - 
   558572941247617043110461841280869072896000 Sqrt[2]
     ArcCot[Sqrt[2]] + 
   23637916932187025487103667523337320 Sqrt[2]
     ArcCot[2 Sqrt[2]] - 
   16178155879591789043088455851252390200 Sqrt[2]
     ArcCot[3 + Sqrt[2]] - 
   558589165778586158484606527963549721006600 Sqrt[2]
     ArcTan[Sqrt[2]]))/816946343106356485029888)

of somewhat different form, to the very same question had been provided in eq. (36) in

2009paper

Both formulas above evaluate (N[,50]) to

0.000039870347068019928855365404975780992652117606213067

However, the FullSimplify command does not reveal the formulas' evident equivalence.

It might seem that some inverse trigonometric function transformations would be required to accomplish that.

So, can the evident equivalence of the two formulas be formally established employing Mathematica?

Answer 1

FindIntegerNullVector is your friend. Notice that this method allows you to obtain an even simpler expression.

A. Find relations between sets of different functions

v[1]={ArcCsc[18/Sqrt[50+17 Sqrt[2]]],ArcTan[Sqrt[2]],ArcCot[3+Sqrt[2]]};
v[2]={ArcCot[Sqrt[2]],ArcCot[2 Sqrt[2]],ArcCot[3+Sqrt[2]]};
v[3]={ArcCot[2 Sqrt[2]],ArcCot[Sqrt[2]],ArcTan[Sqrt[2]]};
v[4]={ArcCot[Sqrt[2]],ArcTan[Sqrt[2]],π/2};

B. This is the main part

Table[FindIntegerNullVector[N[v[i],1000]],{i,4}]
Out[1]= {{-3,-1,11},{-2,1,4},{1,1,-1},{1,1,-1}}

C. Make a list of replacement rules

r[1]={ArcCsc[18/Sqrt[50+17 Sqrt[2]]]->(-ArcTan[Sqrt[2]]+11ArcCot[3+Sqrt[2]])/3};
r[2]={ArcCot[3+Sqrt[2]]->1/4(2ArcCot[Sqrt[2]]-ArcCot[2 Sqrt[2]])};
r[3]={ArcCot[2 Sqrt[2]]->ArcTan[Sqrt[2]]-ArcCot[Sqrt[2]]};
r[4]={ArcCot[Sqrt[2]]->π/2-ArcTan[Sqrt[2]]};

D. Apply the rules

sx=Fold[ReplaceAll,x,Array[r,4]]//Expand;
sy=Fold[ReplaceAll,y,Array[r,4]]//Expand;
sx-sy
Out[2]= 0

Comment/observation

In principle, all but one identities found by the LLL method are easy to prove by hand. Only the first one, namely $$11\,\mathrm{arccot}\big(3+\sqrt{2}\big) = \mathrm{arctan}\big(\sqrt{2}\big)+ 3\,\mathrm{arccsc}\!\Bigg\{\frac{18}{\sqrt{50+17 \sqrt{2}}}\Bigg\}$$ is somewhat unexpected.