====================================================================
RealClosure examples
====================================================================

The Real Closure 1.0 package provided by Renaud Rioboo consists of
different packages, categories and domains :

The package RealPolynomialUtilitiesPackage which needs a Field F and a 
UnivariatePolynomialCategory domain with coefficients in F. It computes 
some simple functions such as Sturm and Sylvester sequences sturmSequence,
sylvesterSequence.

The category RealRootCharacterizationCategory provides abstract
functions to work with "real roots" of univariate polynomials. These
resemble variables with some functionality needed to compute important
operations.

The category RealClosedField provides common operations available over
real closed fiels. These include finding all the roots of a univariate
polynomial, taking square (and higher) roots, ...

The domain RightOpenIntervalRootCharacterization is the main code that
provides the functionality of RealRootCharacterizationCategory for the
case of archimedean fields. Abstract roots are encoded with a left
closed right open interval containing the root together with a
defining polynomial for the root.

The RealClosure domain is the end-user code. It provides usual arithmetic 
with real algebraic numbers, along with the functionality of a real closed 
field. It also provides functions to approximate a real algebraic number 
by an element of the base field. This approximation may either be absolute, 
approximate or relative (relativeApprox).

====================================================================
CAVEATS
====================================================================

Since real algebraic expressions are stored as depending on "real
roots" which are managed like variables, there is an ordering on
these. This ordering is dynamical in the sense that any new algebraic
takes precedence over older ones. In particular every creation
function raises a new "real root". This has the effect that when you
type something like sqrt(2) + sqrt(2) you have two new variables
which happen to be equal. To avoid this name the expression such as in
s2 := sqrt(2) ; s2 + s2

Also note that computing times depend strongly on the ordering you
implicitly provide. Please provide algebraics in the order which seems
most natural to you.

====================================================================
LIMITATIONS
====================================================================

This packages uses algorithms which are published in [1] and [2] which
are based on field arithmetics, in particular for polynomial gcd
related algorithms. This can be quite slow for high degree polynomials
and subresultants methods usually work best. Beta versions of the
package try to use these techniques in a better way and work
significantly faster. These are mostly based on unpublished algorithms
and cannot be distributed. Please contact the author if you have a
particular problem to solve or want to use these versions.

Be aware that approximations behave as post-processing and that all
computations are done exactly. They can thus be quite time consuming when
depending on several ``real roots''.

====================================================================
REFERENCES
====================================================================


[1]  R. Rioboo : Real Algebraic Closure of an ordered Field : Implementation 
     in Axiom. 
     In proceedings of the ISSAC'92 Conference, Berkeley 1992 pp. 206-215.

[2]  Z. Ligatsikas, R. Rioboo, M. F. Roy : Generic computation of the real
     closure of an ordered field.
     In Mathematics and Computers in Simulation Volume 42, Issue 4-6,
     November 1996.

====================================================================
EXAMPLES
====================================================================

We shall work with the real closure of the ordered field of 
rational numbers.

  Ran := RECLOS(FRAC INT)
    RealClosure Fraction Integer
                              Type: Domain

Some simple signs for square roots, these correspond to an extension
of degree 16 of the rational numbers. Examples provided by J. Abbot.

  fourSquares(a:Ran,b:Ran,c:Ran,d:Ran):Ran==sqrt(a)+sqrt(b)-sqrt(c)-sqrt(d)
                              Type: Void

These produce values very close to zero.

  squareDiff1 := fourSquares(73,548,60,586)
       +---+    +--+    +---+    +--+
    - \|586  - \|60  + \|548  + \|73
                              Type: RealClosure Fraction Integer

  recip(squareDiff1)
             +---+          +--+  +--+         +--+ +---+            +---+
     ((54602\|548  + 149602\|73 )\|60  + 49502\|73 \|548  + 9900895)\|586
   + 
             +--+ +---+             +--+            +---+            +--+
     (154702\|73 \|548  + 30941947)\|60  + 10238421\|548  + 28051871\|73
                              Type: Union(RealClosure Fraction Integer,...)

  sign(squareDiff1)
    1
                              Type: PositiveInteger

  squareDiff2 := fourSquares(165,778,86,990)
       +---+    +--+    +---+    +---+
    - \|990  - \|86  + \|778  + \|165
                              Type: RealClosure Fraction Integer

  recip(squareDiff2)
                +---+           +---+  +--+          +---+ +---+
       ((556778\|778  + 1209010\|165 )\|86  + 401966\|165 \|778  + 144019431)
    *
        +---+
       \|990
   + 
              +---+ +---+              +--+             +---+             +---+
     (1363822\|165 \|778  + 488640503)\|86  + 162460913\|778  + 352774119\|165
                              Type: Union(RealClosure Fraction Integer,...)

  sign(squareDiff2)
    1
                              Type: PositiveInteger

  squareDiff3 := fourSquares(217,708,226,692)
       +---+    +---+    +---+    +---+
    - \|692  - \|226  + \|708  + \|217
                              Type: RealClosure Fraction Integer

  recip(squareDiff3)
               +---+         +---+  +---+         +---+ +---+             +---+
     ((- 34102\|708  - 61598\|217 )\|226  - 34802\|217 \|708  - 13641141)\|692
   + 
              +---+ +---+             +---+            +---+            +---+
     (- 60898\|217 \|708  - 23869841)\|226  - 13486123\|708  - 24359809\|217
                              Type: Union(RealClosure Fraction Integer,...)

  sign(squareDiff3)
    - 1
                              Type: Integer

  squareDiff4 := fourSquares(155,836,162,820)
       +---+    +---+    +---+    +---+
    - \|820  - \|162  + \|836  + \|155
                              Type: RealClosure Fraction Integer

  recip(squareDiff4)
               +---+         +---+  +---+         +---+ +---+             +---+
     ((- 37078\|836  - 86110\|155 )\|162  - 37906\|155 \|836  - 13645107)\|820
   + 
              +---+ +---+             +---+            +---+            +---+
     (- 85282\|155 \|836  - 30699151)\|162  - 13513901\|836  - 31384703\|155
                              Type: Union(RealClosure Fraction Integer,...)

  sign(squareDiff4)
    - 1
                              Type: Integer

  squareDiff5 := fourSquares(591,772,552,818)
       +---+    +---+    +---+    +---+
    - \|818  - \|552  + \|772  + \|591
                              Type: RealClosure Fraction Integer

  recip(squareDiff5)
             +---+         +---+  +---+         +---+ +---+             +---+
     ((70922\|772  + 81058\|591 )\|552  + 68542\|591 \|772  + 46297673)\|818
   + 
            +---+ +---+             +---+            +---+            +---+
     (83438\|591 \|772  + 56359389)\|552  + 47657051\|772  + 54468081\|591
                              Type: Union(RealClosure Fraction Integer,...)

  sign(squareDiff5)
    1
                              Type: PositiveInteger

  squareDiff6 := fourSquares(434,1053,412,1088)
       +----+    +---+    +----+    +---+
    - \|1088  - \|412  + \|1053  + \|434
                              Type: RealClosure Fraction Integer

  recip(squareDiff6)
                +----+          +---+  +---+          +---+ +----+
       ((115442\|1053  + 179818\|434 )\|412  + 112478\|434 \|1053  + 76037291)
    *
        +----+
       \|1088
   + 
           +---+ +----+              +---+            +----+             +---+
   (182782\|434 \|1053  + 123564147)\|412  + 77290639\|1053  + 120391609\|434
                             Type: Union(RealClosure Fraction Integer,...)

  sign(squareDiff6)
    1
                             Type: PositiveInteger

  squareDiff7 := fourSquares(514,1049,446,1152)
       +----+    +---+    +----+    +---+
    - \|1152  - \|446  + \|1049  + \|514
                             Type: RealClosure Fraction Integer

  recip(squareDiff7)
                +----+          +---+  +---+          +---+ +----+
       ((349522\|1049  + 499322\|514 )\|446  + 325582\|514 \|1049  + 239072537)
    *
        +----+
       \|1152
   + 
           +---+ +----+              +---+             +----+             +---+
   (523262\|514 \|1049  + 384227549)\|446  + 250534873\|1049  + 357910443\|514
                             Type: Union(RealClosure Fraction Integer,...)

  sign(squareDiff7)
    1
                             Type: PositiveInteger

  squareDiff8 := fourSquares(190,1751,208,1698)
       +----+    +---+    +----+    +---+
    - \|1698  - \|208  + \|1751  + \|190
                             Type: RealClosure Fraction Integer

  recip(squareDiff8)
                     +----+          +---+  +---+          +---+ +----+
           (- 214702\|1751  - 651782\|190 )\|208  - 224642\|190 \|1751
         + 
           - 129571901
    *
        +----+
       \|1698
   + 
               +---+ +----+              +---+             +----+
     (- 641842\|190 \|1751  - 370209881)\|208  - 127595865\|1751
   + 
                 +---+
     - 387349387\|190
                            Type: Union(RealClosure Fraction Integer,...)

  sign(squareDiff8)
    - 1
                            Type: Integer

This should give three digits of precision

  relativeApprox(squareDiff8,10**(-3))::Float
    - 0.2340527771 5937700123 E -10
                            Type: Float

The sum of these 4 roots is 0

  l := allRootsOf((x**2-2)**2-2)$Ran
    [%A33,%A34,%A35,%A36]
                            Type: List RealClosure Fraction Integer

Check that they are all roots of the same polynomial

  removeDuplicates map(mainDefiningPolynomial,l)
      4     2
    [?  - 4?  + 2]
       Type: List Union(
                   SparseUnivariatePolynomial RealClosure Fraction Integer,
                   "failed")

We can see at a glance that they are separate roots

  map(mainCharacterization,l)
    [[- 2,- 1[,[- 1,0[,[0,1[,[1,2[]
       Type: List Union(
              RightOpenIntervalRootCharacterization(
               RealClosure Fraction Integer,
               SparseUnivariatePolynomial RealClosure Fraction Integer),
              "failed")

Check the sum and product

  [reduce(+,l),reduce(*,l)-2]
    [0,0]
                    Type: List RealClosure Fraction Integer

A more complicated test that involve an extension of degree 256.
This is a way of checking nested radical identities.

  (s2, s5, s10) := (sqrt(2)$Ran, sqrt(5)$Ran, sqrt(10)$Ran)
     +--+
    \|10
                    Type: RealClosure Fraction Integer

  eq1:=sqrt(s10+3)*sqrt(s5+2) - sqrt(s10-3)*sqrt(s5-2) = sqrt(10*s2+10)
       +---------+ +--------+    +---------+ +--------+   +-----------+
       | +--+      | +-+         | +--+      | +-+        |   +-+
    - \|\|10  - 3 \|\|5  - 2  + \|\|10  + 3 \|\|5  + 2 = \|10\|2  + 10
                    Type: Equation RealClosure Fraction Integer

  eq1::Boolean
    true
                    Type: Boolean

  eq2:=sqrt(s5+2)*sqrt(s2+1) - sqrt(s5-2)*sqrt(s2-1) = sqrt(2*s10+2)
       +--------+ +--------+    +--------+ +--------+   +----------+
       | +-+      | +-+         | +-+      | +-+        |  +--+
    - \|\|5  - 2 \|\|2  - 1  + \|\|5  + 2 \|\|2  + 1 = \|2\|10  + 2
                    Type: Equation RealClosure Fraction Integer

  eq2::Boolean
    true
                    Type: Boolean

Some more examples from J. M. Arnaudies

  s3 := sqrt(3)$Ran
     +-+
    \|3
                    Type: RealClosure Fraction Integer

  s7:= sqrt(7)$Ran
     +-+
    \|7
                    Type: RealClosure Fraction Integer

  e1 := sqrt(2*s7-3*s3,3)
     +-------------+
    3|  +-+     +-+
    \|2\|7  - 3\|3
                    Type: RealClosure Fraction Integer

  e2 := sqrt(2*s7+3*s3,3)
     +-------------+
    3|  +-+     +-+
    \|2\|7  + 3\|3
                    Type: RealClosure Fraction Integer

This should be null

  e2-e1-s3
    0
                    Type: RealClosure Fraction Integer

A quartic polynomial

  pol : UP(x,Ran) := x**4+(7/3)*x**2+30*x-(100/3)
     4   7  2         100
    x  + - x  + 30x - ---
         3             3
                  Type: UnivariatePolynomial(x,RealClosure Fraction Integer)

Add some cubic roots

  r1 := sqrt(7633)$Ran
     +----+
    \|7633
                        Type: RealClosure Fraction Integer

  alpha := sqrt(5*r1-436,3)/3
       +--------------+
    1 3|  +----+
    - \|5\|7633  - 436
    3
                        Type: RealClosure Fraction Integer

  beta := -sqrt(5*r1+436,3)/3 
         +--------------+
      1 3|  +----+
    - - \|5\|7633  + 436
      3
                        Type: RealClosure Fraction Integer

this should be null

  pol.(alpha+beta-1/3)
    0
                        Type: RealClosure Fraction Integer

A quintic polynomial

  qol : UP(x,Ran) := x**5+10*x**3+20*x+22
     5      3
    x  + 10x  + 20x + 22
              Type: UnivariatePolynomial(x,RealClosure Fraction Integer)

Add some cubic roots

  r2 := sqrt(153)$Ran
     +---+
    \|153
                          Type: RealClosure Fraction Integer

  alpha2 := sqrt(r2-11,5)
     +-----------+
    5| +---+
    \|\|153  - 11
                          Type: RealClosure Fraction Integer

  beta2 := -sqrt(r2+11,5)
       +-----------+
      5| +---+
    - \|\|153  + 11
                          Type: RealClosure Fraction Integer

this should be null

  qol(alpha2+beta2)
    0
                          Type: RealClosure Fraction Integer

Finally, some examples from the book Computer Algebra by Davenport,
Siret and Tournier (page 77).  The last one is due to Ramanujan.

  dst1:=sqrt(9+4*s2)=1+2*s2
     +---------+
     |  +-+         +-+
    \|4\|2  + 9 = 2\|2  + 1
                          Type: Equation RealClosure Fraction Integer

  dst1::Boolean
    true
                          Type: Boolean

  s6:Ran:=sqrt 6
     +-+
    \|6
                          Type: RealClosure Fraction Integer

  dst2:=sqrt(5+2*s6)+sqrt(5-2*s6) = 2*s3
     +-----------+    +---------+
     |    +-+         |  +-+         +-+
    \|- 2\|6  + 5  + \|2\|6  + 5 = 2\|3
                          Type: Equation RealClosure Fraction Integer

  dst2::Boolean
    true
                          Type: Boolean

  s29:Ran:=sqrt 29
     +--+
    \|29
                          Type: RealClosure Fraction Integer

  dst4:=sqrt(16-2*s29+2*sqrt(55-10*s29)) = sqrt(22+2*s5)-sqrt(11+2*s29)+s5
    +--------------------------------+
    |  +--------------+                    +-----------+    +----------+
    |  |     +--+           +--+           |  +--+          |  +-+          +-+
   \|2\|- 10\|29  + 55  - 2\|29  + 16 = - \|2\|29  + 11  + \|2\|5  + 22  + \|5
                          Type: Equation RealClosure Fraction Integer

  dst4::Boolean
    true
                          Type: Boolean

  dst6:=sqrt((112+70*s2)+(46+34*s2)*s5) = (5+4*s2)+(3+s2)*s5 
     +--------------------------------+
     |    +-+       +-+      +-+           +-+      +-+     +-+
    \|(34\|2  + 46)\|5  + 70\|2  + 112 = (\|2  + 3)\|5  + 4\|2  + 5
                          Type: Equation RealClosure Fraction Integer

  dst6::Boolean
    true
                          Type: Boolean

  f3:Ran:=sqrt(3,5)
    5+-+
    \|3
                          Type: RealClosure Fraction Integer

  f25:Ran:=sqrt(1/25,5)
     +--+
     | 1
    5|--
    \|25
                          Type: RealClosure Fraction Integer

  f32:Ran:=sqrt(32/5,5)
     +--+
     |32
    5|--
    \| 5
                          Type: RealClosure Fraction Integer

  f27:Ran:=sqrt(27/5,5)
     +--+
     |27
    5|--
    \| 5
                          Type: RealClosure Fraction Integer

  dst5:=sqrt((f32-f27,3)) = f25*(1+f3-f3**2)
     +---------------+
     |   +--+    +--+                         +--+
     |   |27     |32       5+-+2   5+-+       | 1
    3|- 5|--  + 5|--  = (- \|3   + \|3  + 1) 5|--
    \|  \| 5    \| 5                         \|25
                          Type: Equation RealClosure Fraction Integer

  dst5::Boolean
    true
                          Type: Boolean

See Also:
o )help RightOpenIntervalRootCharacterization
o )help RealClosedField
o )help RealRootCharacterizationCategory
o )help UnivariatePolynomialCategory
o )help Field
o )help RealPolynomialUtilitiesPackage
o )show RealClosure

