legacy/oldnonlinear/nonlinear/break_quad_jul2013.hl

   1 (* ************************************************************************** *)
   2 (* July 2013.
   3    T. Hales
   4    Notes on breaking up the quadrilateral inequalities in ineq.hl into pieces of at most
   5    6 variables.
   6 *)
   7 (* ************************************************************************** *)
   8
   9
  10 (* ************************************************************************** *)
  11 (* INEQ "3862621143 revised" *)
  12 (* ************************************************************************** *)
  13
  14 (*
  15 This inequality is not quite in final form. The inequalities are still too slow.
  16 *)
  17
  18 (* If dih < 2.15 then Main-inequality d(4) implies the result. WLOG dih > 2.15. *)
  19
  20 (*
  21 One way to break up quad 386..revised appears in the following inequalities.
  22 Another approach:
  23 Change num1 lower bound from 2.38 to 2.9/h0.  Then both back edges can
  24 be deformed to 2.  Even the front edges can be deformed to 2, by obtuseness of front angle
  25 and the sign of dih in the inequality.  So all top edges=2.
  26 This is contrary to the diagonal constraints in 386...revised.
  27 *)
  28
  29 run
  30   {
  31     idv="test dih";
  32     doc = "The denominator should be cleared, upper bound increased to &4*h0, delta_y bound made 0";
  33     tags=[];
  34   ineq = Sphere.all_forall `ineq
  35       [
  36          (&2,y1,&2 * h0);
  37          (&2,y2,&2 * h0);
  38          (&2,y3,&2 * h0);
  39          (&2,y4,&2 * h0);
  40          (#3.9,y5,#4.2);
  41          (&2,y6,&2 * h0)]
  42       (
  43        dih_y y1 y2 y3 y4 y5 y6 < #2.15 / &2 \/
  44        delta_y y1 y2 y3 y4 y5 y6 < #0.1)`;
  45   };;
  46
  47 run
  48 {
  49   idv="test dih 2";
  50   doc="
  51     (EAR) A bound on the dih of an ear in a quad,
  52    The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #2.15 / &2  has been 'linearized'.
  53    Tan[2.15 / 2]^2 = (>=) 3.418
  54    In more detail, this calc shows that delta > 0 or dih < 2.15 / 2
  55    ";
  56   tags=[Xconvert;];
  57   ineq = Sphere.all_forall `ineq [
  58          (&2,y1,&2 * h0);
  59          (&2,y2,&2 * h0);
  60          (&2,y3,&2 * h0);
  61          (&2,y4,&2 * h0);
  62          (#3.9,y5,&4 * h0);
  63          (&2,y6,&2 * h0)]
  64 (let tan2lower = #3.418 in
  65    ((&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
  66       delta_y y1 y2 y3 y4 y5 y6 < &0))`;
  67 };;
  68
  69
  70 (* an ineq in main_estimate_ineq.hl, gives that both sides are acute. when cross_diag > 3.01 *)
  71
  72 run2
  73   {
  74     idv="test side azim 3862621143";
  75     doc = "This allows us to restrict the domain on both sides to delta > 16.
  76      Tan[2.15 - Pi/2]^2 >= 0.4277.
  77      Too slow!! (992 secs).
  78      ";
  79     tags=[Xconvert];
  80   ineq = Sphere.all_forall `ineq
  81       [
  82          (&2,y1,&2 * h0);
  83          (&2,y2,&2 * h0);
  84          (&2,y3,&2 * h0);
  85          (&2 ,y4, &2 * h0);
  86          (#3.01,y5,#3.9);
  87          (&2,y6,&2 * h0)]
  88 (let tan2lower = #0.4277 in
  89       (
  90         &4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
  91      //  dih_y y1 y2 y3 y4 y5 y6 < #2.15 - pi / &2 \/
  92        delta_y y1 y2 y3 y4 y5 y6 < &0 \/
  93        delta_y y1 y2 y3 y4 y5 y6 > &16)`;
  94   };;
  95
  96 run2
  97   {
  98     idv="test side' 3862621143";
  99     doc = "";
 100     tags=[Xconvert];
 101   ineq = Sphere.all_forall `ineq
 102       [
 103          (&2,y1,&2 * h0);
 104          (&2,y2,&2 * h0);
 105          (&2,y3,&2 * h0);
 106          (&2 ,y4, &2 * h0);
 107          (#3.01,y5,#3.9);
 108          (&2,y6,&2 * h0)]
 109       (taum y1 y2 y3 y4 y5 y6  > #0.453  * dih_y y1 y2 y3 y4 y5 y6 - #0.77 / &2 \/
 110          delta_y y1 y2 y3 y4 y5 y6 < &16  \/       dih_y y1 y2 y3 y4 y5 y6 < #2.15 - pi / &2
 111 )`;
 112   };;
 113
 114
 115 (* ************************************************************************** *)
 116 (* INEQ "4240815464 a" *)
 117 (* ************************************************************************** *)
 118
 119
 120 skip
 121   {
 122     idv="5365514595"; (* test full 4240815464 *)
 123     doc = "
 124      The following inequalities make 4240815464 into a derived inequality.
 125      If dih > 1.621, then the main_estimate d(4) inequality implies this, so wlog dih < 1.621.
 126      We may take y4 <= 3.36, for otherwise dih > 1.621.
 127      When 3.01 <= y4 <= 3.36, dih < 1.621 ==> Delta(back) > 98 ==> taum(back) > 0.
 128      We replace the back taum with 0, and run the 6D ineq on the front simplex.
 129      -
 130      When 2.62 <= y4 <= 3.01, use taum(back) >= 1.03. to remove the back simplex. Run on the front.
 131      -
 132      When 2.52 <= y4 <= 3.01, use a custom linear lower bound on tam(back) to remove the back simplex.
 133      -
 134      passes when we zero out back term. ";
 135     tags=[];
 136   ineq = Sphere.all_forall `ineq
 137       [
 138          (&2,y1,&2 * h0);
 139          (&2,y2,&2 * h0);
 140          (&2,y3,&2 * h0);
 141          (#3.01 ,y4, #3.36);
 142          (&2,y5,&2 * h0);
 143          (&2,y6,&2 * h0);
 144          (&2,y7,&2 * h0);
 145          (&2,y8,&2 * h0);
 146          (&2,y9,&2 * h0)
 147 ]
 148       (
 149         taum y1 y2 y3 y4 y5 y6  + taum y7 y2 y3 y4 y8 y9 +
 150           #0.7573 * dih_y y1 y2 y3 y4 y5 y6 - #1.433 > &0 \/
 151           dih_y y1 y2 y3 y4 y5 y6 > #1.621)`;
 152   };;
 153
 154 add
 155   {
 156     idv="3397113841"; (* test dih (delta4) 4240815464 *)
 157     doc = "Justifies linearized dih when y4 >= 3.36";
 158     tags=[Xconvert];
 159   ineq = Sphere.all_forall `ineq
 160       [
 161          (&2,y1,&2 * h0);
 162          (&2,y2,&2 * h0);
 163          (&2,y3,&2 * h0);
 164          (#3.36 ,y4, #3.36);
 165          (&2,y5,&2 * h0);
 166          (&2,y6,&2 * h0)]
 167       (
 168        delta4_y y1 y2 y3 y4 y5 y6 < &0)`;
 169   };;
 170
 171 add
 172   {
 173     idv="6078657299"; (* test dih 4240815464 *)
 174     doc = "Monotonic in y4.
 175       y4 > 3.36 ==> dih > 1.621.
 176       Tan[Pi - 1.621]^2 >= 396.1.
 177        ";
 178     tags=[Xconvert];
 179   ineq = Sphere.all_forall `ineq
 180       [
 181          (&2,y1,&2 * h0);
 182          (&2,y2,&2 * h0);
 183          (&2,y3,&2 * h0);
 184          (#3.36 ,y4, #3.36);
 185          (&2,y5,&2 * h0);
 186          (&2,y6,&2 * h0)]
 187   (let tan2lower = #396.1 in
 188    ((&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
 189 //       dih_y y1 y2 y3 y4 y5 y6 > #1.621 \/
 190       delta_y y1 y2 y3 y4 y5 y6 < &0))`;
 191   };;
 192
 193 add
 194   {
 195     idv="8384429938"; (* test delta98 lindih 4240815464 *)
 196     doc = "Justifies linearlized dih on [3.01,3.36] s.t. delta<98.";
 197     tags=[Xconvert];
 198   ineq = Sphere.all_forall `ineq
 199       [
 200          (&2,y1,&2 * h0);
 201          (&2,y2,&2 * h0);
 202          (&2,y3,&2 * h0);
 203          (#3.01 ,y4, #3.36);
 204          (&2,y5,&2 * h0);
 205          (&2,y6,&2 * h0)
 206 //       (&2,y7,&2 * h0)
 207 ]
 208       (
 209 //      delta_y (&2 * h0) y2 y3 y4 (&2) (&2) > &98 \/
 210         y_of_x (delta_234_x ((&2 * h0) pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &98 \/
 211           delta4_y y1 y2 y3 y4 y5 y6 < &0
 212 )`;
 213   };;
 214
 215 add
 216   {
 217     idv="9893763499"; (* test delta98 4240815464 *)
 218     doc = "Use monotonicity of Delta to reduce to y7=2.52, y8=2, y9=2. Shows dih>1.621 ==> delta>98";
 219     tags=[Xconvert];
 220   ineq = Sphere.all_forall `ineq
 221       [
 222          (&2,y1,&2 * h0);
 223          (&2,y2,&2 * h0);
 224          (&2,y3,&2 * h0);
 225          (#3.01 ,y4, #3.36);
 226          (&2,y5,&2 * h0);
 227          (&2,y6,&2 * h0)
 228 //       (&2,y7,&2 * h0)
 229 ]
 230   (let tan2lower = #396.1 in
 231    ((&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
 232 //        dih_y y1 y2 y3 y4 y5 y6 > #1.621 \/
 233 //      delta_y (&2 * h0) y2 y3 y4 (&2) (&2) > &98 \/
 234         y_of_x (delta_234_x ((&2 * h0) pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &98
 235 ))`;
 236   };;
 237
 238 add
 239   {
 240     idv="5429228381"; (* test back98 4240815464 *)
 241     doc = "taum lower bound on back simplex when y4 in [3.01,3.36]";
 242     tags=[Xconvert];
 243   ineq = Sphere.all_forall `ineq
 244       [
 245          (&2,y1,&2 * h0);
 246          (&2,y2,&2 * h0);
 247          (&2,y3,&2 * h0);
 248          (#3.01 ,y4, #3.36);
 249          (&2,y5,&2 * h0);
 250          (&2,y6,&2 * h0)
 251 ]
 252       (
 253         taum y1 y2 y3 y4 y5 y6 > -- #0.07 \/
 254           delta_y y1 y2 y3 y4 y5 y6 < &98)`;
 255   };;
 256
 257 add
 258   {
 259     idv="3508342905"; (* test front98 4240815464 *)
 260     doc = "lower bound on front simplex when y4 in [3.01,3.36]";
 261     tags=[Xconvert];
 262   ineq = Sphere.all_forall `ineq
 263       [
 264          (&2,y1,&2 * h0);
 265          (&2,y2,&2 * h0);
 266          (&2,y3,&2 * h0);
 267          (#3.01 ,y4, #3.36);
 268          (&2,y5,&2 * h0);
 269          (&2,y6,&2 * h0)
 270 ]
 271       (
 272         taum y1 y2 y3 y4 y5 y6   - #0.07 +
 273           #0.7573 * dih_y y1 y2 y3 y4 y5 y6 - #1.433 > &0 \/
 274           dih_y y1 y2 y3 y4 y5 y6 > #1.621 \/
 275         delta_y y1 y2 y3 y4 y5 y6 < &98)`;
 276   };;
 277
 278 add
 279   {
 280     idv="2862885615"; (* test front103 4240815464 *)
 281     doc = "lower bound on front simplex when y4 [2.62,3.01]";
 282     tags=[Xconvert];
 283   ineq = Sphere.all_forall `ineq
 284       [
 285          (&2,y1,&2 * h0);
 286          (&2,y2,&2 * h0);
 287          (&2,y3,&2 * h0);
 288          (#2.62 ,y4, #3.01);
 289          (&2,y5,&2 * h0);
 290          (&2,y6,&2 * h0)
 291 ]
 292       (
 293         taum y1 y2 y3 y4 y5 y6 + #0.103 +
 294           #0.7573 * dih_y y1 y2 y3 y4 y5 y6 - #1.433 > &0 \/
 295           dih_y y1 y2 y3 y4 y5 y6 > #1.621)`;
 296   };;
 297
 298 add
 299   {
 300     idv="1611600345";  (* test back 4240815464 *)
 301     doc = "lower bound on back simplex when y4 in [2.52,2.62]";
 302     tags=[Xconvert];
 303   ineq = Sphere.all_forall `ineq
 304       [
 305          (&2,y1,&2 * h0);
 306          (&2,y2,&2 * h0);
 307          (&2,y3,&2 * h0);
 308          (#2.52 ,y4, #2.62);
 309          (&2,y5,&2 * h0);
 310          (&2,y6,&2 * h0)
 311 ]
 312       (
 313         taum y1 y2 y3 y4 y5 y6 > #0.095 + #0.14 * (y2 + y3 - &4) )`;
 314   };;
 315
 316 add
 317   {
 318     idv="2608321088"; (* test front 4240815464 *)
 319     doc = "";
 320     tags=[Xconvert];
 321   ineq = Sphere.all_forall `ineq
 322       [
 323          (&2,y1,&2 * h0);
 324          (&2,y2,&2 * h0);
 325          (&2,y3,&2 * h0);
 326          (#2.52 ,y4, #2.62);
 327          (&2,y5,&2 * h0);
 328          (&2,y6,&2 * h0)
 329 ]
 330       (
 331         taum y1 y2 y3 y4 y5 y6 + #0.095 + #0.14 * (y2 + y3 - y4) +
 332           #0.7573 * dih_y y1 y2 y3 y4 y5 y6 - #1.433 > &0 \/
 333           dih_y y1 y2 y3 y4 y5 y6 > #1.621)`;
 334   };;
 335
 336
 337 (* ************************************************************************** *)
 338 (* DEPRECATED INEQ 704377224150 *)
 339 (* ************************************************************************** *)
 340
 341 skip
 342   {
 343     idv="test azim 70437224150";
 344     doc = "";
 345     tags=[];
 346   ineq = Sphere.all_forall `ineq
 347       [
 348          (&2,y1,&2 * h0);
 349          (&2,y2,&2 * h0);
 350          (&2,y3,&2 * h0);
 351          (#2.65,y4,sqrt8);
 352          (&2,y5,&2 * h0);
 353          (&2,y6,&2 * h0)]
 354       (dih_y y1 y2 y3 y4 y5 y6 > #1.215)`;
 355   };;
 356
 357 skip
 358   {
 359     idv="old test front 70437224150";
 360     doc = "";
 361     tags=[];
 362   ineq = Sphere.all_forall `ineq
 363       [
 364          (&2,y1,&2 * h0);
 365          (&2,y2,&2 * h0);
 366          (&2,y3,&2 * h0);
 367          (&2 * h0,y4,#2.77);
 368          (&2,y5,&2 * h0);
 369          (&2,y6,&2 * h0)]
 370       (taum y1 y2 y3 y4 y5 y6 + #0.0842 + #0.16 * (y2 + y3 - &4) + -- #0.018 * (y4 - &2 * h0) + #4.72 * dih_y y1 y2 y3 y4 y5 y6 > #6.235)`;
 371   };;
 372
 373 skip
 374   {
 375     idv="old test back 70437224150";
 376     doc = "";
 377     tags=[];
 378   ineq = Sphere.all_forall `ineq
 379       [
 380          (&2,y1,&2 * h0);
 381          (&2,y2,&2 * h0);
 382          (&2,y3,&2 * h0);
 383          (&2 * h0,y4,#2.84);
 384          (&2,y5,&2 * h0);
 385          (&2,y6,&2 * h0)]
 386       (taum y1 y2 y3 y4 y5 y6 > #0.0842 + #0.16 * (y2 + y3  - &4) - #0.018 * (y4 - &2 * h0))`;
 387   };;
 388
 389 skip
 390   {
 391     idv="test front 70437224150";
 392     doc = "";
 393     tags=[];
 394   ineq = Sphere.all_forall `ineq
 395       [
 396          (&2,y1,&2 * h0);
 397          (&2,y2,&2 * h0);
 398          (&2,y3,&2 * h0);
 399          (&2 * h0,y4,#2.65);
 400          (&2,y5,&2 * h0);
 401          (&2,y6,&2 * h0)]
 402       (taum y1 y2 y3 y4 y5 y6 + #0.0842 + #0.17 * (y2 + y3 - &4) + -- #0.01 * (y4 - &2 * h0) + #4.72 * dih_y y1 y2 y3 y4 y5 y6 > #6.248)`;
 403   };;
 404
 405 skip
 406   {
 407     idv="test back 70437224150";
 408     doc = "";
 409     tags=[];
 410   ineq = Sphere.all_forall `ineq
 411       [
 412          (&2,y1,&2 * h0);
 413          (&2,y2,&2 * h0);
 414          (&2,y3,&2 * h0);
 415          (&2 * h0,y4,#2.65);
 416          (&2,y5,&2 * h0);
 417          (&2,y6,&2 * h0)]
 418       (taum y1 y2 y3 y4 y5 y6 > #0.0842 + #0.17 * (y2 + y3  - &4) - #0.01 * (y4 - &2 * h0))`;
 419   };;
 420
 421 skip
 422   {
 423     idv="test";
 424     doc = "";
 425     tags=[];
 426   ineq = Sphere.all_forall `ineq
 427       [
 428          (&2,y1,&2 * h0);
 429          (&2,y2,&2 * h0);
 430          (&2,y3,&2 * h0);
 431          (#3.23,y4,#3.4);
 432          (&2,y5,&2 * h0);
 433          (&2,y6,&2 * h0)]
 434       (dih_y y1 y2 y3 y4 y5 y6 > #1.544)`;
 435   };;
 436
 437 skip
 438   {
 439     idv="test front";
 440     doc = "";
 441     tags=[];
 442   ineq = Sphere.all_forall `ineq
 443       [
 444          (&2,y1,&2 * h0);
 445          (&2,y2,&2 * h0);
 446          (&2,y3,&2 * h0);
 447          (&2 * h0,y4,#2.84);
 448          (&2,y5,&2 * h0);
 449          (&2,y6,&2 * h0)]
 450       (taum y1 y2 y3 y4 y5 y6 + #0.0842 + #0.16 * (y2 + y3 - &4) + -- #0.018 * (y4 - &2 * h0) + #0.972 * dih_y y1 y2 y3 y4 y5 y6 > #1.707)`;
 451   };;
 452
 453 skip
 454   {
 455 idv="test";
 456 doc = "If  minor diag >= 3, then 3/1.26 > 2.38 and we can contract.
 457           15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
 458            Added May 12, 2011.
 459        c2 upper bound changed from 15.53 to 16.0 on May 23.";
 460 tags=[];
 461 ineq = Sphere.all_forall `ineq
 462   [
 463   (&1 , e1, &1 + sol0/ pi);
 464   (&1 , e2, &1 + sol0/ pi);
 465   (&1 , e3, &1 + sol0/ pi);
 466   ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
 467   ((&2/ h0) pow 2, b2, #3.01 pow 2);
 468   ((#2.9 / h0) pow 2, c2,#16.0)
 469   ]
 470    ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
 471 };;