This file is indexed.

/usr/lib/open-axiom/input/realclos.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
)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