/usr/lib/open-axiom/input/realclos.input is in open-axiom-test 1.4.1+svn~2626-2ubuntu2.
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 | )clear all
-- computing without a table manipulation when creating objects
Ran := RECLOS(FRAC INT)
-- Some simple signs for square roots, these correspond to an extension
-- of degree 16 of the rational numbers.
fourSquares(a:Ran,b:Ran,c:Ran,d:Ran):Ran ==
sqrt(a)+sqrt(b) - sqrt(c)-sqrt(d)
squareDiff := fourSquares(73,548,60,586)
recip(squareDiff)
sign(squareDiff)
squareDiff := fourSquares(165,778,86,990)
recip(squareDiff)
sign(squareDiff)
squareDiff := fourSquares(217,708,226,692)
recip(squareDiff)
sign(squareDiff)
squareDiff := fourSquares(155,836,162,820)
recip(squareDiff)
sign(squareDiff)
squareDiff := fourSquares(591,772,552,818)
recip(squareDiff)
sign(squareDiff)
squareDiff := fourSquares(434,1053,412,1088)
recip(squareDiff)
sign(squareDiff)
squareDiff := fourSquares(514,1049,446,1152)
recip(squareDiff)
sign(squareDiff)
squareDiff := fourSquares(190,1751,208,1698)
recip(squareDiff)
sign(squareDiff)
)cl prop s2 s5 s10 l
-- a more complicated test that involve an extension of degree 256
(s2, s5, s10) := (sqrt(2)$Ran, sqrt(5)$Ran, sqrt(10)$Ran);
sqrt(s10+3)*sqrt(s5+2) - sqrt(s10-3)*sqrt(s5-2) = sqrt(10*s2+10)
%::Boolean
-- the sum of these 4 numbers is 0
l := allRootsOf((x^2-2)^2-2)$Ran
l.1+l.2+l.3+l.4
|