(* This file is a continuation of kep_inequalities.ml.
It contains the inequalities related to quad clusters.
It also contains some particularly long, tricky, or high-dimensional verifications *)
(* ----------------------------------------------------------------------- *)
(*
latex-format comment
\section{Notes on Interval Verifications}
%{Appendix 2. Interval Verifications}
\label{sec:verification-notes}
We make a few remarks in this appendix on the verification of the
inequalities of Proposition~\ref{calc:quad-bounds} and \ref{calc:d(R)}.
The basic method in proving an inequality $f(x)<0$ for $x\in C$, is to
use computer-based interval arithmetic to obtain rigorous upper bounds
on the second derivatives: $|f_{ij}(x)|\le a_{ij}$, for $x\in C$. These
bounds lead immediately to upper bounds on $f(x)$ through a Taylor
approximation with explicit bounds on the error. We divide the domain
$C$ as necessary until the Taylor approximation on each piece is less
that the desired bound.
Some of the inequalities involve as many as $12$ variables, such as the
octahedral cases of Lemma~\ref{calc:d(R)}. These are not directly
accessible by computer. We describe some reductions we have used, based
on linear programming. We start by applying the dimension reduction
techniques described in~\cite[Sec.~8.7]{part1}. We have used these
whenever possible.
We will describe Lemma~\ref{calc:d(R)} because in various respects these
inequalities have been the most difficult to prove, although the
verifications of Lemmas~\ref{calc:quad-bounds} and \ref{lemma:1.153} are
quite similar. If there is a diagonal of length $\le2\sqrt{2}$, we have
two flat quarters $S_1$ and $S_2$. The score breaks up into
$\sigma=\sigma(S_1)+\sigma(S_2)$. The simplices $S_1$ and
$S_2$ share a three-dimensional face. The inequality we wish to prove
has the form
$$\sigma \le a(\dih(S_1)+\dih_2(S_1)+\dih_2(S_2))+b.$$
We break the shared face into smaller domains on which we have
$$
\begin{array}{lll}
\sigma(S_1)&\le a (\dih(S_1)+\dih_2(S_1)) + b_1,\\
\sigma(S_2)&\le a \dih_2(S_1) + b_2,\\
\end{array}
$$
for some $b_1,b_2$ satisfying $b_1+b_2\le b$. These inequalities are
six-dimensional verifications.
If the quad cluster is an octahedron with upright diagonal, there are
four upright quarters $S_1,\ldots,S_4$. We consider inequalities of the
form
\begin{equation}
\sigma(S_i)\le \sum _{j\ne 4} a_j^i y_j(S_i)
+ a_7 (\dih_1(S_i)-\pi/2) + \sum_{j=2}^3 a \epsilon^i_j \dih_j(S_i)
+ b^i.
\label{eqn:Xi}
\end{equation}
If $\sum_{i=1}^4 a_j^i \le0$, $j\ne 4$, and $\sum_i b^i\le b$, then for
appropriate $\epsilon^i_j\in\{0,1\}$, these inequalities imply the full
inequality for octahedral quad clusters.
By linear programming techniques, we were able to divide the domain of
all octahedra into about $1200$ pieces and find inequalities of this
form on each piece, giving an explicit list of inequalities that imply
Lemma~\ref{calc:d(R)}. The inequalities involve six variables and were
verified by interval arithmetic.
To find the optimal coefficients $a_j^i$ by linear programming we pose
the linear problem
$$
\begin{array}{lll}
&\max t \\
&\hbox{such that}\\
&\quad X_i,\quad i=1,2,3,4, \ \{S_1,S_2,S_3,S_4\}\in C\\
&\quad\sum_i a_j^i \le 0,\\
&\quad\sum_i b^i \le b,
\end{array}
$$
where $\{S_1,S_2,S_3,S_4\}$ runs over all octahedra in a given domain
$C$. The nonlinear inequalities~\ref{eqn:Xi} are to be regarded as
linear conditions on the coefficients $a_j^i$, $b^i$, etc. The nonlinear
functions $\sigma(S_i),\dih(S_i)$, $y_j(S_i)$ are to be regarded as the
coefficients of the variables $a_j^i,\ldots$ in a system of linear
inequalities. There are infinitely many constraints, because the set
$C$ of octahedra is infinite. In practice we approximate $C$ by a large
finite set. If the maximum of $t$ is positive, then we have a
collection of inequalities in small dimensions that imply the inequality
for octahedral quad clusters. Otherwise, we subdivide $C$ into smaller
domains and try again. Eventually, we succeed in partitioning the
problem into six-dimensional pieces, which were verified by interval
methods.
\smallskip
If the quad cluster is a mixed case, then Lemma~\ref{lemma:1.04} gives
$$\sigma\le \vor_0, -1.04\,\pt,$$ so also
$$\sigma \le \frac{3}{4}\vor_0 + \frac{1}{4} (-1.04\,\pt).$$
In the pure Voronoi case with no quarters and no enclosed vertices, we
have the approximation
$$\sigma \le \vor(\cdot,\sqrt2) \le \vor_0.$$
If we prove $\vor_0\le a (\dih_1+\dih_2) + b$, the mixed case is
established. This is how the first of the Inequalities~\ref{calc:d(R)}
was established. Dimension reduction reduces this to a seven-dimensional
verification. We draw the shorter of the two diagonals between corners
of the quad cluster. As we begin to subdivide this seven-dimensional
domain, we are able to separate the quad cluster into two simplices
along the diagonal, each scored by $\vor_0$. This reduces the dimension
further, to make it accessible. The two last two cases of
Inequality~\ref{calc:d(R)}, are similar, but we establish the
inequalities
$$
\begin{array}{lll}
\frac{3}{4}\vor_0 + \frac{1}{4} (-1.04\,\pt) &\le a (\dih_1+\dih_2) + b,\\
\vor(\cdot,\sqrt2)&\le a (\dih_1+\dih_2) + b.
\end{array}
$$
This completes our sketch of how the verifications were made.
*)
(* now we can list inequalities *)
(* SPIII-1998 Lemma 4.1 *)
let J_310151857 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&57906)/(&10000)
+ ((&456766)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_655029773 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&20749)/(&10000)
+ ((&15094)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_73283761 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&8341)/(&10000)
+ ((&5301)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_15141595 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&6284)/(&10000)
+ ((&3878)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_574391221 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&4124)/(&10000)
- ((&1897)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_396281725 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&15707)/(&10000)
- ((&5905)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_166451608 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&41717)/(&100000)
- ((&3)/(&10))*(solid_area_quad_v v0 v1 v2 v3 v4)))`);;
let J_539320075 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&581446)/(&100000)
+ ((&449461)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_122375455 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&2955)/(&1000)
+ ((&21406)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_408478278 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&6438)/(&10000)
+ ((&316)/(&1000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_996268658 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&1317)/(&10000)))`);;
let J_393682353 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < (&3825)/(&10000)
- ((&2365)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_775642319 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < (&1071)/(&1000)
- ((&4747)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_616145964 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10))) <
--(&577942)/(&100000)
+ ((&425863)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;
let J_153920401 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <
--(&4893)/(&1000)
+ ((&35294)/(&10000))*(dih_or_v v0 v1 v2 v4))))`);;
let J_337637212 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <
--(&4126)/(&10000))))`);;
let J_768057794 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <
(&33)/(&100)
- ((&316)/(&1000))*(dih_or_v v0 v1 v2 v4))))`);;
let J_465497818 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4 <
-- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)
- (&5350181)/(&1000000)
+ ((&4611391)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;
let J_18502666 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4 <
-- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)
- (&166174)/(&100000)
+ ((&1582508)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;
let J_676439533 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4 <
-- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)
+ (&895)/(&10000)
+ ((&342747)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;
let J_974296985 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4 <
-- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)
+ (&336909)/(&100000)
- ((&974137)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;
let C_940884472 = list_mk_conj[
J_310151857;
J_655029773;
J_73283761;
J_15141595;
J_574391221;
J_396281725;
J_166451608;
J_539320075;
J_122375455;
J_408478278;
J_996268658;
J_393682353;
J_775642319;
J_616145964;
J_153920401;
J_337637212;
J_768057794;
J_465497818;
J_18502666 ;
J_676439533;
J_974296985;];;
(* SPIII-1998 Lemma 4.2 *)
let J_322621318 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4 <
-- (&9494)/(&1000)
+ ((&30508)/(&100000))*
((dih_or_v v0 v1 v2 v4)+
(dih_or_v v0 v2 v3 v1)))))`);;
let J_444643063 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4 <
-- (&10472)/(&100000)
+ ((&27605)/(&100000))*
((dih_or_v v0 v1 v2 v4)+
(dih_or_v v0 v2 v3 v1)))))`);;
let J_552698390 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((sigma_quad_approx1 v0 v1 v2 v3 v4 <
(&35926)/(&10000)
- ((&844)/(&1000))*
((dih_or_v v0 v1 v2 v4)+
(dih_or_v v0 v2 v3 v1)))))`);;
(* SPIII-1998 Lemma 4.3 *)
let J_657406669 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((#1.153) < dih_or_v v0 v1 v2 v4))`);;
let J_277330628 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>
((dih_or_v v0 v1 v2 v4) < (#3.247)))`);;
(*
LOC: 2002 k.c page 49
Five simplices in cyclic order A,B,C,D,E around edge x1.
17.20 Group_20
Note from text: If the circumradius of a quasi-regular tetrahedron
is >= 1.41, then tau > 1.8 pt and many of the inequalities hold
(without further interval arithmetic calculation).
*)
(* interval verification by Ferguson *)
let I_551665569=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#8.0), x4C, square_4t0); // NB
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
((#8.0), x4E, square_4t0); // NB
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
(((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
(tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
(tau_sigma_x x1 x2D x3D x4D x5D x6D) >. (#1.4) *. pt) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) +.
(dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi
)))`;;
(* interval verification by Ferguson *)
let I_824762926=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#8.0), x4D, square_4t0); // NB
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
((#8.0), x4E, square_4t0); // NB
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
(((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
(tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
(tau_sigma_x x1 x2C x3C x4C x5C x6C) >. (#1.4) *. pt) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) +.
(dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi
)))`;;
(* interval verification by Ferguson *)
let I_675785884=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
(square_2t0, x4C, (#8.0)); // NB
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
(square_2t0, x4E, square_4t0); // NB
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
(((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
(tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
(tauhatpi_x x1 x2C x3C x4C x5C x6C) +.
(tau_sigma_x x1 x2D x3D x4D x5D x6D)
>. ((#1.4) *. pt +. D31)) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) +.
(dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi ) \/
(dih_x x1 x2E x3E x4E x5E x6E <. #1.32 )
))`;;
(* interval verification by Ferguson *)
let I_193592217=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
(square_2t0, x4D, (#8.0)); // NB
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
(square_2t0, x4E, square_4t0); // NB
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
(((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
(tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
(tau_sigma_x x1 x2C x3C x4C x5C x6C) +.
(tauhatpi_x x1 x2D x3D x4D x5D x6D)
>. ((#1.4) *. pt +. D31)) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) +.
(dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi ) \/
(dih_x x1 x2E x3E x4E x5E x6E <. #1.32 )
))`;;
(*
LOC: 2002 k.c page 50
17.21 Group_21
Note from text: As in Section 17.20, the quasi-regular tetrahedra
are generally compression scored. The constraint sum dih = 2pi
is assumed.
[Note 2/17/2004: We relax this constraint to sum dih <= 2 pi.]
*)
(* interval verification by Ferguson *)
let I_325738864=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
((#8.0), x4E, square_4t0); // NB
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
(((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
(tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
(tau_sigma_x x1 x2C x3C x4C x5C x6C) +.
(tau_sigma_x x1 x2D x3D x4D x5D x6D)
>. ((#1.5) *. pt )) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) +.
(dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )
))`;;
(* interval verification by Ferguson *)
let I_314974315=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1 , square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
(square_2t0, x4E, (#8.0)); // NB
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
(((tau_sigma_x x1 x2A x3A x4A x5A x6A) +.
(tau_sigma_x x1 x2B x3B x4B x5B x6B) +.
(tau_sigma_x x1 x2C x3C x4C x5C x6C) +.
(tau_sigma_x x1 x2D x3D x4D x5D x6D) +.
(tauhatpi_x x1 x2E x3E x4E x5E x6E)
>. ((#1.5) *. pt +. D31 )) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) +.
(dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )
))`;;
(*
LOC: 2002 k.c page 50
17.22 Group_22
[The constraint sum dih <= 2pi was not explicitly stated in the text.]
*)
(* interval verification by Ferguson, I think. In SPVI-1998, it carries
a dagger, which means that Ferguson has done the verification, but the
dagger has been commented out in the tex file. -TCH 1/19/2008 *)
let I_867359387=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1 , square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
(square_2t0, x4E, (#8.0)); // NB
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
(((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +.
(sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +.
(sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +.
(sigma_qrtet_x x1 x2D x3D x4D x5D x6D) +.
(sigmahat_x x1 x2E x3E x4E x5E x6E)
<. #0.114) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) +.
(dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )
))`;;
(*
LOC: 2002 III, page 15.
Sec. 10, Group_4
SKIP equation 2.
It asserts that the angle sum around a vertex is 2pi.
This is not an interval calculation.
*)
(*
LOC: 2002 III, page 15.
Sec. 10, Group_4
equation 3. Dihedral sum changed to an inequality.
*)
let J_694278521=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
((#4.0), x4E, square_2t0);
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
((
((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +.
#0.419351*. (sol_x x1 x2A x3A x4A x5A x6A)) +.
((sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +.
#0.419351*. (sol_x x1 x2B x3B x4B x5B x6B)) +.
((sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +.
#0.419351*. (sol_x x1 x2C x3C x4C x5C x6C)) +.
((sigma_qrtet_x x1 x2D x3D x4D x5D x6D) +.
#0.419351*. (sol_x x1 x2D x3D x4D x5D x6D)) +.
((sigma_qrtet_x x1 x2E x3E x4E x5E x6E) +.
#0.419351*. (sol_x x1 x2E x3E x4E x5E x6E))
<. (#5.0 *. (#0.2856354))) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) +.
(dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi
)))`;;
(*
LOC: 2002 III, page 15.
Sec. 10, Group_4
*)
(*
equation 1. Dihedral sum changed to inequality.
*)
let J_895315463=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6A = x5D in
let x2A = x3D in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0)]
(((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +.
(sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +.
(sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +.
(sigma_qrtet_x x1 x2D x3D x4D x5D x6D) <. (#0.33) *. pt) \/
((dih_x x1 x2A x3A x4A x5A x6A) +.
(dih_x x1 x2B x3B x4B x5B x6B) +.
(dih_x x1 x2C x3C x4C x5C x6C) +.
(dih_x x1 x2D x3D x4D x5D x6D) <. (#2.0) *. pi
)))`;;
(*
LOC: 2002 k.c page 52--53
17.28 Group_28
*)
(* interval verification by Ferguson *)
let I_615073260=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
((square_2t0), x4E, (square_4t0)); // (* NB *)
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
((sqrt x2A) + (sqrt x2B) + (sqrt x2C) + (sqrt x2D) + (sqrt x2E) +
(sqrt x6A) + (sqrt x6B) + (sqrt x6C) + (sqrt x6D) + (sqrt x6E) >. (#20.42)))`;;
(* interval verification by Ferguson *)
let I_844430737=
all_forall
`
let x6B = x5A in
let x2B = x3A in
let x6C = x5B in
let x2C = x3B in
let x6D = x5C in
let x2D = x3C in
let x6E = x5D in
let x2E = x3D in
let x6A = x5E in
let x2A = x3E in
(ineq
[((#4.0), x1, square_2t0);
((#4.0), x2A, square_2t0);
((#4.0), x3A, square_2t0);
((#4.0), x4A, square_2t0);
((#4.0), x5A, square_2t0);
((#4.0), x6A, square_2t0);
((#4.0), x2B, square_2t0);
((#4.0), x3B, square_2t0);
((#4.0), x4B, square_2t0);
((#4.0), x5B, square_2t0);
((#4.0), x6B, square_2t0);
((#4.0), x2C, square_2t0);
((#4.0), x3C, square_2t0);
((#4.0), x4C, square_2t0);
((#4.0), x5C, square_2t0);
((#4.0), x6C, square_2t0);
((#4.0), x2D, square_2t0);
((#4.0), x3D, square_2t0);
((#4.0), x4D, square_2t0);
((#4.0), x5D, square_2t0);
((#4.0), x6D, square_2t0);
((#4.0), x2E, square_2t0);
((#4.0), x3E, square_2t0);
((#8.0), x4E, (square_4t0)); // (* NB *)
((#4.0), x5E, square_2t0);
((#4.0), x6E, square_2t0)]
((sqrt x2A) + (sqrt x2B) + (sqrt x2C) + (sqrt x2D) + (sqrt x2E) +
(sqrt x6A) + (sqrt x6B) + (sqrt x6C) + (sqrt x6D) + (sqrt x6E) >. (#20.76)))`;;
(* Duplicate inequality. This is the same as 413688580 *)
(*
let J_549774315_1=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#4.10113)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#4.3223)))`;;
*)
(* Duplicate inequality. This is the same as 805296510 *)
(*
let J_549774315_2=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.80449)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#0.9871)))`;;
*)
(* Duplicate inequality. This is the same as 136610219 *)
(*
let J_549774315_3=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.70186)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#0.8756)))`;;
*)
(* Duplicate inequality. This is the same as 379204810 *)
(*
let J_549774315_4=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.24573)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#0.3404)))`;;
*)
(* Duplicate inequality. This is the same as 878731435 *)
(*
let J_549774315_5=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (nu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.00154)) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (--. (#0.0024)))`;;
*)
(* Duplicate inequality. This is the same as 891740103 *)
(*
let J_549774315_6=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (nu_x x1 x2 x3 x4 x5 x6) +. ( (#0.07611) *. (dih_x x1 x2 x3 x4 x5 x6))) <. (#0.1196))`;;
*)
(* Duplicate inequality. This is the same as 334002329 *)
(*
let J_574435320_1=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#4.16523) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#4.42873))`;;
*)
(* Duplicate inequality. This is the same as 883139937 *)
(*
let J_574435320_2=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#0.78701) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#1.01104))`;;
*)
(* Duplicate inequality. This is the same as 507989176 *)
(*
let J_574435320_3=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#0.77627) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#0.99937))`;;
*)
(* Duplicate inequality. This is the same as 244435805 *)
(*
let J_574435320_4=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#0.21916) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#0.34877))`;;
*)
(* Duplicate inequality. This is the same as 930176500 *)
(*
let J_574435320_5=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (#0.05107) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (#0.11434))`;;
*)
(* Duplicate inequality. This is the same as 815681339 *)
(*
let J_574435320_6=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
(
( (taunu_x x1 x2 x3 x4 x5 x6) +. ( (--. (#0.07106)) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (--. (#0.07749)))`;;
*)
(*
This was false for strict inequality.
gives equality at [8,4,4,8,4,4].
It is trivially true when weak inequality is used, because dih(simplex)<=pi
without any constraints on the simplex. So we don't need interval arithmetic
for its verification. Commented out.
*)
(*
let I_853728973_24=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
(square_2t0, x4, (#8.0));
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
( (dih_x x1 x2 x3 x4 x5 x6) <=. pi)`;;
*)
(*
dih < pi is false
gives equality at [8,4,4,8,4,4].
See comments for I_853728973_24.
*)
(*
let I_853728973_26=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
(square_2t0, x4, square_4t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
( (dih_x x1 x2 x3 x4 x5 x6) <=. pi)`;;
*)
(*
dih < pi is false
gives equality at [8,4,4,8,4,4].
Interval verification not needed.
See comments for I_853728973_24.
*)
(*
let I_853728973_28=
all_forall `ineq
[(square_2t0, x1, (#8.0));
((#4.0), x2, square_2t0);
((#4.0), x3, square_2t0);
((#8.0), x4, square_4t0);
((#4.0), x5, square_2t0);
((#4.0), x6, square_2t0)
]
( (dih_x x1 x2 x3 x4 x5 x6) <=. pi)`;;
*)
(*
dih > 0 is false
gives equality at [4,4,8,4,4,8]
Interval verification not needed,
since dih is always >= 0.
See comments for I_853728973_24.
*)
(*
let I_853728973_33=
all_forall `ineq
[((#4.0), x1, square_2t0);
((#4.0), x2, square_2t0);
(square_2t0, x3, (#8.0));
((#4.0), x4, square_2t0);
((#4.0), x5, square_2t0);
(square_2t0, x6, (#8.0))
]
( (dih_x x1 x2 x3 x4 x5 x6) =>. (#0.0))`;;
*)