Rather than compactifying the space of decomposition stars and proving
the
continuity of the scoring function, for the formal proof it should be
easier
just to bound the scoring function away from 8pt by an explicit
constant.

For this, Lemma 10.6 (DCGVersion2004) needs to be strengthened to give
an
explicit constant less than 4.52 pt.  A Lemma 10.7 giving the better
constant
will be added to the 2005 Version of DCG.

Here are the calculations that are required.  I have added one interval
calculation to kep_inequalities.ml.

Here is the inequality:

let J_241241504_1=
   all_forall `ineq
    [((#4.0), x1, square_2t0);
     ((#4.0), x2, square_2t0);
     ((#4.0), x3, square_2t0);

        ((square (#2.177303)), x4, square_2t0);
     ((#4.0), x5, square_2t0);
     ((#4.0), x6, square_2t0)
    ]
    ( (sigma_qrtet_x x1 x2 x3 x4 x5 x6) <.  (  0.028794285 ))`;;

Here is the interval arithmetic code and the output to justify it:

------------------------
code added to part3.cpp:
------------------------

int C2005_03_07_241241504() // redo 241241504 with better constant on
March 7, 2005.
{
// F < 0.
domain x,z;
interval xi("2.177303");
interval s=xi*xi;
interval tx[6]={"4","4","4","4","4",s};
x = domain::lowerD(tx);
interval tz[6]={"6.3001","6.3001","6.3001","6.3001","6.3001","6.3001"};
z = domain::upperD(tz);
taylorFunction F = taylorSimplex::unit*("-0.028794285") ; // about 0.52
pt - 10^-8
F.setReducibleState(1);
return prove::qrtet(x,z,F);

...

if (C2005_03_07_241241504())
cout << "C2005_03_07_241241504 done"; else cout << "NO!" ;
error::printTime();
cout << endl;

---------------------------
OS: Windows 2000
Date: March 7, 2005
Computer: 51873-270-7013415-09832, University of Pittsburgh
Compiler: Microsoft Visual C++
Workspace: interval
Output follows:
---------------------------
gamma done! 1110232230
vor done! 1110232308
C2005_03_07_241241504 done1110232308

1110232308
(no errors++)
Press any key to continue