When Close Enough Is Close Enough *

* The article "When Close Enough Is Close Enough" is published by Edward R. Scheinerman on American Mathematical  Monthly, June-July 2000

Prelude

The following equations are taken from my brother's algebra workbook. He always challenges me to prove these equations by Mathematica, otherwise to remove this software to save disk space for his PC games. 
(1) (Sqrt[5 - 2 (Sqrt[ 6])]) = -(Sqrt[2]) + (Sqrt[3])
(2) ((20 + 14 (Sqrt[ 2]))^(1/3)) + ((20 - 14 (Sqrt[ 2]))^(1/3)) = 
        4
(3) ((5 (Sqrt[13]) - 18)^(1/3)) = (1/2) (-3 + (Sqrt[13]))
(4) \(TraditionalForm\`\@\(\(9 - 5 \@ 3\)\/\(9 + 5 \@ 3\)\)\%3 = \(\@3 - 1\)\/\@\(3 + 1\)\)
(5) \(TraditionalForm\`\@\(\(3 + 2 \@ 5\%4\)\/\(3 - 2 \@ 5\%4\)\)\%4 = \(\@5\%4 + 1\)\/\(\@5\%4 - 1\)\)

I am very lucky that Mathematica's FullSimplify[] function is powerful enough to solve these problems . But I am not sure whether what my brother brings next time may prove Mathematica a "failure". After reading Mr. Scheinerman's article, now, I know how to deal with these problems "manually", if FullSimplify happens to fail. If you have the same brother or interest as I do, please go on reading.

Main Idea

The main idea of Scheinerman's article is expressed below. It is highly recommended for you to read the original paper if possible.

When does \(TraditionalForm\`|α - β| < ε\) imply α = β ? For example, if α and β are integers, then if we know that \(TraditionalForm\`|α - β|\) is (say) less than 0.9, then we may conclude that  α = β .

Let n and b be positive integers. Let M(n,  b) denote the set of all n×n matrices whose entries  are integers bounded in absolute value by b. Let Λ(n,  b) denote the set of all eigenvalues of matrices in M(n,  b).

Proposition 1. Let A ∈ M(n,  b). Then det(λ I - A) is a monic, integer polynomial.

Proposition 2. Let α be a complex number. Then α is an algebraic integer if and only if α ∈  Λ(n,  b) for some positive integers n,  b.

Proposition 3. Suppose α ∈  Λ(n,  b). Then \(TraditionalForm\`|α| ≤ \ n\ b\).

Theorem 4. Suppose A ∈  M(n,  b) and α is a nonzero eigenvalue of A. Then \(TraditionalForm\`|α| ≥ \ \((n\ b)\)\^\(1 - n\)\).

Theorem 4 is a known as a root separation theorem; It enables us to answer the question: When is close enough, close enough? Suppose we are given an algebraic expression, such as α = (Sqrt[5 - 2 (Sqrt[ 6])]) + (Sqrt[2]) - (Sqrt[3]). We need to find integers n and b such that α ∈  Λ(n,  b). Then we calculate α to sufficient precision to show that  \(TraditionalForm\`|α| < \ \((n\ b)\)\^\(1 - n\)\). From this, it follows that α = 0.

The issue, then, is: Given an algebraic expression α, how do we find positive integers n and b such that α ∈ Λ(n,  b)? The next result gives us tools to find n and b.

Theorem 5. Let n,  (Subscript[n, 1]),  (Subscript[n, 2]),  b,  (Subscript[b, 1]),  (Subscript[b, 2]) be positive integers.
1. If α is a root of a monic integer polynomial of degree n whose coefficients have absolute value no larger than b, then α ∈ Λ(n,  b).
2. If  (Subscript[n, 1]) ≤  (Subscript[n, 2]) and (Subscript[b, 1]) ≤  (Subscript[b, 2]), then Λ((Subscript[n, 1]),  
          (Subscript[b, 1])) ⊆ Λ((Subscript[n, 2]),  (Subscript[b, 2])).
3. If α ∈ Λ(n,  b), then -α and \(TraditionalForm\`a\&_ ∈ Λ(n, \ b)\).
4. If  k is an integer, then k ∈  Λ(
          1,  |k|).
5. If α ∈ Λ((Subscript[n, 1]),  
          (Subscript[b, 1])) and β ∈ Λ((Subscript[n, 2]),  (Subscript[b, 2])), then \(TraditionalForm\`α\ β ∈ Λ(\(n\_1\) n\_2, \ b\_1\ b\_2)\).
6. If α ∈ Λ((Subscript[n, 1]),  
          (Subscript[b, 1])) and β ∈ Λ((Subscript[n, 2]),  (Subscript[b, 2])). then \(TraditionalForm\`α + β ∈ Λ(\(n\_1\) n\_2, \ b\_1 + b\_2)\).
7. If k is a positive integer and (β^k) ∈ Λ(n,  b), then β ∈ Λ(n k,  b).

Mathematica Implementation

I implement the Mathematica function CalculateEquality[] to check the equality of equations in the prelude. 
First ExpressionToΛ[] constructs Λ(n,  b) from the input expression according to Theorem 5. Then CalculateResult[] figures out whether α = 0 according to Theorem 4.

ExpressionToΛ[expression_,  Λ_] := 
      Module[{separate}, 
Λ[a_,  
              b_] + Λ[c_,  d_] ^:= Λ[a c,  
            b + d]; 
Λ[a_,  
              b_] Λ[c_,  d_] ^:= Λ[a c,  
            b d]; 
Λ[a_,  b_]^k_ ^:= Λ[a k,  b]; 
separate[x_ + y_] := 
          separate[x] + separate[y]; 
separate[x_*y_] := 
          separate[x]*separate[y]; 
separate[
            x_^y_ /; IntegerQ[1/y]] := 
          separate[x]^(1/y); 
separate[
            x_Integer] := Λ[1,  
            Abs[x]]; 
separate[expression]]

CalculateResult[expression_,  Λ_] := 
      Module[{threshold}, 
Block[{$MaxExtraPrecision = 
              500,  Message},  
threshold = 
            N[(((Λ[[1]] Λ[[2]]))^(1 - Λ[[1]]))]; 
N[Abs[expression],  
              Abs[Log[10,  threshold]]] < 
            threshold
]
]

CalculateEquality[expression_] := 
      Module[{Λ},  
CalculateResult[
          expression,  
          ExpressionToΛ[
            expression,  Λ]]]

Examples

I would use equations (1) through (5) as examples to verify my function.

1. Before using CalculateEquality[], you have to construct α first. In this case α = (Sqrt[5 - 2 (Sqrt[ 6])]) + (Sqrt[2]) - (Sqrt[3])

(Sqrt[5 - 2 (Sqrt[ 6])]) == (Sqrt[3]) - (Sqrt[2])

As I have mentioned FullSimplify[] works very well,

FullSimplify[(Sqrt[5 - 2 (Sqrt[ 6])])]

as well as my function.

CalculateEquality[(Sqrt[5 - 2 (Sqrt[ 6])]) + (Sqrt[2]) - (Sqrt[3])]

2. \(TraditionalForm\`α = \@\(20 + 14 \@ 2\)\%3 + \@\(20 - 14 \@ 2\)\%3 - 4\)

FullSimplify[((20 + 14 (Sqrt[ 2]))^(1/3)) + ((20 - 14 (Sqrt[ 2]))^(1/3))]

CalculateEquality[((20 + 14 (Sqrt[ 2]))^(1/3)) + ((20 - 14 (Sqrt[ 2]))^(1/3)) - 
        4]

3. α = 
        2 (( 5 (Sqrt[13]) - 18)^(1/3)) -  (-3 + (Sqrt[13]))

FullSimplify[((5 (Sqrt[13]) - 18)^(1/3))]

CalculateEquality[
      2 (( 5 (Sqrt[13]) - 18)^(1/3)) - (-3 + (Sqrt[13]))]

Important In this case α is not  ((5 (Sqrt[13]) - 18)^(1/3)) - 
        (1/2) (-3 + (Sqrt[13])) , you have to eliminate (1/2) by double both sides of the equation. It does no harm for a equation if both sides are equal. This principle holds true for the rest of the problems.

4. α = ((9 - 5 (Sqrt[ 3]))^(1/3)) ((Sqrt[3]) + 
                1) - ((Sqrt[3]) - 1) ((9 + 5 (Sqrt[ 3]))^(1/3))

FullSimplify[(((((9 - 5 (Sqrt[ 3]))/(9 + 5 (Sqrt[ 3])))))^(1/3))]

CalculateEquality[((9 - 5 (Sqrt[ 3]))^(1/3)) ((Sqrt[3]) + 1) - ((Sqrt[3]) - 
              1) ((9 + 5 (Sqrt[ 3]))^(1/3))]

5. α = ((3 + 2 ( 5^(1/4)))^(1/4)) ((5^(1/4)) - 
                1) - ((5^(1/4)) + 1) ((3 - 2 ( 5^(1/4)))^(1/4))

$MaxExtraPrecision = 500

FullSimplify[((((3 + 2 ( 5^(1/4)))/(3 - 2 ( 5^(1/4)))))^(1/4)) == (((5^(1/4)) + 1)/((5^(1/4)) - 1))]

CalculateEquality[((3 + 2 ( 5^(1/4)))^(1/4)) ((5^(1/4)) - 
              1) - ((5^(1/4)) + 1) ((3 - 2 ( 5^(1/4)))^(1/4))]

6. This last example shows that CalculateEquality[] does not always return True. If there is little difference, it can be detected. Say \(TraditionalForm\`\@7502 + \@121393 + \@196418 + \@317811 ≠ \@514229 + \@832040\)

CalculateEquality[(Sqrt[7502]) + (Sqrt[121393]) + (Sqrt[196418]) + (Sqrt[317811]) - (Sqrt[514229]) - (Sqrt[832040])]

Further Reading

In Edward R. Scheinerman's paper, he also presents one more calculation efficient way to construct Λ(n,  b). And a more complicated problem is solved as example. So reading his original paper is recommended. 
Edward R. Scheinerman, When Close Enough Is Close Enough, American Mathematical Monthly, June-July 2000