1 (* This file is a continuation of kep_inequalities.ml.
\r
2 It contains the inequalities related to quad clusters.
\r
3 It also contains some particularly long, tricky, or high-dimensional verifications *)
\r
7 (* ----------------------------------------------------------------------- *)
\r
11 \section{Notes on Interval Verifications}
\r
12 %{Appendix 2. Interval Verifications}
\r
13 \label{sec:verification-notes}
\r
15 We make a few remarks in this appendix on the verification of the
\r
16 inequalities of Proposition~\ref{calc:quad-bounds} and \ref{calc:d(R)}.
\r
17 The basic method in proving an inequality $f(x)<0$ for $x\in C$, is to
\r
18 use computer-based interval arithmetic to obtain rigorous upper bounds
\r
19 on the second derivatives: $|f_{ij}(x)|\le a_{ij}$, for $x\in C$. These
\r
20 bounds lead immediately to upper bounds on $f(x)$ through a Taylor
\r
21 approximation with explicit bounds on the error. We divide the domain
\r
22 $C$ as necessary until the Taylor approximation on each piece is less
\r
23 that the desired bound.
\r
25 Some of the inequalities involve as many as $12$ variables, such as the
\r
26 octahedral cases of Lemma~\ref{calc:d(R)}. These are not directly
\r
27 accessible by computer. We describe some reductions we have used, based
\r
28 on linear programming. We start by applying the dimension reduction
\r
29 techniques described in~\cite[Sec.~8.7]{part1}. We have used these
\r
32 We will describe Lemma~\ref{calc:d(R)} because in various respects these
\r
33 inequalities have been the most difficult to prove, although the
\r
34 verifications of Lemmas~\ref{calc:quad-bounds} and \ref{lemma:1.153} are
\r
35 quite similar. If there is a diagonal of length $\le2\sqrt{2}$, we have
\r
36 two flat quarters $S_1$ and $S_2$. The score breaks up into
\r
37 $\sigma=\sigma(S_1)+\sigma(S_2)$. The simplices $S_1$ and
\r
38 $S_2$ share a three-dimensional face. The inequality we wish to prove
\r
40 $$\sigma \le a(\dih(S_1)+\dih_2(S_1)+\dih_2(S_2))+b.$$
\r
41 We break the shared face into smaller domains on which we have
\r
44 \sigma(S_1)&\le a (\dih(S_1)+\dih_2(S_1)) + b_1,\\
\r
45 \sigma(S_2)&\le a \dih_2(S_1) + b_2,\\
\r
48 for some $b_1,b_2$ satisfying $b_1+b_2\le b$. These inequalities are
\r
49 six-dimensional verifications.
\r
51 If the quad cluster is an octahedron with upright diagonal, there are
\r
52 four upright quarters $S_1,\ldots,S_4$. We consider inequalities of the
\r
55 \sigma(S_i)\le \sum _{j\ne 4} a_j^i y_j(S_i)
\r
56 + a_7 (\dih_1(S_i)-\pi/2) + \sum_{j=2}^3 a \epsilon^i_j \dih_j(S_i)
\r
60 If $\sum_{i=1}^4 a_j^i \le0$, $j\ne 4$, and $\sum_i b^i\le b$, then for
\r
61 appropriate $\epsilon^i_j\in\{0,1\}$, these inequalities imply the full
\r
62 inequality for octahedral quad clusters.
\r
64 By linear programming techniques, we were able to divide the domain of
\r
65 all octahedra into about $1200$ pieces and find inequalities of this
\r
66 form on each piece, giving an explicit list of inequalities that imply
\r
67 Lemma~\ref{calc:d(R)}. The inequalities involve six variables and were
\r
68 verified by interval arithmetic.
\r
70 To find the optimal coefficients $a_j^i$ by linear programming we pose
\r
76 &\quad X_i,\quad i=1,2,3,4, \ \{S_1,S_2,S_3,S_4\}\in C\\
\r
77 &\quad\sum_i a_j^i \le 0,\\
\r
78 &\quad\sum_i b^i \le b,
\r
81 where $\{S_1,S_2,S_3,S_4\}$ runs over all octahedra in a given domain
\r
82 $C$. The nonlinear inequalities~\ref{eqn:Xi} are to be regarded as
\r
83 linear conditions on the coefficients $a_j^i$, $b^i$, etc. The nonlinear
\r
84 functions $\sigma(S_i),\dih(S_i)$, $y_j(S_i)$ are to be regarded as the
\r
85 coefficients of the variables $a_j^i,\ldots$ in a system of linear
\r
86 inequalities. There are infinitely many constraints, because the set
\r
87 $C$ of octahedra is infinite. In practice we approximate $C$ by a large
\r
88 finite set. If the maximum of $t$ is positive, then we have a
\r
89 collection of inequalities in small dimensions that imply the inequality
\r
90 for octahedral quad clusters. Otherwise, we subdivide $C$ into smaller
\r
91 domains and try again. Eventually, we succeed in partitioning the
\r
92 problem into six-dimensional pieces, which were verified by interval
\r
96 If the quad cluster is a mixed case, then Lemma~\ref{lemma:1.04} gives
\r
97 $$\sigma\le \vor_0, -1.04\,\pt,$$ so also
\r
98 $$\sigma \le \frac{3}{4}\vor_0 + \frac{1}{4} (-1.04\,\pt).$$
\r
99 In the pure Voronoi case with no quarters and no enclosed vertices, we
\r
100 have the approximation
\r
101 $$\sigma \le \vor(\cdot,\sqrt2) \le \vor_0.$$
\r
102 If we prove $\vor_0\le a (\dih_1+\dih_2) + b$, the mixed case is
\r
103 established. This is how the first of the Inequalities~\ref{calc:d(R)}
\r
104 was established. Dimension reduction reduces this to a seven-dimensional
\r
105 verification. We draw the shorter of the two diagonals between corners
\r
106 of the quad cluster. As we begin to subdivide this seven-dimensional
\r
107 domain, we are able to separate the quad cluster into two simplices
\r
108 along the diagonal, each scored by $\vor_0$. This reduces the dimension
\r
109 further, to make it accessible. The two last two cases of
\r
110 Inequality~\ref{calc:d(R)}, are similar, but we establish the
\r
114 \frac{3}{4}\vor_0 + \frac{1}{4} (-1.04\,\pt) &\le a (\dih_1+\dih_2) + b,\\
\r
115 \vor(\cdot,\sqrt2)&\le a (\dih_1+\dih_2) + b.
\r
118 This completes our sketch of how the verifications were made.
\r
124 (* now we can list inequalities *)
\r
126 (* SPIII-1998 Lemma 4.1 *)
\r
129 let J_310151857 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
130 ((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&57906)/(&10000)
\r
131 + ((&456766)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
132 let J_655029773 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
133 ((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&20749)/(&10000)
\r
134 + ((&15094)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
135 let J_73283761 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
136 ((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&8341)/(&10000)
\r
137 + ((&5301)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
138 let J_15141595 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
139 ((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&6284)/(&10000)
\r
140 + ((&3878)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
141 let J_574391221 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
142 ((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&4124)/(&10000)
\r
143 - ((&1897)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
144 let J_396281725 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
145 ((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&15707)/(&10000)
\r
146 - ((&5905)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
147 let J_166451608 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
148 ((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&41717)/(&100000)
\r
149 - ((&3)/(&10))*(solid_area_quad_v v0 v1 v2 v3 v4)))`);;
\r
150 let J_539320075 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
151 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&581446)/(&100000)
\r
152 + ((&449461)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
153 let J_122375455 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
154 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&2955)/(&1000)
\r
155 + ((&21406)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
156 let J_408478278 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
157 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&6438)/(&10000)
\r
158 + ((&316)/(&1000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
159 let J_996268658 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
160 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&1317)/(&10000)))`);;
\r
161 let J_393682353 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
162 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < (&3825)/(&10000)
\r
163 - ((&2365)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
164 let J_775642319 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
165 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < (&1071)/(&1000)
\r
166 - ((&4747)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
167 let J_616145964 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
168 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10))) <
\r
169 --(&577942)/(&100000)
\r
170 + ((&425863)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;
\r
171 let J_153920401 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
172 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <
\r
174 + ((&35294)/(&10000))*(dih_or_v v0 v1 v2 v4))))`);;
\r
175 let J_337637212 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
176 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <
\r
177 --(&4126)/(&10000))))`);;
\r
178 let J_768057794 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
179 ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <
\r
181 - ((&316)/(&1000))*(dih_or_v v0 v1 v2 v4))))`);;
\r
182 let J_465497818 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
183 ((sigma_quad_approx1 v0 v1 v2 v3 v4 <
\r
184 -- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)
\r
185 - (&5350181)/(&1000000)
\r
186 + ((&4611391)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;
\r
187 let J_18502666 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
188 ((sigma_quad_approx1 v0 v1 v2 v3 v4 <
\r
189 -- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)
\r
190 - (&166174)/(&100000)
\r
191 + ((&1582508)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;
\r
192 let J_676439533 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
193 ((sigma_quad_approx1 v0 v1 v2 v3 v4 <
\r
194 -- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)
\r
196 + ((&342747)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;
\r
197 let J_974296985 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
198 ((sigma_quad_approx1 v0 v1 v2 v3 v4 <
\r
199 -- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)
\r
200 + (&336909)/(&100000)
\r
201 - ((&974137)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;
\r
203 let C_940884472 = list_mk_conj[
\r
227 (* SPIII-1998 Lemma 4.2 *)
\r
229 let J_322621318 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
230 ((sigma_quad_approx1 v0 v1 v2 v3 v4 <
\r
232 + ((&30508)/(&100000))*
\r
233 ((dih_or_v v0 v1 v2 v4)+
\r
234 (dih_or_v v0 v2 v3 v1)))))`);;
\r
235 let J_444643063 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
236 ((sigma_quad_approx1 v0 v1 v2 v3 v4 <
\r
237 -- (&10472)/(&100000)
\r
238 + ((&27605)/(&100000))*
\r
239 ((dih_or_v v0 v1 v2 v4)+
\r
240 (dih_or_v v0 v2 v3 v1)))))`);;
\r
241 let J_552698390 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
242 ((sigma_quad_approx1 v0 v1 v2 v3 v4 <
\r
244 - ((&844)/(&1000))*
\r
245 ((dih_or_v v0 v1 v2 v4)+
\r
246 (dih_or_v v0 v2 v3 v1)))))`);;
\r
248 (* SPIII-1998 Lemma 4.3 *)
\r
250 let J_657406669 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
251 ((#1.153) < dih_or_v v0 v1 v2 v4))`);;
\r
252 let J_277330628 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
\r
253 ((dih_or_v v0 v1 v2 v4) < (#3.247)))`);;
\r
260 LOC: 2002 k.c page 49
\r
261 Five simplices in cyclic order A,B,C,D,E around edge x1.
\r
264 Note from text: If the circumradius of a quasi-regular tetrahedron
\r
265 is >= 1.41, then tau > 1.8 pt and many of the inequalities hold
\r
266 (without further interval arithmetic calculation).
\r
270 (* interval verification by Ferguson *)
\r
285 [((#4.0), x1, square_2t0);
\r
286 ((#4.0), x2A, square_2t0);
\r
287 ((#4.0), x3A, square_2t0);
\r
288 ((#4.0), x4A, square_2t0);
\r
289 ((#4.0), x5A, square_2t0);
\r
290 ((#4.0), x6A, square_2t0);
\r
291 ((#4.0), x2B, square_2t0);
\r
292 ((#4.0), x3B, square_2t0);
\r
293 ((#4.0), x4B, square_2t0);
\r
294 ((#4.0), x5B, square_2t0);
\r
295 ((#4.0), x6B, square_2t0);
\r
296 ((#4.0), x2C, square_2t0);
\r
297 ((#4.0), x3C, square_2t0);
\r
298 ((#8.0), x4C, square_4t0); // NB
\r
299 ((#4.0), x5C, square_2t0);
\r
300 ((#4.0), x6C, square_2t0);
\r
301 ((#4.0), x2D, square_2t0);
\r
302 ((#4.0), x3D, square_2t0);
\r
303 ((#4.0), x4D, square_2t0);
\r
304 ((#4.0), x5D, square_2t0);
\r
305 ((#4.0), x6D, square_2t0);
\r
306 ((#4.0), x2E, square_2t0);
\r
307 ((#4.0), x3E, square_2t0);
\r
308 ((#8.0), x4E, square_4t0); // NB
\r
309 ((#4.0), x5E, square_2t0);
\r
310 ((#4.0), x6E, square_2t0)]
\r
311 (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
\r
312 (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
\r
313 (tau_sigma_x x1 x2D x3D x4D x5D x6D) >. (#1.4) *. pt) \/
\r
314 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
315 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
316 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
317 (dih_x x1 x2D x3D x4D x5D x6D) +.
\r
318 (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi
\r
321 (* interval verification by Ferguson *)
\r
336 [((#4.0), x1, square_2t0);
\r
337 ((#4.0), x2A, square_2t0);
\r
338 ((#4.0), x3A, square_2t0);
\r
339 ((#4.0), x4A, square_2t0);
\r
340 ((#4.0), x5A, square_2t0);
\r
341 ((#4.0), x6A, square_2t0);
\r
342 ((#4.0), x2B, square_2t0);
\r
343 ((#4.0), x3B, square_2t0);
\r
344 ((#4.0), x4B, square_2t0);
\r
345 ((#4.0), x5B, square_2t0);
\r
346 ((#4.0), x6B, square_2t0);
\r
347 ((#4.0), x2C, square_2t0);
\r
348 ((#4.0), x3C, square_2t0);
\r
349 ((#4.0), x4C, square_2t0);
\r
350 ((#4.0), x5C, square_2t0);
\r
351 ((#4.0), x6C, square_2t0);
\r
352 ((#4.0), x2D, square_2t0);
\r
353 ((#4.0), x3D, square_2t0);
\r
354 ((#8.0), x4D, square_4t0); // NB
\r
355 ((#4.0), x5D, square_2t0);
\r
356 ((#4.0), x6D, square_2t0);
\r
357 ((#4.0), x2E, square_2t0);
\r
358 ((#4.0), x3E, square_2t0);
\r
359 ((#8.0), x4E, square_4t0); // NB
\r
360 ((#4.0), x5E, square_2t0);
\r
361 ((#4.0), x6E, square_2t0)]
\r
362 (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
\r
363 (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
\r
364 (tau_sigma_x x1 x2C x3C x4C x5C x6C) >. (#1.4) *. pt) \/
\r
365 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
366 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
367 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
368 (dih_x x1 x2D x3D x4D x5D x6D) +.
\r
369 (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi
\r
372 (* interval verification by Ferguson *)
\r
387 [((#4.0), x1, square_2t0);
\r
388 ((#4.0), x2A, square_2t0);
\r
389 ((#4.0), x3A, square_2t0);
\r
390 ((#4.0), x4A, square_2t0);
\r
391 ((#4.0), x5A, square_2t0);
\r
392 ((#4.0), x6A, square_2t0);
\r
393 ((#4.0), x2B, square_2t0);
\r
394 ((#4.0), x3B, square_2t0);
\r
395 ((#4.0), x4B, square_2t0);
\r
396 ((#4.0), x5B, square_2t0);
\r
397 ((#4.0), x6B, square_2t0);
\r
398 ((#4.0), x2C, square_2t0);
\r
399 ((#4.0), x3C, square_2t0);
\r
400 (square_2t0, x4C, (#8.0)); // NB
\r
401 ((#4.0), x5C, square_2t0);
\r
402 ((#4.0), x6C, square_2t0);
\r
403 ((#4.0), x2D, square_2t0);
\r
404 ((#4.0), x3D, square_2t0);
\r
405 ((#4.0), x4D, square_2t0);
\r
406 ((#4.0), x5D, square_2t0);
\r
407 ((#4.0), x6D, square_2t0);
\r
408 ((#4.0), x2E, square_2t0);
\r
409 ((#4.0), x3E, square_2t0);
\r
410 (square_2t0, x4E, square_4t0); // NB
\r
411 ((#4.0), x5E, square_2t0);
\r
412 ((#4.0), x6E, square_2t0)]
\r
413 (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
\r
414 (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
\r
415 (tauhatpi_x x1 x2C x3C x4C x5C x6C) +.
\r
416 (tau_sigma_x x1 x2D x3D x4D x5D x6D)
\r
417 >. ((#1.4) *. pt +. D31)) \/
\r
418 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
419 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
420 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
421 (dih_x x1 x2D x3D x4D x5D x6D) +.
\r
422 (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi ) \/
\r
423 (dih_x x1 x2E x3E x4E x5E x6E <. #1.32 )
\r
426 (* interval verification by Ferguson *)
\r
441 [((#4.0), x1, square_2t0);
\r
442 ((#4.0), x2A, square_2t0);
\r
443 ((#4.0), x3A, square_2t0);
\r
444 ((#4.0), x4A, square_2t0);
\r
445 ((#4.0), x5A, square_2t0);
\r
446 ((#4.0), x6A, square_2t0);
\r
447 ((#4.0), x2B, square_2t0);
\r
448 ((#4.0), x3B, square_2t0);
\r
449 ((#4.0), x4B, square_2t0);
\r
450 ((#4.0), x5B, square_2t0);
\r
451 ((#4.0), x6B, square_2t0);
\r
452 ((#4.0), x2C, square_2t0);
\r
453 ((#4.0), x3C, square_2t0);
\r
454 ((#4.0), x4C, square_2t0);
\r
455 ((#4.0), x5C, square_2t0);
\r
456 ((#4.0), x6C, square_2t0);
\r
457 ((#4.0), x2D, square_2t0);
\r
458 ((#4.0), x3D, square_2t0);
\r
459 (square_2t0, x4D, (#8.0)); // NB
\r
460 ((#4.0), x5D, square_2t0);
\r
461 ((#4.0), x6D, square_2t0);
\r
462 ((#4.0), x2E, square_2t0);
\r
463 ((#4.0), x3E, square_2t0);
\r
464 (square_2t0, x4E, square_4t0); // NB
\r
465 ((#4.0), x5E, square_2t0);
\r
466 ((#4.0), x6E, square_2t0)]
\r
467 (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
\r
468 (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
\r
469 (tau_sigma_x x1 x2C x3C x4C x5C x6C) +.
\r
470 (tauhatpi_x x1 x2D x3D x4D x5D x6D)
\r
471 >. ((#1.4) *. pt +. D31)) \/
\r
472 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
473 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
474 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
475 (dih_x x1 x2D x3D x4D x5D x6D) +.
\r
476 (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi ) \/
\r
477 (dih_x x1 x2E x3E x4E x5E x6E <. #1.32 )
\r
485 LOC: 2002 k.c page 50
\r
488 Note from text: As in Section 17.20, the quasi-regular tetrahedra
\r
489 are generally compression scored. The constraint sum dih = 2pi
\r
491 [Note 2/17/2004: We relax this constraint to sum dih <= 2 pi.]
\r
495 (* interval verification by Ferguson *)
\r
510 [((#4.0), x1, square_2t0);
\r
511 ((#4.0), x2A, square_2t0);
\r
512 ((#4.0), x3A, square_2t0);
\r
513 ((#4.0), x4A, square_2t0);
\r
514 ((#4.0), x5A, square_2t0);
\r
515 ((#4.0), x6A, square_2t0);
\r
516 ((#4.0), x2B, square_2t0);
\r
517 ((#4.0), x3B, square_2t0);
\r
518 ((#4.0), x4B, square_2t0);
\r
519 ((#4.0), x5B, square_2t0);
\r
520 ((#4.0), x6B, square_2t0);
\r
521 ((#4.0), x2C, square_2t0);
\r
522 ((#4.0), x3C, square_2t0);
\r
523 ((#4.0), x4C, square_2t0);
\r
524 ((#4.0), x5C, square_2t0);
\r
525 ((#4.0), x6C, square_2t0);
\r
526 ((#4.0), x2D, square_2t0);
\r
527 ((#4.0), x3D, square_2t0);
\r
528 ((#4.0), x4D, square_2t0);
\r
529 ((#4.0), x5D, square_2t0);
\r
530 ((#4.0), x6D, square_2t0);
\r
531 ((#4.0), x2E, square_2t0);
\r
532 ((#4.0), x3E, square_2t0);
\r
533 ((#8.0), x4E, square_4t0); // NB
\r
534 ((#4.0), x5E, square_2t0);
\r
535 ((#4.0), x6E, square_2t0)]
\r
536 (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
\r
537 (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
\r
538 (tau_sigma_x x1 x2C x3C x4C x5C x6C) +.
\r
539 (tau_sigma_x x1 x2D x3D x4D x5D x6D)
\r
540 >. ((#1.5) *. pt )) \/
\r
541 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
542 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
543 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
544 (dih_x x1 x2D x3D x4D x5D x6D) +.
\r
545 (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )
\r
548 (* interval verification by Ferguson *)
\r
563 [((#4.0), x1 , square_2t0);
\r
564 ((#4.0), x2A, square_2t0);
\r
565 ((#4.0), x3A, square_2t0);
\r
566 ((#4.0), x4A, square_2t0);
\r
567 ((#4.0), x5A, square_2t0);
\r
568 ((#4.0), x6A, square_2t0);
\r
569 ((#4.0), x2B, square_2t0);
\r
570 ((#4.0), x3B, square_2t0);
\r
571 ((#4.0), x4B, square_2t0);
\r
572 ((#4.0), x5B, square_2t0);
\r
573 ((#4.0), x6B, square_2t0);
\r
574 ((#4.0), x2C, square_2t0);
\r
575 ((#4.0), x3C, square_2t0);
\r
576 ((#4.0), x4C, square_2t0);
\r
577 ((#4.0), x5C, square_2t0);
\r
578 ((#4.0), x6C, square_2t0);
\r
579 ((#4.0), x2D, square_2t0);
\r
580 ((#4.0), x3D, square_2t0);
\r
581 ((#4.0), x4D, square_2t0);
\r
582 ((#4.0), x5D, square_2t0);
\r
583 ((#4.0), x6D, square_2t0);
\r
584 ((#4.0), x2E, square_2t0);
\r
585 ((#4.0), x3E, square_2t0);
\r
586 (square_2t0, x4E, (#8.0)); // NB
\r
587 ((#4.0), x5E, square_2t0);
\r
588 ((#4.0), x6E, square_2t0)]
\r
589 (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
\r
590 (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
\r
591 (tau_sigma_x x1 x2C x3C x4C x5C x6C) +.
\r
592 (tau_sigma_x x1 x2D x3D x4D x5D x6D) +.
\r
593 (tauhatpi_x x1 x2E x3E x4E x5E x6E)
\r
594 >. ((#1.5) *. pt +. D31 )) \/
\r
595 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
596 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
597 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
598 (dih_x x1 x2D x3D x4D x5D x6D) +.
\r
599 (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )
\r
604 LOC: 2002 k.c page 50
\r
606 [The constraint sum dih <= 2pi was not explicitly stated in the text.]
\r
609 (* interval verification by Ferguson, I think. In SPVI-1998, it carries
\r
610 a dagger, which means that Ferguson has done the verification, but the
\r
611 dagger has been commented out in the tex file. -TCH 1/19/2008 *)
\r
626 [((#4.0), x1 , square_2t0);
\r
627 ((#4.0), x2A, square_2t0);
\r
628 ((#4.0), x3A, square_2t0);
\r
629 ((#4.0), x4A, square_2t0);
\r
630 ((#4.0), x5A, square_2t0);
\r
631 ((#4.0), x6A, square_2t0);
\r
632 ((#4.0), x2B, square_2t0);
\r
633 ((#4.0), x3B, square_2t0);
\r
634 ((#4.0), x4B, square_2t0);
\r
635 ((#4.0), x5B, square_2t0);
\r
636 ((#4.0), x6B, square_2t0);
\r
637 ((#4.0), x2C, square_2t0);
\r
638 ((#4.0), x3C, square_2t0);
\r
639 ((#4.0), x4C, square_2t0);
\r
640 ((#4.0), x5C, square_2t0);
\r
641 ((#4.0), x6C, square_2t0);
\r
642 ((#4.0), x2D, square_2t0);
\r
643 ((#4.0), x3D, square_2t0);
\r
644 ((#4.0), x4D, square_2t0);
\r
645 ((#4.0), x5D, square_2t0);
\r
646 ((#4.0), x6D, square_2t0);
\r
647 ((#4.0), x2E, square_2t0);
\r
648 ((#4.0), x3E, square_2t0);
\r
649 (square_2t0, x4E, (#8.0)); // NB
\r
650 ((#4.0), x5E, square_2t0);
\r
651 ((#4.0), x6E, square_2t0)]
\r
652 (((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +.
\r
653 (sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +.
\r
654 (sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +.
\r
655 (sigma_qrtet_x x1 x2D x3D x4D x5D x6D) +.
\r
656 (sigmahat_x x1 x2E x3E x4E x5E x6E)
\r
658 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
659 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
660 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
661 (dih_x x1 x2D x3D x4D x5D x6D) +.
\r
662 (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )
\r
667 LOC: 2002 III, page 15.
\r
670 It asserts that the angle sum around a vertex is 2pi.
\r
671 This is not an interval calculation.
\r
675 LOC: 2002 III, page 15.
\r
677 equation 3. Dihedral sum changed to an inequality.
\r
694 [((#4.0), x1, square_2t0);
\r
695 ((#4.0), x2A, square_2t0);
\r
696 ((#4.0), x3A, square_2t0);
\r
697 ((#4.0), x4A, square_2t0);
\r
698 ((#4.0), x5A, square_2t0);
\r
699 ((#4.0), x6A, square_2t0);
\r
700 ((#4.0), x2B, square_2t0);
\r
701 ((#4.0), x3B, square_2t0);
\r
702 ((#4.0), x4B, square_2t0);
\r
703 ((#4.0), x5B, square_2t0);
\r
704 ((#4.0), x6B, square_2t0);
\r
705 ((#4.0), x2C, square_2t0);
\r
706 ((#4.0), x3C, square_2t0);
\r
707 ((#4.0), x4C, square_2t0);
\r
708 ((#4.0), x5C, square_2t0);
\r
709 ((#4.0), x6C, square_2t0);
\r
710 ((#4.0), x2D, square_2t0);
\r
711 ((#4.0), x3D, square_2t0);
\r
712 ((#4.0), x4D, square_2t0);
\r
713 ((#4.0), x5D, square_2t0);
\r
714 ((#4.0), x6D, square_2t0);
\r
715 ((#4.0), x2E, square_2t0);
\r
716 ((#4.0), x3E, square_2t0);
\r
717 ((#4.0), x4E, square_2t0);
\r
718 ((#4.0), x5E, square_2t0);
\r
719 ((#4.0), x6E, square_2t0)]
\r
721 ((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +.
\r
722 #0.419351*. (sol_x x1 x2A x3A x4A x5A x6A)) +.
\r
723 ((sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +.
\r
724 #0.419351*. (sol_x x1 x2B x3B x4B x5B x6B)) +.
\r
725 ((sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +.
\r
726 #0.419351*. (sol_x x1 x2C x3C x4C x5C x6C)) +.
\r
727 ((sigma_qrtet_x x1 x2D x3D x4D x5D x6D) +.
\r
728 #0.419351*. (sol_x x1 x2D x3D x4D x5D x6D)) +.
\r
729 ((sigma_qrtet_x x1 x2E x3E x4E x5E x6E) +.
\r
730 #0.419351*. (sol_x x1 x2E x3E x4E x5E x6E))
\r
731 <. (#5.0 *. (#0.2856354))) \/
\r
733 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
734 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
735 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
736 (dih_x x1 x2D x3D x4D x5D x6D) +.
\r
737 (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi
\r
743 LOC: 2002 III, page 15.
\r
748 equation 1. Dihedral sum changed to inequality.
\r
763 [((#4.0), x1, square_2t0);
\r
764 ((#4.0), x2A, square_2t0);
\r
765 ((#4.0), x3A, square_2t0);
\r
766 ((#4.0), x4A, square_2t0);
\r
767 ((#4.0), x5A, square_2t0);
\r
768 ((#4.0), x6A, square_2t0);
\r
769 ((#4.0), x2B, square_2t0);
\r
770 ((#4.0), x3B, square_2t0);
\r
771 ((#4.0), x4B, square_2t0);
\r
772 ((#4.0), x5B, square_2t0);
\r
773 ((#4.0), x6B, square_2t0);
\r
774 ((#4.0), x2C, square_2t0);
\r
775 ((#4.0), x3C, square_2t0);
\r
776 ((#4.0), x4C, square_2t0);
\r
777 ((#4.0), x5C, square_2t0);
\r
778 ((#4.0), x6C, square_2t0);
\r
779 ((#4.0), x2D, square_2t0);
\r
780 ((#4.0), x3D, square_2t0);
\r
781 ((#4.0), x4D, square_2t0);
\r
782 ((#4.0), x5D, square_2t0);
\r
783 ((#4.0), x6D, square_2t0)]
\r
784 (((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +.
\r
785 (sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +.
\r
786 (sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +.
\r
787 (sigma_qrtet_x x1 x2D x3D x4D x5D x6D) <. (#0.33) *. pt) \/
\r
788 ((dih_x x1 x2A x3A x4A x5A x6A) +.
\r
789 (dih_x x1 x2B x3B x4B x5B x6B) +.
\r
790 (dih_x x1 x2C x3C x4C x5C x6C) +.
\r
791 (dih_x x1 x2D x3D x4D x5D x6D) <. (#2.0) *. pi
\r
796 LOC: 2002 k.c page 52--53
\r
800 (* interval verification by Ferguson *)
\r
815 [((#4.0), x1, square_2t0);
\r
816 ((#4.0), x2A, square_2t0);
\r
817 ((#4.0), x3A, square_2t0);
\r
818 ((#4.0), x4A, square_2t0);
\r
819 ((#4.0), x5A, square_2t0);
\r
820 ((#4.0), x6A, square_2t0);
\r
821 ((#4.0), x2B, square_2t0);
\r
822 ((#4.0), x3B, square_2t0);
\r
823 ((#4.0), x4B, square_2t0);
\r
824 ((#4.0), x5B, square_2t0);
\r
825 ((#4.0), x6B, square_2t0);
\r
826 ((#4.0), x2C, square_2t0);
\r
827 ((#4.0), x3C, square_2t0);
\r
828 ((#4.0), x4C, square_2t0);
\r
829 ((#4.0), x5C, square_2t0);
\r
830 ((#4.0), x6C, square_2t0);
\r
831 ((#4.0), x2D, square_2t0);
\r
832 ((#4.0), x3D, square_2t0);
\r
833 ((#4.0), x4D, square_2t0);
\r
834 ((#4.0), x5D, square_2t0);
\r
835 ((#4.0), x6D, square_2t0);
\r
836 ((#4.0), x2E, square_2t0);
\r
837 ((#4.0), x3E, square_2t0);
\r
838 ((square_2t0), x4E, (square_4t0)); // (* NB *)
\r
839 ((#4.0), x5E, square_2t0);
\r
840 ((#4.0), x6E, square_2t0)]
\r
841 ((sqrt x2A) + (sqrt x2B) + (sqrt x2C) + (sqrt x2D) + (sqrt x2E) +
\r
842 (sqrt x6A) + (sqrt x6B) + (sqrt x6C) + (sqrt x6D) + (sqrt x6E) >. (#20.42)))`;;
\r
844 (* interval verification by Ferguson *)
\r
859 [((#4.0), x1, square_2t0);
\r
860 ((#4.0), x2A, square_2t0);
\r
861 ((#4.0), x3A, square_2t0);
\r
862 ((#4.0), x4A, square_2t0);
\r
863 ((#4.0), x5A, square_2t0);
\r
864 ((#4.0), x6A, square_2t0);
\r
865 ((#4.0), x2B, square_2t0);
\r
866 ((#4.0), x3B, square_2t0);
\r
867 ((#4.0), x4B, square_2t0);
\r
868 ((#4.0), x5B, square_2t0);
\r
869 ((#4.0), x6B, square_2t0);
\r
870 ((#4.0), x2C, square_2t0);
\r
871 ((#4.0), x3C, square_2t0);
\r
872 ((#4.0), x4C, square_2t0);
\r
873 ((#4.0), x5C, square_2t0);
\r
874 ((#4.0), x6C, square_2t0);
\r
875 ((#4.0), x2D, square_2t0);
\r
876 ((#4.0), x3D, square_2t0);
\r
877 ((#4.0), x4D, square_2t0);
\r
878 ((#4.0), x5D, square_2t0);
\r
879 ((#4.0), x6D, square_2t0);
\r
880 ((#4.0), x2E, square_2t0);
\r
881 ((#4.0), x3E, square_2t0);
\r
882 ((#8.0), x4E, (square_4t0)); // (* NB *)
\r
883 ((#4.0), x5E, square_2t0);
\r
884 ((#4.0), x6E, square_2t0)]
\r
885 ((sqrt x2A) + (sqrt x2B) + (sqrt x2C) + (sqrt x2D) + (sqrt x2E) +
\r
886 (sqrt x6A) + (sqrt x6B) + (sqrt x6C) + (sqrt x6D) + (sqrt x6E) >. (#20.76)))`;;
\r
889 (* Duplicate inequality. This is the same as 413688580 *)
\r
893 [(square_2t0, x1, (#8.0));
\r
894 ((#4.0), x2, square_2t0);
\r
895 ((#4.0), x3, square_2t0);
\r
896 ((#4.0), x4, square_2t0);
\r
897 ((#4.0), x5, square_2t0);
\r
898 ((#4.0), x6, square_2t0)
\r
901 ( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#4.10113)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#4.3223)))`;;
\r
905 (* Duplicate inequality. This is the same as 805296510 *)
\r
909 [(square_2t0, x1, (#8.0));
\r
910 ((#4.0), x2, square_2t0);
\r
911 ((#4.0), x3, square_2t0);
\r
912 ((#4.0), x4, square_2t0);
\r
913 ((#4.0), x5, square_2t0);
\r
914 ((#4.0), x6, square_2t0)
\r
917 ( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.80449)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#0.9871)))`;;
\r
920 (* Duplicate inequality. This is the same as 136610219 *)
\r
924 [(square_2t0, x1, (#8.0));
\r
925 ((#4.0), x2, square_2t0);
\r
926 ((#4.0), x3, square_2t0);
\r
927 ((#4.0), x4, square_2t0);
\r
928 ((#4.0), x5, square_2t0);
\r
929 ((#4.0), x6, square_2t0)
\r
932 ( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.70186)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#0.8756)))`;;
\r
935 (* Duplicate inequality. This is the same as 379204810 *)
\r
939 [(square_2t0, x1, (#8.0));
\r
940 ((#4.0), x2, square_2t0);
\r
941 ((#4.0), x3, square_2t0);
\r
942 ((#4.0), x4, square_2t0);
\r
943 ((#4.0), x5, square_2t0);
\r
944 ((#4.0), x6, square_2t0)
\r
947 ( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.24573)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#0.3404)))`;;
\r
950 (* Duplicate inequality. This is the same as 878731435 *)
\r
954 [(square_2t0, x1, (#8.0));
\r
955 ((#4.0), x2, square_2t0);
\r
956 ((#4.0), x3, square_2t0);
\r
957 ((#4.0), x4, square_2t0);
\r
958 ((#4.0), x5, square_2t0);
\r
959 ((#4.0), x6, square_2t0)
\r
962 ( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.00154)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#0.0024)))`;;
\r
965 (* Duplicate inequality. This is the same as 891740103 *)
\r
969 [(square_2t0, x1, (#8.0));
\r
970 ((#4.0), x2, square_2t0);
\r
971 ((#4.0), x3, square_2t0);
\r
972 ((#4.0), x4, square_2t0);
\r
973 ((#4.0), x5, square_2t0);
\r
974 ((#4.0), x6, square_2t0)
\r
977 ( (nu_x x1 x2 x3 x4 x5 x6) +. ( (#0.07611) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (#0.1196))`;;
\r
980 (* Duplicate inequality. This is the same as 334002329 *)
\r
984 [(square_2t0, x1, (#8.0));
\r
985 ((#4.0), x2, square_2t0);
\r
986 ((#4.0), x3, square_2t0);
\r
987 ((#4.0), x4, square_2t0);
\r
988 ((#4.0), x5, square_2t0);
\r
989 ((#4.0), x6, square_2t0)
\r
992 ( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#4.16523) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#4.42873))`;;
\r
995 (* Duplicate inequality. This is the same as 883139937 *)
\r
999 [(square_2t0, x1, (#8.0));
\r
1000 ((#4.0), x2, square_2t0);
\r
1001 ((#4.0), x3, square_2t0);
\r
1002 ((#4.0), x4, square_2t0);
\r
1003 ((#4.0), x5, square_2t0);
\r
1004 ((#4.0), x6, square_2t0)
\r
1007 ( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#0.78701) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#1.01104))`;;
\r
1010 (* Duplicate inequality. This is the same as 507989176 *)
\r
1012 let J_574435320_3=
\r
1014 [(square_2t0, x1, (#8.0));
\r
1015 ((#4.0), x2, square_2t0);
\r
1016 ((#4.0), x3, square_2t0);
\r
1017 ((#4.0), x4, square_2t0);
\r
1018 ((#4.0), x5, square_2t0);
\r
1019 ((#4.0), x6, square_2t0)
\r
1022 ( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#0.77627) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#0.99937))`;;
\r
1025 (* Duplicate inequality. This is the same as 244435805 *)
\r
1027 let J_574435320_4=
\r
1029 [(square_2t0, x1, (#8.0));
\r
1030 ((#4.0), x2, square_2t0);
\r
1031 ((#4.0), x3, square_2t0);
\r
1032 ((#4.0), x4, square_2t0);
\r
1033 ((#4.0), x5, square_2t0);
\r
1034 ((#4.0), x6, square_2t0)
\r
1037 ( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#0.21916) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#0.34877))`;;
\r
1040 (* Duplicate inequality. This is the same as 930176500 *)
\r
1042 let J_574435320_5=
\r
1044 [(square_2t0, x1, (#8.0));
\r
1045 ((#4.0), x2, square_2t0);
\r
1046 ((#4.0), x3, square_2t0);
\r
1047 ((#4.0), x4, square_2t0);
\r
1048 ((#4.0), x5, square_2t0);
\r
1049 ((#4.0), x6, square_2t0)
\r
1052 ( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#0.05107) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#0.11434))`;;
\r
1055 (* Duplicate inequality. This is the same as 815681339 *)
\r
1057 let J_574435320_6=
\r
1059 [(square_2t0, x1, (#8.0));
\r
1060 ((#4.0), x2, square_2t0);
\r
1061 ((#4.0), x3, square_2t0);
\r
1062 ((#4.0), x4, square_2t0);
\r
1063 ((#4.0), x5, square_2t0);
\r
1064 ((#4.0), x6, square_2t0)
\r
1067 ( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.07106)) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (--. (#0.07749)))`;;
\r
1071 This was false for strict inequality.
\r
1072 gives equality at [8,4,4,8,4,4].
\r
1073 It is trivially true when weak inequality is used, because dih(simplex)<=pi
\r
1074 without any constraints on the simplex. So we don't need interval arithmetic
\r
1075 for its verification. Commented out.
\r
1078 let I_853728973_24=
\r
1080 [(square_2t0, x1, (#8.0));
\r
1081 ((#4.0), x2, square_2t0);
\r
1082 ((#4.0), x3, square_2t0);
\r
1083 (square_2t0, x4, (#8.0));
\r
1084 ((#4.0), x5, square_2t0);
\r
1085 ((#4.0), x6, square_2t0)
\r
1087 ( (dih_x x1 x2 x3 x4 x5 x6) <=. pi)`;;
\r
1094 gives equality at [8,4,4,8,4,4].
\r
1095 See comments for I_853728973_24.
\r
1099 let I_853728973_26=
\r
1101 [(square_2t0, x1, (#8.0));
\r
1102 ((#4.0), x2, square_2t0);
\r
1103 ((#4.0), x3, square_2t0);
\r
1104 (square_2t0, x4, square_4t0);
\r
1105 ((#4.0), x5, square_2t0);
\r
1106 ((#4.0), x6, square_2t0)
\r
1108 ( (dih_x x1 x2 x3 x4 x5 x6) <=. pi)`;;
\r
1114 gives equality at [8,4,4,8,4,4].
\r
1115 Interval verification not needed.
\r
1116 See comments for I_853728973_24.
\r
1120 let I_853728973_28=
\r
1122 [(square_2t0, x1, (#8.0));
\r
1123 ((#4.0), x2, square_2t0);
\r
1124 ((#4.0), x3, square_2t0);
\r
1125 ((#8.0), x4, square_4t0);
\r
1126 ((#4.0), x5, square_2t0);
\r
1127 ((#4.0), x6, square_2t0)
\r
1129 ( (dih_x x1 x2 x3 x4 x5 x6) <=. pi)`;;
\r
1135 gives equality at [4,4,8,4,4,8]
\r
1136 Interval verification not needed,
\r
1137 since dih is always >= 0.
\r
1138 See comments for I_853728973_24.
\r
1142 let I_853728973_33=
\r
1144 [((#4.0), x1, square_2t0);
\r
1145 ((#4.0), x2, square_2t0);
\r
1146 (square_2t0, x3, (#8.0));
\r
1147 ((#4.0), x4, square_2t0);
\r
1148 ((#4.0), x5, square_2t0);
\r
1149 (square_2t0, x6, (#8.0))
\r
1151 ( (dih_x x1 x2 x3 x4 x5 x6) =>. (#0.0))`;;
\r