/usr/lib/open-axiom/input/reclos.input is in open-axiom-test 1.5.0~svn3056+ds-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | -- 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
|