text_formalization/nonlinear/types.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                  *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-05-30                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 File of types for nonlinear inequalities to be verified by interval arithmetic.
  11 *)
  12
  13 type tag =
  14   (* Application and organization tags *)
  15
  16  | Flypaper of string list
  17  | Clusterlp   | Marchal
  18  | Tablelp | Main_estimate
  19  | Fejestoth | Strongdodec | Further
  20  | Tex | Derived of string list   | Deprecated
  21
  22   (* Numerical testing tags *)
  23
  24   | Cfsqp | Cfsqp_branch of int | Eps of float
  25   | Penalty of float*float
  26
  27   (* Linear programming tags *)
  28   |  Lp | Lp_aux of string | Lpsymmetry
  29
  30   (* Interval arithmetic verification tags *)
  31
  32   | Xconvert
  33   | Split of int list
  34   | Branching | Sharp  | Disallow_derivatives | Onlycheckderiv1negative
  35   | Dim_red | Dim_red_backsym
  36   | Quad_cluster of float
  37   | Set_rad2 | Delta126min of float | Delta126max of float | Widthcutoff of float
  38   | Delta135min of float | Delta135max of float
  39   | Set298 (* deprecated *)
  40   ;;
  41
  42 type ineq_datum =
  43   {
  44     ineq : term;
  45     idv : string; (* name changed 2/16/2011 because of conflict with type_expr *)
  46     doc : string;
  47     tags : tag list;
  48   };;
  49
  50 type texmarker = Section | Ineqdoc | Comment;;
  51
  52 (*
  53    Clusterlp means they enter the GLPK calcs for the cluster
  54    inequality.
  55
  56    Marchal means they enter the non-negativity estimate for clusters
  57    of Marchal cells.
  58
  59    Tablelp means they enter the LP calcs for the A and B tables in
  60    the definition of Tame h.
  61
  62    Flypaper means an inequality cited directly in the flypaper
  63    text. The tags are the citation names in the book.
  64
  65    Further means that it is not part of the Flyspeck project, but
  66    part of one of the extension theorems: StrongDodec, Fejes
  67    Toth's contact conjecture, or Musin-Tarasov.
  68
  69    Fejestoth means that it is part of the proof of the Fejes Toth's contact conjecture,
  70    but not part of the proof of the Kepler conjecture
  71
  72    Strongdodec means that it is part of the proof of the strong dodec conjecture,
  73    but not part of the proof of the Kepler conjecture
  74
  75    The TeX flag means that the doc field is Tex'able code (with
  76    software_guide.tex context).
  77
  78    CFSQP TAGS:
  79    Cfsqp means that there is cfsqp nonlinear optimization code to
  80    test it by gradient descent.
  81
  82    Cfsqp_branch uses this disjunct as the objective function,
  83    the others as constraints.
  84    The default is disjunct 0.
  85
  86    Eps is a small epsilon that is added to numerical testing to
  87    avoid answers neg. by machine eps.
  88
  89    Penalty implements a penalty method in cfsqp.
  90
  91    The floats (ub,wt) give the upper bound on the penalty term and its
  92    weight.
  93
  94    LINEAR PROGRAMMING TAGS:
  95    Lp gives an instruction to generate a MathProg inequality for the
  96    GLPK program to eliminate tame hypermaps.
  97
  98    Lp_aux are use to prove the Lp inequalities, but are not themselves Lp.
  99
 100    Lpsymmetry gives an instruction to generate a second MathProg
 101    inequality by symmetry.  y2 <-> y3, y5 <-> y6.  The domain must
 102    already be symmetrical, otherwise an error results.
 103
 104    INTERVAL ARITHMETIC TAGS:
 105    Derived means that it is not a primitive inequality, but rather a
 106    logical consequence of others.
 107
 108    Main_estimate  inequalities for TameTableD and related AD HOC
 109    linear programming inequalities.  These appear in the Local Fan
 110    chapter of flypaper.
 111
 112    Xconvert means to use the squared variables "x1...x6" rather than
 113    "y1..y6" when doing the nonlinear verification.
 114
 115    Split is an instruction to the nonlinear ineq verification to split
 116    the indicated variables (at 2 h0).  This is needed on piecewise differentiable
 117    functions (namely, lmfun) to restrict to differentiable domains.
 118
 119    Sharp means that equality is attained.
 120
 121    Disallow_derivatives means that verification should not use first derivative
 122    sign to slide to an edge of the domain.
 123
 124    Onlycheckderiv1negative means that it is not the function itself that should be
 125    verified, but only the first derivative of the first conjunct should be checked to
 126    be negative.  This is useful in monotonicity results.
 127
 128    Dim_red means that dimension reduction can be used on a quad cluster.
 129
 130    Dim_red_backsym means that dimension reduction can be used on a
 131    quad cluster.  It is assumed that the function on the back simplex is taum.
 132    It takes the following form x8,x9 are both extremal, if both
 133    are as long as possible, then x7 is as short as possible.  Also x1
 134    is minimal or x5 is minimal (eliminating x6 minimal by a symmetry
 135    5-6,2-3,8-9 ).  The reductions also use ineq 4828966562 to assume
 136    that the diagonal y4 is at most 3.01 when both x5 and x6 are extremal.
 137
 138    Quad_cluster is an ineq on a coupled pair of simplices. The float
 139    is the margin value for "breaksapart".
 140
 141    Set_rad2 means the circumradius can be assumed to be exactly sqrt2.
 142
 143    Delta126min is a lower bound on delta_x x1 x2 (&2) (&2) (&2) x6
 144
 145    Delta126max is an upper bound on delta_x x1 x2 (&2) (&2) (&2) x6
 146
 147    Delta135min is a lower bound on delta_x x1 (&2) x3 (&2) x5 (&2).
 148
 149    Delta135max is an upper bound on delta_x x1 (&2) x3 (&2) x5 (&2).
 150
 151 (*   Set298 is a special tag for the inequality 2986512815. *)
 152
 153 *)
 154