1
2
3accPolyC14 = <float64ne> (_accPolyC14);
4accPolyC13 = <float64ne> (_accPolyC13);
5accPolyC12 = <float64ne> (_accPolyC12);
6accPolyC11 = <float64ne> (_accPolyC11);
7accPolyC10 = <float64ne> (_accPolyC10);
8
9accPolyC9h = <float64ne> (_accPolyC9h);
10accPolyC9l = <float64ne> (_accPolyC9l);
11AccPolyC9hl = accPolyC9h + accPolyC9l; #MAPLE
12accPolyC8h = <float64ne> (_accPolyC8h);
13accPolyC8l = <float64ne> (_accPolyC8l);
14AccPolyC8hl = accPolyC8h + accPolyC8l; #MAPLE
15accPolyC7h = <float64ne> (_accPolyC7h);
16accPolyC7l = <float64ne> (_accPolyC7l);
17AccPolyC7hl = accPolyC7h + accPolyC7l; #MAPLE
18accPolyC6h = <float64ne> (_accPolyC6h);
19accPolyC6l = <float64ne> (_accPolyC6l);
20AccPolyC6hl = accPolyC6h + accPolyC6l; #MAPLE
21accPolyC5h = <float64ne> (_accPolyC5h);
22accPolyC5l = <float64ne> (_accPolyC5l);
23AccPolyC5hl = accPolyC5h + accPolyC5l; #MAPLE
24accPolyC4h = <float64ne> (_accPolyC4h);
25accPolyC4l = <float64ne> (_accPolyC4l);
26AccPolyC4hl = accPolyC4h + accPolyC4l; #MAPLE
27accPolyC3h = <float64ne> (_accPolyC3h);
28accPolyC3l = <float64ne> (_accPolyC3l);
29AccPolyC3hl = accPolyC3h + accPolyC3l; #MAPLE
30
31E = 0; #MAPLE
32
33zh = <float64ne> (Z);
34zl = Z - zh; #MAPLE
35
36highPoly <float64ne> = accPolyC10 + zh * (accPolyC11 + zh * (accPolyC12 + zh * (accPolyC13 + zh * accPolyC14)));
37
38T1hl = zh * highPoly; #MAPLE
39
40T2 = AccPolyC9hl + T1hl; #MAPLE
41T3 = Z * T2hl; #MAPLE
42T4 = AccPolyC8hl + T3hl; #MAPLE
43T5 = Z * T4hl; #MAPLE
44T6 = AccPolyC7hl + T5hl; #MAPLE
45T7 = Z * T6hl; #MAPLE
46T8 = AccPolyC6hl + T7hl; #MAPLE
47T9 = Z * T8hl; #MAPLE
48T10 = AccPolyC5hl + T9hl; #MAPLE
49T11 = Z * T10hl; #MAPLE
50T12 = AccPolyC4hl + T11hl; #MAPLE
51T13 = Z * T12hl; #MAPLE
52T14 = AccPolyC3hl + T13hl; #MAPLE
53
54
55ZSquare = Z * Z; #MAPLE
56ZCube = Z * ZSquarehml; #MAPLE
57HigherPolyMultZ = T14hl * ZCubehml; #MAPLE
58ZSquareHalfhml = -0.5 * ZSquarehml; #MAPLE
59PolyWithSquare = ZSquareHalfhml + HigherPolyMultZhml; #MAPLE
60Poly = Z + PolyWithSquarehml; #MAPLE
61
62#We can simplify the proof in this case since we know that adding a triple double which is
63#equal to 0 exactly is exact.
64
65Loghml = Polyhml; #MAPLE
66
67
68#Mathematical definition of the logarithm
69
70MHighPoly = accPolyC10 + Z * (accPolyC11 + Z * (accPolyC12 + Z * (accPolyC13 + Z * accPolyC14))); #MAPLE
71MT1 = Z * MHighPoly; #MAPLE
72MT2 = AccPolyC9hl + MT1; #MAPLE
73MT3 = Z * MT2; #MAPLE
74MT4 = AccPolyC8hl + MT3; #MAPLE
75MT5 = Z * MT4; #MAPLE
76MT6 = AccPolyC7hl + MT5; #MAPLE
77MT7 = Z * MT6; #MAPLE
78MT8 = AccPolyC6hl + MT7; #MAPLE
79MT9 = Z * MT8; #MAPLE
80MT10 = AccPolyC5hl + MT9; #MAPLE
81MT11 = Z * MT10; #MAPLE
82MT12 = AccPolyC4hl + MT11; #MAPLE
83MT13 = Z * MT12; #MAPLE
84MT14 = AccPolyC3hl + MT13; #MAPLE
85MZSquare = Z * Z; #MAPLE
86MZCube = Z * MZSquare; #MAPLE
87MHigherPolyMultZ = MT14 * MZCube; #MAPLE
88MZSquareHalf = -0.5 * MZSquare; #MAPLE
89MPolyWithSquare = MZSquareHalf + MHigherPolyMultZ; #MAPLE
90MPoly = Z + MPolyWithSquare; #MAPLE
91
92#We apply the same simplification here
93
94MLog = MLog1pZ; #MAPLE
95
96
97#Useful additional definitions
98
99epsilon1 = (highPoly - MHighPoly) / MHighPoly; #MAPLE
100epsilon2 = (T1hl - MT1) / MT1; #MAPLE
101epsilon3 = (T2hl - MT2) / MT2; #MAPLE
102epsilon4 = (T3hl - MT3) / MT3; #MAPLE
103epsilon5 = (T4hl - MT4) / MT4; #MAPLE
104epsilon6 = (T5hl - MT5) / MT5; #MAPLE
105epsilon7 = (T6hl - MT6) / MT6; #MAPLE
106epsilon8 = (T7hl - MT7) / MT7; #MAPLE
107epsilon9 = (T8hl - MT8) / MT8; #MAPLE
108epsilon10 = (T9hl - MT9) / MT9; #MAPLE
109epsilon11 = (T10hl - MT10) / MT10; #MAPLE
110epsilon12 = (T11hl - MT11) / MT11; #MAPLE
111epsilon13 = (T12hl - MT12) / MT12; #MAPLE
112epsilon14 = (T13hl - MT13) / MT13; #MAPLE
113epsilon15 = (T14hl - MT14) / MT14; #MAPLE
114
115epsilon16 = (ZCubehml - MZCube) / MZCube; #MAPLE
116epsilon17 = (HigherPolyMultZhml - MHigherPolyMultZ) / MHigherPolyMultZ; #MAPLE
117epsilon18 = (ZSquareHalfhml - MZSquareHalf) / MZSquareHalf; #MAPLE
118epsilon19 = (PolyWithSquarehml - MPolyWithSquare) / MPolyWithSquare; #MAPLE
119epsilon20 = (Polyhml - MLog1pZ) / MLog1pZ; #MAPLE
120
121epsilon21 = (PolyWithSquare - MPolyWithSquare) / MPolyWithSquare; #MAPLE
122epsilon22 = (Polyhml - MPoly) / MPoly; #MAPLE
123epsilon23 = (Poly - MPoly) / MPoly; #MAPLE
124
125aux1 = -0.5 * Z + MZSquare * MT14; #MAPLE
126
127
128#End additional definitions
129
130{
131(
132(T2hl - T2) / T2 in [-1b-103,1b-103]
133/\ (T3hl - T3) / T3 in [-1b-102,1b-102]
134/\ (T4hl - T4) / T4 in [-1b-103,1b-103]
135/\ (T5hl - T5) / T5 in [-1b-102,1b-102]
136/\ (T6hl - T6) / T6 in [-1b-103,1b-103]
137/\ (T7hl - T7) / T7 in [-1b-102,1b-102]
138/\ (T8hl - T8) / T8 in [-1b-103,1b-103]
139/\ (T9hl - T9) / T9 in [-1b-102,1b-102]
140/\ (T10hl - T10) / T10 in [-1b-103,1b-103]
141/\ (T11hl - T11) / T11 in [-1b-102,1b-102]
142/\ (T12hl - T12) / T12 in [-1b-103,1b-103]
143/\ (T13hl - T13) / T13 in [-1b-102,1b-102]
144/\ (T14hl - T14) / T14 in [-1b-103,1b-103]
145/\ (ZSquarehml - ZSquare) / ZSquare in [-1b-149,1b-149]
146/\ (ZCubehml - ZCube) / ZCube in [-1b-144,1b-144]
147/\ (HigherPolyMultZhml - HigherPolyMultZ) / HigherPolyMultZ in [-1b-141,1b-141]
148/\ (PolyWithSquarehml - PolyWithSquare) / PolyWithSquare in [-1b-137,1b-137]
149/\ (Polyhml - Poly) / Poly in [-1b-134,1b-134]
150/\ (MPoly - MLog1pZ) / MLog1pZ in [-_epsilonApproxAccurate,_epsilonApproxAccurate]
151/\ Z in [1b-900,_zmax]
152/\ ((logh + logm + logl) - Loghml) / Loghml in [-1b-159,1b-159]
153->
154((logh + logm + logl) - MLog) / MLog in [-5735b-132,5735b-132]
155)
156/\
157(
158(T2hl - T2) / T2 in [-1b-103,1b-103]
159/\ (T3hl - T3) / T3 in [-1b-102,1b-102]
160/\ (T4hl - T4) / T4 in [-1b-103,1b-103]
161/\ (T5hl - T5) / T5 in [-1b-102,1b-102]
162/\ (T6hl - T6) / T6 in [-1b-103,1b-103]
163/\ (T7hl - T7) / T7 in [-1b-102,1b-102]
164/\ (T8hl - T8) / T8 in [-1b-103,1b-103]
165/\ (T9hl - T9) / T9 in [-1b-102,1b-102]
166/\ (T10hl - T10) / T10 in [-1b-103,1b-103]
167/\ (T11hl - T11) / T11 in [-1b-102,1b-102]
168/\ (T12hl - T12) / T12 in [-1b-103,1b-103]
169/\ (T13hl - T13) / T13 in [-1b-102,1b-102]
170/\ (T14hl - T14) / T14 in [-1b-103,1b-103]
171/\ (ZSquarehml - ZSquare) / ZSquare in [-1b-149,1b-149]
172/\ (ZCubehml - ZCube) / ZCube in [-1b-144,1b-144]
173/\ (HigherPolyMultZhml - HigherPolyMultZ) / HigherPolyMultZ in [-1b-141,1b-141]
174/\ (PolyWithSquarehml - PolyWithSquare) / PolyWithSquare in [-1b-137,1b-137]
175/\ (Polyhml - Poly) / Poly in [-1b-134,1b-134]
176/\ (MPoly - MLog1pZ) / MLog1pZ in [-_epsilonApproxAccurate,_epsilonApproxAccurate]
177/\ Z in [_zmin,-1b-900]
178/\ ((logh + logm + logl) - Loghml) / Loghml in [-1b-159,1b-159]
179->
180((logh + logm + logl) - MLog) / MLog in [-5735b-132,5735b-132]
181)
182}
183
184((logh + logm + logl) - MLog) / MLog -> ((Loghml - MLog) / MLog) + ((((logh + logm + logl) - Loghml) / Loghml) * (((Loghml - MLog) / MLog) + 1));
185
186T2hl -> (T2 * ((T2hl - T2) / T2)) + T2;
187T3hl -> (T3 * ((T3hl - T3) / T3)) + T3;
188T4hl -> (T4 * ((T4hl - T4) / T4)) + T4;
189T5hl -> (T5 * ((T5hl - T5) / T5)) + T5;
190T6hl -> (T6 * ((T6hl - T6) / T6)) + T6;
191T7hl -> (T7 * ((T7hl - T7) / T7)) + T7;
192T8hl -> (T8 * ((T8hl - T8) / T8)) + T8;
193T9hl -> (T9 * ((T9hl - T9) / T9)) + T9;
194T10hl -> (T10 * ((T10hl - T10) / T10)) + T10;
195T11hl -> (T11 * ((T11hl - T11) / T11)) + T11;
196T12hl -> (T12 * ((T12hl - T12) / T12)) + T12;
197T13hl -> (T13 * ((T13hl - T13) / T13)) + T13;
198T14hl -> (T14 * ((T14hl - T14) / T14)) + T14;
199
200
201ZSquarehml -> (ZSquare * ((ZSquarehml - ZSquare) / ZSquare)) + ZSquare;
202ZCubehml -> (ZCube * ((ZCubehml - ZCube) / ZCube)) + ZCube;
203HigherPolyMultZhml -> (HigherPolyMultZ * ((HigherPolyMultZhml - HigherPolyMultZ) / HigherPolyMultZ)) + HigherPolyMultZ;
204PolyWithSquarehml -> (PolyWithSquare * ((PolyWithSquarehml - PolyWithSquare) / PolyWithSquare)) + PolyWithSquare;
205Polyhml -> (Poly * ((Polyhml - Poly) / Poly)) + Poly;
206
207
208epsilon2 -> epsilon1 + (((zh - Z) / Z) * (epsilon1 + 1));
209epsilon3 -> ((epsilon2 * MT1) / (AccPolyC9hl + MT1)) + (((AccPolyC9hl + T1hl) / (AccPolyC9hl + MT1)) * ((T2hl - T2) / T2));
210epsilon4 -> epsilon3 + (((T3hl - T3) / T3) * (epsilon3 + 1));
211epsilon5 -> ((epsilon4 * MT3) / (AccPolyC8hl + MT3)) + (((AccPolyC8hl + T3hl) / (AccPolyC8hl + MT3)) * ((T4hl - T4) / T4));
212epsilon6 -> epsilon5 + (((T5hl - T5) / T5) * (epsilon5 + 1));
213epsilon7 -> ((epsilon6 * MT5) / (AccPolyC7hl + MT5)) + (((AccPolyC7hl + T5hl) / (AccPolyC7hl + MT5)) * ((T6hl - T6) / T6));
214epsilon8 -> epsilon7 + (((T7hl - T7) / T7) * (epsilon7 + 1));
215epsilon9 -> ((epsilon8 * MT7) / (AccPolyC6hl + MT7)) + (((AccPolyC6hl + T7hl) / (AccPolyC6hl + MT7)) * ((T8hl - T8) / T8));
216epsilon10 -> epsilon9 + (((T9hl - T9) / T9) * (epsilon9 + 1));
217epsilon11 -> ((epsilon10 * MT9) / (AccPolyC5hl + MT9)) + (((AccPolyC5hl + T9hl) / (AccPolyC5hl + MT9)) * ((T10hl - T10) / T10));
218epsilon12 -> epsilon11 + (((T11hl - T11) / T11) * (epsilon11 + 1));
219epsilon13 -> ((epsilon12 * MT11) / (AccPolyC4hl + MT11)) + (((AccPolyC4hl + T11hl) / (AccPolyC4hl + MT11)) * ((T12hl - T12) / T12));
220epsilon14 -> epsilon13 + (((T13hl - T13) / T13) * (epsilon13 + 1));
221epsilon15 -> ((epsilon14 * MT13) / (AccPolyC3hl + MT13)) + (((AccPolyC3hl + T13hl) / (AccPolyC3hl + MT13)) * ((T14hl - T14) / T14));
222epsilon16 -> ((ZSquarehml - MZSquare) / MZSquare) + (((ZCubehml - ZCube) / ZCube) * (((ZSquarehml - MZSquare) / MZSquare) + 1));
223epsilon17 -> epsilon15 + epsilon16 + epsilon15 * epsilon16 +
224((HigherPolyMultZhml - HigherPolyMultZ) / HigherPolyMultZ) * (1 + epsilon15 + epsilon16 + epsilon15 * epsilon16);
225epsilon18 -> (ZSquarehml - MZSquare) / MZSquare;
226epsilon19 -> epsilon21 + (1 + epsilon21) * ((PolyWithSquarehml - PolyWithSquare) / PolyWithSquare);
227epsilon20 -> (((Polyhml - MPoly) / MPoly) + ((MPoly - MLog1pZ) / MLog1pZ)) + (((Polyhml - MPoly) / MPoly) * ((MPoly - MLog1pZ) / MLog1pZ));
228epsilon21 -> ((-0.5 * epsilon18) + (Z * MT14 * epsilon17)) / (-0.5 + (Z * MT14));
229epsilon22 -> epsilon23 + (((Polyhml - Poly) / Poly) * (1+ epsilon23));
230epsilon23 -> epsilon19 * (aux1 / (1 + aux1));
231