legacy/oldnonlinear/nonlinear/main_estimate_pent_hex_cut_may_2013.hl

   1 addtex(Comment,"","
   2 The actual definitions of these functions need to be supplied.
   3 For now, the functions only get used in cfsqp and interval verifications.
   4
   5 The LC functions are implemented in intervals as locally constant functions.
   6 ");;
   7
   8 (* true definitions in mdtau.hl *)
   9
  10
  11 let mdtau_fake = new_definition
  12   `mdtau (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real)  = &0`;;
  13
  14 let mdtau2_fake = new_definition
  15   `mdtau2 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real)  = &0`;;
  16
  17 addtex (Section,"Main Estimate","Ears, top edges 2,2,long");;
  18
  19
  20 add
  21 {
  22   idv="4322269127";
  23   doc="taum 1st deriv test.
  24    This shows that the first derivative of tau (wrt y1) is nonzero.
  25   Thus the  optimal configuration has delta > 15 or (y1 minimal = 2)
  26    It is implemented in interval code, using locally constant structures (LC).";
  27   tags=[Flypaper["TNNOPSI"];Main_estimate;Tex;Disallow_derivatives;Penalty(50.0,500.0);];
  28   ineq = all_forall `ineq [
  29     (&2,y1,#2.52);
  30     (#2.0,y2,#2.52);
  31     (&2,y3,#2.52);
  32     (#3.01,y4,#3.915);
  33     (&2,y5,&2);
  34       (&2,y6,&2)
  35   ]
  36 (
  37   ( mdtau_y_LC y1 y2 y3 y4 y5 y6  > &0) \/
  38   ( mdtau_y_LC y1 y2 y3 y4 y5 y6  < &0) \/
  39   (delta_y_LC y1 y2 y3 y4 y5 y6 > &15) \/
  40   (delta_y_LC y1 y2 y3 y4 y5 y6 < &0)
  41  )`;
  42 };;
  43
  44 skip
  45 {
  46   idv="4322269127 cfsqp version";
  47   doc="taum 1st deriv test.  This is the cfsqp version of 4322269127.
  48     It is not to be proved, only used as numerical evidence.";
  49   tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
  50   ineq = all_forall `ineq [
  51     (&2,y1,#2.52);
  52     (#2.0,y2,#2.52);
  53     (&2,y3,#2.52);
  54     (#3.01,y4,#3.915);
  55     (&2,y5,&2);
  56       (&2,y6,&2)
  57   ]
  58 (
  59   ( mdtau y1 y2 y3 y4 y5 y6 pow 2 > #0.47) \/ // fake
  60   (delta_y y1 y2 y3 y4 y5 y6 > &15) \/
  61   (delta_y y1 y2 y3 y4 y5 y6 < &0)
  62  )`;
  63 };;
  64
  65
  66 add
  67 {
  68   idv="5556646409";
  69   doc="taum 2nd deriv test.  This is a key inequality.
  70    It asserts that taum has no local minimum on the given domain.
  71    If the derivative is zero, then the second derivative is negative.
  72    By symmetry, wlog y2 < y3.
  73    The C++ code has been customized for this particular inequality.
  74    The C++ has an embedded assumption that mdtau2_y_LC is on the domain delta>=15.
  75    Case delta<=15 is done in 4322269127.
  76    ";
  77   tags=[Flypaper["TNNOPSI"];Main_estimate;Tex;Disallow_derivatives;Widthcutoff 0.004;Penalty(1500.0,5000.0);Cfsqp_branch 2];
  78   ineq = all_forall `ineq [
  79     (&2,y1,#2.52);
  80     (#2.0,y2,#2.52);
  81     (&2,y3,#2.52);
  82     (#3.01,y4,#3.915);
  83     (&2,y5,&2);
  84       (&2,y6,&2)
  85   ]
  86 (
  87   (delta_y_LC y1 y2 y3 y4 y5 y6 < &15) \/
  88  (y2 < y3) \/
  89   (mdtau_y_LC  y1 y2 y3 y4 y5 y6  > &0) \/
  90   (mdtau_y_LC  y1 y2 y3 y4 y5 y6  < &0) \/
  91   (mdtau2uf_y_LC y1 y2 y3 y4 y5 y6 < &0)
  92  )`;
  93 };;
  94
  95 skip
  96 {
  97   idv="5556646409 cfsqp version";
  98   doc="taum 2nd deriv test. Cfsqp version -- only for testing.";
  99   tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Tex;Penalty(1500.0,5000.0);Deprecated];
 100   ineq = all_forall `ineq [
 101     (&2,y1,#2.52);
 102     (#2.0,y2,#2.52);
 103     (&2,y3,#2.52);
 104     (#3.01,y4,#3.915);
 105     (&2,y5,&2);
 106       (&2,y6,&2)
 107   ]
 108 (
 109   (mdtau y1 y2 y3 y4 y5 y6 pow 2 > #0.004) \/ // fake
 110   (mdtau2 y1 y2 y3 y4 y5 y6 < -- #0.004) \/  // fake
 111   (delta_y y1 y2 y3 y4 y5 y6 < &15)
 112  )`;
 113 };;
 114
 115 skip
 116 {
 117   idv="5132343267";
 118   doc="delta monotonicity.
 119    In the interval code for 5556646409,
 120    the interval implementation of delta_y_LC assumes this  monotonicity
 121     results.  This calculation is not cited explicitly in the code, but still needed.
 122   -
 123    Deprecated.  This is a consequence of 4559601669, which asserts that
 124    the wide angle of a skinny triangle (ear) is obtuse.";
 125   tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
 126   ineq = all_forall `ineq [
 127     (&2,y1,#2.52);
 128     (#2.0,y2,#2.52);
 129     (&2,y3,#2.52);
 130     (#3.01,y4,#3.915);
 131     (&2,y5,&2);
 132       (&2,y6,&2)
 133   ]
 134 (
 135   ( delta4_y y1 y2 y3 y4 y5 y6 < &0)
 136  )`;
 137 };;
 138
 139 skip
 140 {
 141   idv="7479785942";
 142   doc="delta monotonicity (for edge y5 and by symmetry y6).
 143    In the interval code for 5556646409,
 144    the interval implementation of delta_y_LC assumes various  monotonicity
 145     results.  This is among them.
 146     -
 147    This is a consequence of 2485876245. No separate verification is needed.
 148   ";
 149   tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
 150   ineq = all_forall `ineq [
 151     (&2,y1,#2.52);
 152     (#2.0,y2,&2);
 153     (&2,y3,&2);
 154     (&2,y4,#2.52);
 155     (#3.01,y5,#3.915);
 156       (&2,y6,#2.52)
 157   ]
 158 (
 159   ( delta4_y y1 y2 y3 y4 y5 y6 > &0)
 160  )`;
 161 };;
 162
 163 addtex (Section,"Main Estimate","June Hexagons, top edges all 2.");;
 164
 165 addtex(Comment,"Main Estimate",
 166 "
 167 ");;
 168
 169 add
 170 {
 171   idv="5338748573";
 172   doc="full hexagon with three alternating flats.
 173     Big alternating central triangle.
 174     Symmetries, wlog y1<y2<y3.
 175     y4 y5 y6 are non-standard indexing of variables.
 176     They are the heights of the enclosed flat nodes.
 177     ";
 178   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 179   ineq = all_forall `ineq [
 180     (&2,y1,#2.52);
 181     (&2,y2,#2.52);
 182     (&2,y3,#2.52);
 183       (&2,y4,#2.52);
 184       (&2,y5,#2.52);
 185     (&2,y6,#2.52)
 186   ]
 187 (
 188   (y_of_x taum_3flat_x y1 y2 y3 y4 y5 y6 > #0.712 ) \/
 189     (y_of_x euler_3flat_x y1 y2 y3 y4 y5 y6 < &0) \/
 190     (y2 < y1) \/ (y3 < y2)
 191  )`;
 192 };;
 193
 194 add
 195 {
 196   idv="3306409086";
 197   doc="full hexagon with two flats, one hi, can zero out the hi ear.
 198     Big alternating central triangle.
 199     By symmetry wlog y5 < y6
 200     The constant 0.013 comes from 2535350075.
 201     We add constant in on the hi case, even though it isn't needed here.
 202     To permit simplification of the lo case later.
 203     ";
 204   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 205   ineq = all_forall `ineq [
 206     (&2,y1,#2.52);
 207     (&2,y2,#2.52);
 208     (&2,y3,#2.52);
 209       (#3.01,y4,#3.915);
 210       (&2,y5,#2.52);
 211     (&2,y6,#2.52)
 212   ]
 213 (
 214   (y_of_x taum_2flat_x y1 y2 y3 y4 y5 y6
 215     > #0.712 + #0.013) \/
 216    y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 217      (y_of_x euler_2flat_x y1 y2 y3 y4 y5 y6<  &0)  \/
 218    (y6 < y5)
 219  )`;
 220 };;
 221
 222 add
 223 {
 224   idv="9075398267";
 225   doc="full hexagon with two flats, one lo
 226     Big alternating central triangle.
 227    To stabilize near delta=0, we  erases and takes a penalty.
 228     By symmetry, wlog  y5 < y6.
 229     The constant 0.013 comes from 2535350075.
 230     The extra disjuncts are justified by that calc and by
 231     the stronger ineq proved in '3306...'
 232     ";
 233   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 234   ineq = all_forall `ineq [
 235     (&2,y1,#2.52);
 236     (&2,y2,#2.52);
 237     (&2,y3,#2.52);
 238       (#3.01,y4,#3.915);
 239      (&2,y5,#2.52);
 240     (&2,y6,#2.52)
 241    ]
 242 (
 243   (y_of_x taum_2flat_x y1 y2 y3 y4 y5 y6
 244    > #0.712 + sol0) \/
 245   y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 246     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 247      ( y_of_x euler_2flat_x y1 y2 y3 y4 y5 y6<  &0) \/
 248    (y6 < y5)
 249  )`;
 250 };;
 251
 252 add
 253 {
 254   idv="1324821088";
 255   doc="full hexagon with one flat, hi,hi, can zero out both ears.
 256     Big alternating central triangle.
 257     By symmetry, wlog y4 < y5.
 258    The constant 0.013 comes from 2535350075.
 259     We add constant in on the hi case, even though it isn't needed here.
 260     To permit simplification of the lo case later.
 261     ";
 262   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 263   ineq = all_forall `ineq [
 264     (&2,y1,#2.52);
 265     (&2,y2,#2.52);
 266     (&2,y3,#2.52);
 267       (#3.01,y4,#3.915);
 268    (#3.01,y5,#3.915);
 269       (&2,y6,#2.52)
 270   ]
 271 (
 272   (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6  > #0.712 + &2 * #0.013) \/
 273   y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 274   y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 275   y5 < y4 \/
 276      ( y_of_x euler_1flat_x y1 y2 y3 y4 y5 y6< &0)
 277  )`;
 278 };;
 279
 280 add
 281 {
 282   idv="4108834026";
 283   doc="full hexagon with one flat, ears: hi,lo, can zero  out hi ear.
 284     Big alternating central triangle.
 285    To stabilize near delta=0, we add  a disjunct that erases and takes a penalty.
 286     The constant 0.013 comes from 2535350075.
 287     The extra disjuncts are justified by that calc and by
 288     the stronger ineq proved in '132482...'
 289     ";
 290   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 291   ineq = all_forall `ineq [
 292     (&2,y1,#2.52);
 293     (&2,y2,#2.52);
 294     (&2,y3,#2.52);
 295       (#3.01,y4,#3.915);
 296    (#3.01,y5,#3.915);
 297       (&2,y6,#2.52)
 298   ]
 299 (
 300   (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6 +
 301  y_of_x (taum_sub246_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  > #0.712 + #0.013) \/
 302  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6  > #0.712 + #0.013 + sol0) \/
 303   y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 304      y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 305      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
 306      (y_of_x euler_1flat_x y1 y2 y3 y4 y5 y6< &0)
 307  )`;
 308 };;
 309
 310 add
 311 {
 312   idv="6388508112";
 313   doc="full hexagon with one flat, ears: lo,lo
 314     Big alternating central triangle.
 315     If delta hi>0, take the penalty and erase.
 316     By symmetry, wlog 0  < delta234 < delta135
 317     To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
 318     ";
 319   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 320   ineq = all_forall `ineq [
 321     (&2,y1,#2.52);
 322     (&2,y2,#2.52);
 323     (&2,y3,#2.52);
 324       (#3.01,y4,#3.915);
 325    (#3.01,y5,#3.915);
 326       (&2,y6,#2.52)
 327   ]
 328 (
 329   (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6 +
 330       y_of_x (taum_sub246_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 >
 331    #0.712 + sol0) \/
 332   (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6
 333    > #0.712 + &2 * sol0) \/
 334   y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 335   y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 336     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  <
 337  y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
 338     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
 339      ( y_of_x euler_1flat_x y1 y2 y3 y4 y5 y6< &0)
 340  )`;
 341 };;
 342
 343
 344 add
 345 {
 346   idv="5493250206";
 347   doc="full hexagon with no flats, three ears: hi,hi,hi, can zero out all ears.
 348     Big alternating central triangle.
 349     By symmetry y1 < y2 < y3
 350     ";
 351   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 352   ineq = all_forall `ineq [
 353     (&2,y1,#2.52);
 354     (&2,y2,#2.52);
 355     (&2,y3,#2.52);
 356       (#3.01,y4,#3.915);
 357    (#3.01,y5,#3.915);
 358    (#3.01,y6,#3.915)
 359   ]
 360 (  (taum y1 y2 y3 y4 y5 y6
 361     > #0.712 + &3 * #0.013) \/
 362    y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 363      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 364      y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 365      ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/
 366     (y2 < y1) \/ (y3 < y2)
 367  )`;
 368 };;
 369
 370 add
 371 {
 372   idv="2283016857";
 373   doc="full hexagon with no flats, three ears: hi,hi,lo=126, zero out hi ears.
 374     Big alternating central triangle, extremal ears.
 375     To stabilize near delta=0, we add  a disjunct that erases and takes a penalty.
 376     By symmetry, y4<y5.
 377     ";
 378   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 379   ineq = all_forall `ineq [
 380     (&2,y1,#2.52);
 381     (&2,y2,#2.52);
 382     (&2,y3,#2.52);
 383       (#3.01,y4,#3.915);
 384    (#3.01,y5,#3.915);
 385    (#3.01,y6,#3.915)
 386   ]
 387 (  (taum y1 y2 y3 y4 y5 y6  +
 388 y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
 389     > #0.712 + &2 * #0.013) \/
 390  (taum y1 y2 y3 y4 y5 y6
 391     > #0.712 + &2 * #0.013 + sol0) \/
 392     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 393      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 394     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 395      y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6> &0  \/
 396      ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y5 < y4)
 397  )`;
 398 };;
 399
 400 add
 401 {
 402   idv="4872337467";
 403   doc="full hexagon with no flats, three ears: hi,lo,lo, zero out hi  ear.
 404     Big alternating central triangle, extremal ears.
 405     By symmetry, wlog 0  < delta135 < delta126
 406     To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
 407     ";
 408   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 409   ineq = all_forall `ineq [
 410     (&2,y1,#2.52);
 411     (&2,y2,#2.52);
 412     (&2,y3,#2.52);
 413       (#3.01,y4,#3.915);
 414    (#3.01,y5,#3.915);
 415    (#3.01,y6,#3.915)
 416   ]
 417 (
 418  (taum y1 y2 y3 y4 y5 y6  +
 419 y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
 420     > #0.712 + #0.013 + sol0) \/
 421  (taum y1 y2 y3 y4 y5 y6
 422     > #0.712 + #0.013 + &2 * sol0) \/
 423      y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6  < &0  \/
 424      y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0  \/
 425      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
 426     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 <
 427  y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
 428      y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
 429      ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
 430  )`;
 431 };;
 432
 433 add
 434 {
 435   idv="3615835903";
 436   doc="full hexagon with no flats, three ears: low, low, low
 437     Big alternating central triangle, extremal ears.
 438     By symmetry, wlog, we may order the delta terms.
 439     0 < delta234 < delta135 < delta126
 440     To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
 441     ";
 442   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 443   ineq = all_forall `ineq [
 444     (&2,y1,#2.52);
 445     (&2,y2,#2.52);
 446     (&2,y3,#2.52);
 447       (#3.01,y4,#3.915);
 448    (#3.01,y5,#3.915);
 449    (#3.01,y6,#3.915)
 450   ]
 451 (
 452 (taum y1 y2 y3 y4 y5 y6  +
 453 y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
 454     > #0.712 + &2 * sol0) \/
 455 (taum y1 y2 y3 y4 y5 y6
 456     > #0.712 + &3 * sol0) \/
 457     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  < &0  \/
 458    y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
 459     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 <  y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6   \/
 460      y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
 461     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 <
 462   y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
 463     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
 464      ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
 465  )`;
 466 };;
 467
 468
 469 add
 470 {
 471   idv="2535350075";
 472   doc="full hexagon ear calculation.
 473    This shows that if (delta hi > 0) and (delta lo >0) we can erase the ear with small penalty.
 474    Hence, when we look at a lo ear, we can wrap it in with the hi ear case when
 475    the hi ear exists: (delta hi>0).
 476    By symmetry, wlog y2 < y3.
 477     ";
 478   tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 479   ineq = all_forall `ineq [
 480     (&2,y1,&2);
 481     (&2,y2,#2.52);
 482     (&2,y3,#2.52);
 483     (#3.01,y4,#3.915);
 484     (&2,y5,&2);
 485     (&2,y6,&2)
 486   ]
 487 (
 488  (taum y1 y2 y3 y4 y5 y6   > -- #0.013) \/
 489     (y_of_x (delta_sub1_x (#2.52 pow 2)) y1 y2 y3 y4 y5 y6 < &0) \/
 490     (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y3 < y2)
 491  )`;
 492 };;
 493
 494 addtex (Section,"Main Estimate","Pentagons, all top edges 2");;
 495 (* New Pentagons,  June 3, 2011.
 496  This section completely treats all kinds of
 497    pentagons, modulo cases with a diagonal <= 3.01.  *)
 498
 499
 500 add
 501 {
 502   idv="7067938795";
 503   doc="A pentagon cannot have two straights.  This is the A-piece dihedral bound.
 504     If a pentagon has two straights then
 505      pi /2 < dih y1 _ _ 3.01 2 2 < dih_y.  This is impossible, by this calc.
 506     This estimate also gets used on straight+hi.";
 507   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
 508   ineq = all_forall `ineq [
 509     (&2,y1,#2.52);
 510     (&2,y2,#2.52);
 511     (&2,y3,#2.52);
 512     (&2,y4,&2);
 513     (#3.01,y5,#3.24);
 514       (#3.01,y6,#3.24)
 515   ]
 516 (
 517   ( dih_y y1 y2 y3 y4 y5 y6 < pi / &2 - #0.46)
 518  )`;
 519 };;
 520
 521
 522 add
 523 {
 524   idv="9459075374";
 525   doc="(EAR) A bound on the delta of an ear in a pent, when the pent has a straight on the other side.
 526    The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #0.46)  has been 'linearized'.
 527    Tan[0.46]^2 = 0.245469...
 528    In more detail, this calc shows that delta > 30.2 or dih < 0.46.
 529    By obtuse calcs, we know that the combined angle at the node is
 530    at least pi/2.  If we have a straight node, and dih < 0.46, then
 531    the combined angle is less than 0 + 0.46 + (pi/2 - 0.46) =pi/2 by
 532    '7067938795'.  Hence a flat on the other side ==> delta of this ear > 30.2.
 533    ";
 534   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
 535   ineq = all_forall `ineq [
 536     (&2,y1,#2.52);
 537     (#2.52,y2,#2.52);
 538     (&2,y3,#2.52);
 539     (&2,y4,&2);
 540      (#3.01,y5,#3.24);
 541       (&2,y6,#2.52)
 542   ]
 543 (let tan2lower = #0.245468 in
 544    (delta_y y1 y2 y3 y4 y5 y6 > #30.2) \/
 545   (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)
 546  )`;
 547 };;
 548
 549
 550 add
 551 {
 552   idv="2559885109";
 553   doc="(EAR) A pentagon lo ear bound";
 554   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
 555   ineq = all_forall `ineq [
 556     (&2,y1,&2);
 557     (&2,y2,#2.52);
 558     (&2,y3,#2.52);
 559     (#3.01,y4,#3.24);
 560     (&2,y5,&2);
 561       (&2,y6,&2)
 562   ]
 563 (
 564   ( taum y1 y2 y3 y4 y5 y6 > &0)
 565  )`;
 566 };;
 567
 568 add
 569 {
 570   idv="9861833891";
 571   doc="pent+hi+something that we can zero out.
 572     This and '8199484193' do the case of no straight nodes.
 573     ";
 574   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 575   ineq = all_forall `ineq [
 576     (&2,y1,#2.52);
 577     (&2,y2,#2.52);
 578     (&2,y3,#2.52);
 579    (&2,y4,&2);
 580     (#3.01,y5,#3.24);
 581       (#3.01,y6,#3.24)
 582   ]
 583 ( taum y1 y2 y3 y4 y5 y6 +
 584     y_of_x (taum_sub345_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6  > #0.616 \/
 585   taum y1 y2 y3 y4 y5 y6   > #0.616
 586  )`;
 587 };;
 588
 589 add
 590 {
 591   idv="8199484193";
 592   doc="pent+lo+something that we can zero out.
 593     (We can zero out anything but a straight node.)
 594     This and '9861833891' do the case of no straight nodes.
 595     ";
 596   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 597   ineq = all_forall `ineq [
 598     (&2,y1,#2.52);
 599     (&2,y2,#2.52);
 600     (&2,y3,#2.52);
 601    (&2,y4,&2);
 602     (#3.01,y5,#3.24);
 603       (#3.01,y6,#3.24)
 604   ]
 605 ( taum y1 y2 y3 y4 y5 y6 +
 606    y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
 607    > #0.616
 608  )`;
 609 };;
 610
 611
 612 add
 613 {
 614   idv="3980286827";
 615   doc="pent+straight126+lo
 616   The delta_pent >0 iff  edge_flat y6 y1 y2  _   (&2) (&2) > #3.24
 617   The straight goes along 126.
 618   the low is placed along 135.
 619   The variable called y6 is in fact the ht of enclosed straight node
 620   along the (1,2,6) face.  The edge |v1-v2| is computed by taum_1flat.
 621    delta_pent_x = delta_x x1 x2 x6 4 4 3.24^2.
 622     ";
 623   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 624   ineq = all_forall `ineq [
 625     (&2,y1,#2.52);
 626     (&2,y2,#2.52);
 627     (&2,y3,#2.52);
 628    (&2,y4,&2);
 629     (#3.01,y5,#3.24);
 630       (&2,y6,#2.52)
 631   ]
 632 ( y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6 +
 633    y_of_x (taum_sub246_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
 634      > #0.616 \/
 635    y_of_x (delta_pent_x) y1 y2 y3 y4 y5 y6 > &0
 636  )`;
 637 };;
 638
 639 add
 640 {
 641   idv="3221740746 a";
 642   doc="pent+straight126+hi
 643    delta_pent_x = delta_x x1 x2 x6 4 4 3.24^2.
 644     has non-standard ordering of variables, x3<->x6.
 645     y6 = ht of the straight node on the y1-y2-* face.
 646     ";
 647   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;
 648       Xconvert;Tex;Penalty(500.0,5000.0)];
 649   ineq = all_forall `ineq [
 650     (&2,y1,#2.52);
 651     (&2,y2,#2.52);
 652     (&2,y3,#2.52);
 653    (&2,y4,&2);
 654     (#3.01,y5,#3.24);
 655       (&2,y6,#2.52)
 656   ]
 657 ( y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6 +
 658      y_of_x (taum_sub246_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.616 \/
 659     (y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < #30.2) \/
 660     y_of_x (delta_pent_x) y1 y2 y3 y4 y5 y6 > &0
 661  )`;
 662 };;
 663
 664 (* We have finished the main part of the verification of pents.
 665    These last calculations show that none of the three nodes on
 666    the big inner triangle can be straight.  So we don't need to
 667    worry about this, when making calculations. *)
 668
 669 add
 670 {
 671   idv="8520556953";
 672   doc="(EAR) no straights on vertices of big inner triangle of pent.
 673   This is the skinny triangle (ear) bound.
 674    Upper bound on y6 is 1+Sqrt[5].
 675    Need to do a dih replacement.
 676    Tan[1.001]^2 > 2.43621.
 677    The disjunct implies dih < #1.001.
 678     Combine this with '9977174768'
 679     ";
 680   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
 681   ineq = all_forall `ineq [
 682     (&2,y1,#2.52);
 683     (&2,y2,#2.52);
 684     (&2,y3,#2.52);
 685     (&2,y4,&2);
 686     (&2,y5,&2);
 687       (#3.01,y6,#3.23607)
 688   ]
 689 (
 690   let tan2lower = #2.43621 in
 691   ( &4 * x1_delta_y  y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
 692   (delta_y y1 y2 y3 y4 y5 y6 < &0)
 693  )`;
 694 };;
 695
 696 add
 697 {
 698   idv="9977174768";
 699   doc="no straight nodes on big inner triangle of pent.
 700    Upper bound on y6 is 1+Sqrt[5].
 701       Tan[1.001]^2 > 2.43621.
 702    The disjunct implies dih < pi - #1.001.
 703    Combine this with '8520556953'.
 704     ";
 705   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
 706   ineq = all_forall `ineq [
 707     (&2,y1,#2.52);
 708     (&2,y2,#2.52);
 709     (&2,y3,#2.52);
 710     (#3.01,y4,#3.23607);
 711     (&2,y5,&2);
 712       (#3.01,y6,#3.23607)
 713   ]
 714 ( dih_y y1 y2 y3 y4 y5 y6 < pi - #1.001)`;
 715 };;
 716
 717
 718 skip
 719 {
 720   idv="6281973111";
 721   doc="no straight node on big inner triangle of pent.
 722    Upper bound on y6 is 1+Sqrt[5].
 723    Moved to skipped May 26, 2012.  It is a special case of '7067938795'
 724    This is used to prove that the node of the pentagon with three
 725    triangles is not straight:
 726      (pi - 2 1.001) + 1.001 + 1.001 <= pi.)
 727     ";
 728   tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
 729   ineq = all_forall `ineq [
 730     (&2,y1,#2.52);
 731     (&2,y2,#2.52);
 732     (&2,y3,#2.52);
 733     (&2,y4,&2);
 734     (#3.01,y5,#3.23607);
 735       (#3.01,y6,#3.23607)
 736   ]
 737 (
 738   ( dih_y y1 y2 y3 y4 y5 y6 < pi - &2 * #1.001)
 739  )`;
 740 };;
 741
 742 Functional_equation.functional_overload();;
 743
 744 (* May 9, 2013. taud function.  taud_v4 seems to be the version that
 745    works in all cases (pent and hex).  *)
 746
 747
 748     let add = Ineq.add;;
 749
 750     let skip = Ineq.skip;;
 751
 752     let all_forall = Sphere.all_forall;;
 753
 754
 755 run
 756 {
 757   idv="test";
 758   doc="
 759     local fan/main estimate/terminal pent
 760     LHS(135,delta=20) RHS(126,delta=0)
 761     ";
 762   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 763   ineq = all_forall `ineq [
 764     (&2,y1,#2.52);
 765     (&2,y2,#2.52);
 766     (&2,y3,#2.52);
 767     (&2,y4,&2);
 768     (#3.01,y5,#3.237);
 769     (#3.01,y6,#3.237)
 770   ]
 771 (
 772     ((taum y1 y2 y3 y4 y5 y6 +
 773        y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 774        y_of_x mu6_x
 775 //       y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
 776      > #0.616) \/
 777       y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
 778 `;
 779 };;
 780
 781
 782
 783
 784
 785 (* Scratch area *)
 786
 787 (*
 788 let runhh i234 i126 i135 = try (run(make_hex_ear i234 i126 i135)) with _ -> () ;;
 789 let run2hh i234 i126 i135 = try (
 790   let _ = run2(make_hex_ear i234 i126 i135) in ()) with _ -> () ;;
 791
 792 *)
 793
 794
 795
 796 let install_functions () =
 797   let _ = map Parse_ineq.autogen_add [mu_y;delta_x1;taud;] in
 798   let _ = map Parse_ineq.macro_add[ mud_135_x;
 799                               mud_126_x;mud_234_x;mudLs_234_x;mudLs_135_x;mudLs_126_x;
 800                               taud_x;nonfunctional_mu6_x;nonfunctional_taud_D1;
 801                             nonfunctional_taud_D2;
 802                             nonfunctional_edge2_126_x;
 803                             nonfunctional_edge2_135_x;
 804                             nonfunctional_edge2_234_x;
 805                             flat_term2_126_x;
 806                                        flat_term2_135_x;flat_term2_234_x] in
 807   let _ = map Function_list.function_add
 808     [ functional_delta_x1;mu6_x;taud_x_ALT;taud_D2_num_x;taud_D1_num_x;
 809     functional_mud_135_x;functional_mud_126_x;functional_mud_234_x;mudLs_234_x;mudLs_126_x;mudLs_135_x;
 810     ups_126;
 811     functional_edge2_126_x;functional_edge2_135_x;functional_edge2_234_x;
 812     flat_term2_126_x;flat_term2_135_x;flat_term2_234_x] in
 813     "remember to reload Auto_lib, etc.";;
 814
 815 (*
 816     map Parse_ineq.autogen_remove [edge_flatD_x1;taud_v4_D2_num;taud;taud_D2_num_x];;
 817     map Parse_ineq.macro_remove [taud_D2_num_x;edge_126_x;edge_135_x;
 818                                  functional_edge_135_x;flat_term_126_x;flat_term_135_x;
 819                                 functional_edge_126_x;mudd_135_x;mudd_126_x;
 820       mudd_135_x_v2;mudd_126_x_v2;
 821 ];;
 822
 823    map Function_list.function_remove [mu_y;taud_x;delta_x1;functional_edge_126_x;
 824                                        functional_edge_135_x;];;
 825 *)
 826
 827
 828 Parse_ineq.autogen_remove mudL_234_x;;
 829 Function_list.function_remove mudL_234_x;;
 830 1;;
 831
 832
 833 (*
 834
 835 flyspeck_needs "nonlinear/scripts.hl";;
 836
 837     let run s =
 838       let _ = Ineq.add s in
 839         Scripts.one_cfsqp s.idv;;
 840
 841     rflyspeck_needs   "nonlinear/auto_lib.hl";;
 842
 843     let run2 s =
 844       let _ = Ineq.add s in
 845         Auto_lib.testsplit true s.idv;;
 846
 847     let run2f s =
 848       let _ = Ineq.add s in
 849         Auto_lib.testsplit false s.idv;;
 850
 851
 852
 853 Auto_lib.testsplit true "7796879304";;
 854 map (Auto_lib.testsplit true)  cases;;
 855
 856
 857 map Scripts.one_cfsqp cases;;
 858 *)
 859
 860 map (Auto_lib.testsplit true) ["test U1";"test U2";"test U3";
 861 "test U4";"test U5";"test U6";
 862 "test U7";"test U8";"test U9";
 863 "test U10";];;
 864
 865