1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
\documentclass{article}
\usepackage{axiom}
\begin{document}
\title{\$SPAD/src/input RECLOS.input}
\author{The Axiom Team}
\maketitle
\begin{abstract}
\end{abstract}
\eject
\tableofcontents
\eject
This input file was updated by Renaud Rioboo in January 2004
<<*>>=
-- Input generated from RealClosureXmpPage
)clear all
Ran := RECLOS(FRAC INT)
--
-- Some simple signs for square roots, these correspond to an extension
-- of degree 16 of the rational numbers.
-- these examples were given to me by J. Abbot
--
fourSquares(a:Ran,b:Ran,c:Ran,d:Ran):Ran == sqrt(a)+sqrt(b) - sqrt(c)-sqrt(d)
squareDiff1 := fourSquares(73,548,60,586)
recip(squareDiff1)
sign(squareDiff1)
squareDiff2 := fourSquares(165,778,86,990)
recip(squareDiff2)
sign(squareDiff2)
squareDiff3 := fourSquares(217,708,226,692)
recip(squareDiff3)
sign(squareDiff3)
squareDiff4 := fourSquares(155,836,162,820)
recip(squareDiff4)
sign(squareDiff4)
squareDiff5 := fourSquares(591,772,552,818)
recip(squareDiff5)
sign(squareDiff5)
squareDiff6 := fourSquares(434,1053,412,1088)
recip(squareDiff6)
sign(squareDiff6)
squareDiff7 := fourSquares(514,1049,446,1152)
recip(squareDiff7)
sign(squareDiff7)
squareDiff8 := fourSquares(190,1751,208,1698)
recip(squareDiff8)
sign(squareDiff8)
relativeApprox(squareDiff8,10**(-3))::Float
--
-- test the Renaud Rioboo fix (Jan 2004)
--
allRootsOf((x-2)*(x-3)*(x-4))$RECLOS(FRAC INT)
--
-- check out if the sum of all roots is null
-- example from P.V. Koseleff
--
l := allRootsOf((x**2-2)**2-2)$Ran
l.1+l.2+l.3+l.4
removeDuplicates map(mainDefiningPolynomial,l)
map(mainCharacterization,l)
[reduce(+,l),reduce(*,l)-2]
--
-- a more complicated test that involve an extension of degree 256
-- example by prof Kahan at ISSAC'92
--
)cl prop s2 s5 10
(s2, s5, s10) := (sqrt(2)$Ran, sqrt(5)$Ran, sqrt(10)$Ran)
eq1:=sqrt(s10+3)*sqrt(s5+2) - sqrt(s10-3)*sqrt(s5-2) = sqrt(10*s2+10)
eq1::Boolean
--
-- analogous one by [rr]
--
eq2:=sqrt(s5+2)*sqrt(s2+1) - sqrt(s5-2)*sqrt(s2-1) = sqrt(2*s10+2)
eq2::Boolean
--
-- these came from J.M. Arnaudies
--
)cl prop s4 s7 e1 e2
s3 := sqrt(3)$Ran
s7:= sqrt(7)$Ran
e1 := sqrt(2*s7-3*s3,3)
e2 := sqrt(2*s7+3*s3,3)
-- this should be null
ee1:=e2-e1=s3
ee1::Boolean
)cl prop pol r1 alpha beta
pol : UP(x,Ran) := x**4+(7/3)*x**2+30*x-(100/3)
r1 := sqrt(7633)$Ran
-- cubic roots
alpha := sqrt(5*r1-436,3)/3
beta := -sqrt(5*r1+436,3)/3
-- this should be null
pol.(alpha+beta-1/3)
)cl prop qol r2 alpha beta
r2 := sqrt(153)$Ran
-- roots of order 5
alpha2 := sqrt(r2-11,5)
beta2 := -sqrt(r2+11,5)
qol : UP(x,Ran) := x**5+10*x**3+20*x+22
qol(alpha2+beta2)
dst1:=sqrt(9+4*s2)=1+2*s2
dst1::Boolean
s6:Ran:=sqrt 6
dst2:=sqrt(5+2*s6)+sqrt(5-2*s6) = 2*s3
dst2::Boolean
s29:Ran:=sqrt 29
dst4:=sqrt(16-2*s29+2*sqrt(55-10*s29)) = sqrt(22+2*s5)-sqrt(11+2*s29)+s5
dst4::Boolean
dst6:=sqrt((112+70*s2)+(46+34*s2)*s5) = (5+4*s2)+(3+s2)*s5
dst6::Boolean
f3:Ran:=sqrt(3,5)
f25:Ran:=sqrt(1/25,5)
f32:Ran:=sqrt(32/5,5)
f27:Ran:=sqrt(27/5,5)
dst5:=sqrt((f32-f27,3)) = f25*(1+f3-f3**2)
dst5::Boolean
@
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
\end{thebibliography}
\end{document}
|
