legacy/inequalities/dodec_inequalities.ml

   1
   2 (* -------------------------------------------------------------------------- *)
   3 (*  Util                                                                      *)
   4 (* -------------------------------------------------------------------------- *)
   5
   6 let mk_times x y = mk_binop `( *. )` x y
   7 let mk_plus x y = mk_binop `( +. )` x y
   8 let mk_gt x y = mk_binop `( >. )` x y
   9 let _0 = `&0`
  10 let _1 = `&1`
  11 let m_1 = `-- &1`
  12 let list_disj l = end_itlist (curry mk_disj) l
  13
  14 (* -------------------------------------------------------------------------- *)
  15 (*  Definitions                                                               *)
  16 (* -------------------------------------------------------------------------- *)
  17
  18 (*
  19  * t = 1.25841
  20  * 2t = 2.51682
  21  * (2t)^2 = 6.3343829124
  22  *)
  23 let dodecTrunc = kepler_def `dodecTrunc = #1.25841`
  24 let twoDodecTrunc = kepler_def `twoDodecTrunc = #2.51682`
  25 let twoDodecTruncSq = kepler_def `twoDodecTruncSq = #6.3343829124`
  26 let dodecSlope = kepler_def `dodecSlope = #0.42755`
  27
  28 let volume_x = kepler_def(`volume_x x1 x2 x3 x4 x5 x6 =
  29         let del = sqrt (delta_x x1 x2 x3 x4 x5 x6) in
  30         let u126 = ups_x x1 x2 x6 in
  31         let u135 = ups_x x1 x3 x5 in
  32         let u234 = ups_x x2 x3 x4 in
  33         let vol = ((&1)/((&48)*del))*
  34                 ((x1*(x2+x6-x1)+x2*(x1+x6-x2))*(chi_x x4 x5 x3 x1 x2 x6)/u126
  35                +(x2*(x3+x4-x2)+x3*(--x3+x4+x2))*(chi_x x6 x5 x1 x3 x2 x4)/u234
  36                +(x1*(--x1+x3+x5)+x3*(x1-x3+x5))*(chi_x x4 x6 x2 x1 x3 x5)/u135) in
  37           vol`)
  38
  39 let truncated_volume_x = kepler_def(`truncated_volume_x x1 x2 x3 x4 x5 x6 =
  40         let vor = vort_x x1 x2 x3 x4 x5 x6 dodecTrunc in
  41         let sol = sol_x x1 x2 x3 x4 x5 x6 in
  42           (vor - (&4 / &3) * sol) / (--(&4) * doct)`)
  43
  44 let omega_x = kepler_def( `omega_x x1 x2 x3 x4 x5 x6 =
  45     if eta_x x1 x2 x6 < sqrt2 /\
  46        eta_x x1 x3 x5 < sqrt2 /\
  47        eta_x x2 x3 x4 < sqrt2 /\
  48        eta_x x4 x5 x6 < sqrt2
  49     then
  50       volume_x x1 x2 x3 x4 x5 x6
  51     else
  52       truncated_volume_x x1 x2 x3 x4 x5 x6`)
  53
  54 let squander_x = kepler_def( `squander_x x1 x2 x3 x4 x5 x6 =
  55     omega_x x1 x2 x3 x4 x5 x6 - dodecSlope * sol_x x1 x2 x3 x4 x5 x6`)
  56
  57 (* -------------------------------------------------------------------------- *)
  58 (*  Tetrahedra                                                                *)
  59 (* -------------------------------------------------------------------------- *)
  60
  61 let basicTet =
  62   let bnds = `ineq
  63     [(&4, x1, twoDodecTruncSq);
  64      (&4, x2, twoDodecTruncSq);
  65      (&4, x3, twoDodecTruncSq);
  66      (&4, x4, twoDodecTruncSq);
  67      (&4, x5, twoDodecTruncSq);
  68      (&4, x6, twoDodecTruncSq)]` in
  69   let mk_p (vol,sol,dih,y1,y2,y3,y4,y5,y6,const) =
  70     let vt = mk_times vol `omega_x x1 x2 x3 x4 x5 x6` in
  71     let st = mk_times sol `sol_x x1 x2 x3 x4 x5 x6` in
  72     let dt = mk_times dih `dih_x x1 x2 x3 x4 x5 x6` in
  73     let y1t = mk_times y1 `sqrt x1` in
  74     let y2t = mk_times y2 `sqrt x2` in
  75     let y3t = mk_times y3 `sqrt x3` in
  76     let y4t = mk_times y4 `sqrt x4` in
  77     let y5t = mk_times y5 `sqrt x5` in
  78     let y6t = mk_times y6 `sqrt x6` in
  79     let lhs = end_itlist mk_plus [vt;st;dt;y1t;y2t;y3t;y4t;y5t;y6t;const] in
  80       mk_gt lhs _0 in
  81     fun args -> all_forall (mk_comb(bnds,mk_p args))
  82
  83 (*
  84 structure R = Random
  85 val rand = R.rand(1029,4139871)
  86 fun n () = R.randRange(100000000,999999999) rand
  87 n()
  88
  89  *)
  90
  91 let D_232427898 = basicTet(_1,_0,_0,_0,_0,_0,_0,_0,_0,`-- #0.20280`)
  92 let D_501745932 = basicTet(_0,_1,_0,_0,_0,_0,_0,_0,_0,`-- #0.31568`)
  93 let D_454413312 = basicTet(_0,m_1,_0,_0,_0,_0,_0,_0,_0,`#1.05124`)
  94 let D_484548925 = basicTet(_0,_0,_1,_0,_0,_0,_0,_0,_0,`-- #0.85613`)
  95 let D_140432082 = basicTet(_0,_0,m_1,_0,_0,_0,_0,_0,_0,`#1.88674`)
  96 let D_211431164 = basicTet(_1,`-- #0.42755`,_0,_0,_0,_0,_0,_0,_0,_0)
  97 let D_120383233 = basicTet(_1,`-- #0.68`,`#1.88718`,_0,_0,_0,_0,_0,_0,`-- #1.54550`)
  98 let D_950195574 = basicTet(_1,`-- #0.68`,`#0.90746`,_0,_0,_0,_0,_0,_0,`-- #0.70671`)
  99 let D_411439162 = basicTet(_1,`-- #0.68`,`#0.46654`,_0,_0,_0,_0,_0,_0,`-- #0.32922`)
 100 let D_930476095 = basicTet(_1,`-- #0.55889`,_0,_0,_0,_0,_0,_0,_0,`#0.07365`)
 101 let D_504216105 = basicTet(_1,`-- #0.63214`,_0,_0,_0,_0,_0,_0,_0,`#0.13033`)
 102 let D_303447655 = basicTet(_1,`-- #0.73256`,_0,_0,_0,_0,_0,_0,_0,`#0.23590`)
 103 let D_999530305 = basicTet(_1,`-- #0.89346`,_0,_0,_0,_0,_0,_0,_0,`#0.40504`)
 104 let D_774222998 = basicTet(_1,`-- #0.3`,`-- #0.5734`,_0,_0,_0,_0,_0,_0,`#0.97823`)
 105 let D_583790155 = basicTet(_1,`-- #0.3`,`-- #0.03668`,_0,_0,_0,_0,_0,_0,`-- #0.02475`)
 106 let D_954638763 = basicTet(_1,`-- #0.3`,`#0.04165`,_0,_0,_0,_0,_0,_0,`-- #0.12118`)
 107 let D_836501282 = basicTet(_1,`-- #0.3`,`#0.1234`,_0,_0,_0,_0,_0,_0,`-- #0.20926`)
 108 let D_815857122 = basicTet(_1,`-- #0.42755`,`-- #0.11509`,_0,_0,_0,_0,_0,_0,`#0.17186`)
 109 let D_143442051 = basicTet(_1,`-- #0.42755`,`-- #0.04078`,_0,_0,_0,_0,_0,_0,`#0.05072`)
 110 let D_616037833 = basicTet(_1,`-- #0.42755`,`#0.11031`,_0,_0,_0,_0,_0,_0,`-- #0.13562`)
 111 let D_943639543 = basicTet(_1,`-- #0.42755`,`#0.13091`,_0,_0,_0,_0,_0,_0,`-- #0.15735`)
 112 let D_348573741 = basicTet(_1,`-- #0.55792`,`-- #0.21394`,_0,_0,_0,_0,_0,_0,`#0.41800`)
 113 let D_887895540 = basicTet(_1,`-- #0.55792`,`-- #0.0068`,_0,_0,_0,_0,_0,_0,`#0.08191`)
 114 let D_292050936 = basicTet(_1,`-- #0.55792`,`#0.0184`,_0,_0,_0,_0,_0,_0,`#0.05123`)
 115 let D_747114280 = basicTet(_1,`-- #0.55792`,`#0.24335`,_0,_0,_0,_0,_0,_0,`-- #0.19398`)
 116 let D_407035272 = basicTet(_1,`-- #0.68`,`-- #0.30651`,_0,_0,_0,_0,_0,_0,`#0.64850`)
 117 let D_746762527 = basicTet(_1,`-- #0.68`,`-- #0.06965`,_0,_0,_0,_0,_0,_0,`#0.27799`)
 118 let D_908135697 = basicTet(_1,`-- #0.68`,`#0.0172`,_0,_0,_0,_0,_0,_0,`#0.15661`)
 119 let D_852700722 = basicTet(_1,`-- #0.68`,`#0.41812`,_0,_0,_0,_0,_0,_0,`-- #0.28776`)
 120 let D_187794654 = basicTet(_1,`-- #0.64934`,_0,_0,_0,_0,_0,_0,_0,`#0.14841`)
 121 let D_241250402 = basicTet(_1,`-- #0.6196`,_0,_0,_0,_0,_0,_0,_0,`#0.11763`)
 122 let D_614375500 = basicTet(_1,`-- #0.58402`,_0,_0,_0,_0,_0,_0,_0,`#0.09029`)
 123 let D_392850749 = basicTet(_1,`-- #0.25181`,_0,_0,_0,_0,_0,_0,_0,`-- #0.09649`)
 124 let D_324682944 = basicTet(_1,`-- #0.00909`,_0,_0,_0,_0,_0,_0,_0,`-- #0.19954`)
 125 let D_102919537 = basicTet(_1,`#0.93877`,_0,_0,_0,_0,_0,_0,_0,`-- #0.53788`)
 126 let D_756454529 = basicTet(_1,`#0.93877`,`-- #0.20211`,_0,_0,_0,_0,_0,_0,`-- #0.28126`)
 127 let D_563250599 = basicTet(_1,`#0.93877`,`#0.63517`,_0,_0,_0,_0,_0,_0,`-- #1.21407`)
 128 let D_439521695 = basicTet(_1,`#1.93877`,_0,_0,_0,_0,_0,_0,_0,`-- #0.85479`)
 129 let D_805633512 = basicTet(_1,`#1.93877`,`-- #0.20211`,_0,_0,_0,_0,_0,_0,`-- #0.62187`)
 130 let D_892141600 = basicTet(_1,`#1.93877`,`#0.63517`,_0,_0,_0,_0,_0,_0,`-- #1.57647`)
 131 let D_224306197 = basicTet(_1,`-- #0.42775`,_0,_0,_0,_0,_0,_0,_0,`#0.00012`)
 132 let D_120210454 = basicTet(_1,`-- #0.55792`,_0,_0,_0,_0,_0,_0,_0,`#0.07304`)
 133 let D_479875130 = basicTet(_1,_0,`-- #0.07853`,_0,_0,_0,_0,_0,_0,`-- #0.09374`)
 134 let D_629548058 = basicTet(_1,_0,`-- #0.00339`,_0,_0,_0,_0,_0,_0,`-- #0.19868`)
 135 let D_469668150 = basicTet(_1,_0,`#0.18199`,_0,_0,_0,_0,_0,_0,`-- #0.39666`)
 136 let D_218128189 = basicTet(_1,`-- #0.42755`,`-- #0.2`,_0,_0,_0,_0,_0,_0,`#0.33207`)
 137 let D_169113912 = basicTet(_1,`-- #0.3`,`-- #0.36373`,_0,_0,_0,_0,_0,_0,`#0.58263`)
 138 let D_143105921 = basicTet(_1,`-- #0.3`,`#0.20583`,_0,_0,_0,_0,_0,_0,`-- #0.27984`)
 139 let D_421739939 = basicTet(_1,`-- #0.3`,`#0.40035`,_0,_0,_0,_0,_0,_0,`-- #0.44637`)
 140 let D_595203705 = basicTet(_1,`-- #0.3`,`#0.83259`,_0,_0,_0,_0,_0,_0,`-- #0.81644`)
 141 let D_943490566 = basicTet(_1,`-- #0.42755`,`-- #0.51838`,_0,_0,_0,_0,_0,_0,`#0.93276`)
 142 let D_797136399 = basicTet(_1,`-- #0.42755`,`#0.29344`,_0,_0,_0,_0,_0,_0,`-- #0.29650`)
 143 let D_603733089 = basicTet(_1,`-- #0.42755`,`#0.57056`,_0,_0,_0,_0,_0,_0,`-- #0.53375`)
 144 let D_459264712 = basicTet(_1,`-- #0.42755`,`#1.18656`,_0,_0,_0,_0,_0,_0,`-- #1.06114`)
 145 let D_557495949 = basicTet(_1,`-- #0.55792`,`-- #0.67644`,_0,_0,_0,_0,_0,_0,`#1.29062`)
 146 let D_171329882 = basicTet(_1,`-- #0.55792`,`#0.38278`,_0,_0,_0,_0,_0,_0,`-- #0.31335`)
 147 let D_720788076 = basicTet(_1,`-- #0.55792`,`#0.74454`,_0,_0,_0,_0,_0,_0,`-- #0.62307`)
 148 let D_554235027 = basicTet(_1,`-- #0.55792`,`#1.54837`,_0,_0,_0,_0,_0,_0,`-- #1.31127`)
 149 let D_569393441 = basicTet(_1,`-- #0.68`,`-- #0.82445`,_0,_0,_0,_0,_0,_0,`#1.62571`)
 150
 151 let D_992963254 = basicTet
 152   (_0,_1,_0,`#0.245`,`#0.245`,`#0.245`,
 153    `-- #0.063`,`-- #0.063`,`-- #0.063`,`-- #1.64327`)
 154
 155 let D_157321192 = basicTet
 156   (_0,_1,_0,`#0.3798`,`#0.3798`,`#0.3798`,
 157    `-- #0.198`,`-- #0.198`,`-- #0.198`,`-- #1.64207`)
 158
 159 (* Error: changed from 0.480715*)
 160 let D_954705068 = basicTet
 161   (_0,m_1,_0,`-- #0.151`,`-- #0.151`,`-- #0.151`,
 162    `#0.323`,`#0.323`,`#0.323`,`-- #0.48070`)
 163
 164 let D_607292193 = basicTet
 165   (_1,`-- #0.42755`,_0,`-- #0.0392`,`-- #0.0392`,`-- #0.0392`,
 166    `-- #0.0101`,`-- #0.0101`,`-- #0.0101`,`#0.29580`)
 167
 168 let D_852636576 = basicTet
 169   (_1,_0,_0,`#0.107`,`#0.107`,`#0.107`,
 170    `-- #0.116`,`-- #0.116`,`-- #0.116`,`-- #0.18169`)
 171
 172 let D_981457443 = basicTet
 173   (_1,_0,_0,`#0.0623`,`#0.0623`,`#0.0623`,
 174    `-- #0.0722`,`-- #0.0722`,`-- #0.0722`,`-- #0.17629`)
 175
 176 let D_400655725 = basicTet
 177   (_0,_0,_1,`-- #0.237`,`#0.372`,`#0.372`,
 178    `-- #0.708`,`#0.372`,`#0.372`,`-- #2.31694`)
 179
 180 let D_552790530 = basicTet
 181   (_0,_0,_1,`-- #0.237`,`#0.363`,`#0.363`,
 182    `-- #0.688`,`#0.363`,`#0.363`,`-- #2.28494`)
 183
 184 (* Error: changed from 0.9505*)
 185 let D_339650543 = basicTet
 186   (_0,_0,m_1,`#0.505`,`-- #0.152`,`-- #0.152`,
 187    `#0.766`,`-- #0.152`,`-- #0.152`,`-- #0.09503`)
 188
 189 (* -------------------------------------------------------------------------- *)
 190 (*  Quadrilaterals                                                            *)
 191 (* -------------------------------------------------------------------------- *)
 192
 193 let basicQuad =
 194   let bnds = `ineq
 195     [(&4, x1, twoDodecTruncSq);
 196      (&4, x2, twoDodecTruncSq);
 197      (&4, x3, twoDodecTruncSq);
 198      (twoDodecTruncSq, x4, #26.0));
 199      (&4, x5, twoDodecTruncSq);
 200      (&4, x6, twoDodecTruncSq);
 201      (&4, x7, twoDodecTruncSq);
 202      (&4, x8, twoDodecTruncSq);
 203      (&4, x9, twoDodecTruncSq)]` in
 204   let mk_times x y = mk_binop `( *. )` x y in
 205   let mk_plus x y = mk_binop `( +. )` x y in
 206   let mk_gt x y = mk_binop `( >. )` x y in
 207   let constr1 = `delta_x x1 x2 x3 x4 x5 x6 < &0` in
 208   let constr2 = `delta_x x7 x2 x3 x4 x8 x9 < &0` in
 209   let constr3 = `cross_diag_x x1 x2 x3 x4 x5 x6 x7 x8 x9 < twoDodecTrunc` in
 210   let mk_p (vol,sol,dih,const) =
 211     let vt = mk_times vol `omega_x x1 x2 x3 x4 x5 x6 + omega_x x7 x2 x3 x4 x8 x9` in
 212     let st = mk_times sol `sol_x x1 x2 x3 x4 x5 x6 + sol_x x7 x2 x3 x4 x8 x9` in
 213     let dt = mk_times dih `dih_x x1 x2 x3 x4 x5 x6` in
 214     let rhs = end_itlist  mk_plus [vt;st;dt;const] in
 215       mk_gt rhs _0 in
 216     fun args ->
 217       all_forall (mk_comb(bnds,list_disj [mk_p args;constr1;constr2;constr3]))
 218
 219 let D_195763418 = basicQuad (_1,_0,_0,`-- #0.45513`)
 220 let D_346647038 = basicQuad (_0,_1,_0,`-- #0.73192`)
 221 let D_542422328 = basicQuad (_0,m_1,_0,`#2.85860`)
 222 let D_958501031 = basicQuad (_0,_0,_1,`-- #1.15242`)
 223 let D_977882706 = basicQuad (_0,_0,m_1,`#3.25887`)
 224 let D_817699709 = basicQuad (_1,`-- #0.42755`,_0,`-- #0.031350`)
 225
 226 (* false *)
 227 (* let D_221335081 = basicQuad (_1,`-- #0.42775`,`-- #0.15098`,`-- #0.3670`) *)
 228
 229 (* false *)
 230 (* let D_380511524 = basicQuad (_1,`-- #0.42775`,`-- #0.09098`,`-- #0.1737`) *)
 231
 232 let D_534704091 = basicQuad (_1,`-- #0.42775`,`-- #0.00000`,`#0.0310`)
 233
 234 (* too true *)
 235 (* let D_510654661 = basicQuad (_1,`-- #0.42775`,`#0.18519`,`#0.3183`) *)
 236
 237
 238 let D_296038926 = basicQuad (_1,`-- #0.42775`,`#0.20622`,`#0.3438`)
 239
 240 (* false *)
 241 (* let D_725284239 = basicQuad (_1,`-- #0.55792`,`-- #0.30124`,`-- #1.0173`) *)
 242
 243 (* false *)
 244 (* let D_508592316 = basicQuad (_1,`-- #0.55792`,`-- #0.02921`,`-- #0.2101`) *)
 245
 246 (* false *)
 247 (* let D_780228595 = basicQuad (_1,`-- #0.55792`,`-- #0.00000`,`-- #0.1393`) *)
 248
 249 (* false *)
 250 (* let D_129176394 = basicQuad (_1,`-- #0.55792`,`#0.05947`,`-- #0.0470`) *)
 251
 252 let D_794503453 = basicQuad (_1,`-- #0.55792`,`#0.39938`,`#0.4305`)
 253 let D_820371697 = basicQuad (_1,`-- #0.55792`,`#2.50210`,`#2.8976`)
 254
 255 (* false *)
 256 (* let D_993947481 = basicQuad (_1,`-- #0.68000`,`-- #0.44194`,`-- #1.6264`) *)
 257
 258 (* false *)
 259 (* let D_888634003 = basicQuad (_1,`-- #0.68000`,`-- #0.10957`,`-- #0.6753`) *)
 260
 261 (* false *)
 262 (* let D_985594975 = basicQuad (_1,`-- #0.68000`,`-- #0.00000`,`-- #0.4029`) *)
 263
 264 let D_278856582 = basicQuad (_1,`-- #0.68000`,`#0.86096`,`#0.8262`)
 265 let D_309781213 = basicQuad (_1,`-- #0.68000`,`#2.44439`,`#2.7002`)
 266
 267 (* false *)
 268 (* let D_546070702 = basicQuad (_1,`-- #0.30000`,`-- #0.12596`,`-- #0.1279`) *)
 269
 270 let D_273299220 = basicQuad (_1,`-- #0.30000`,`-- #0.02576`,`#0.1320`)
 271 let D_420356876 = basicQuad (_1,`-- #0.30000`,`#0.00000`,`#0.1945`)
 272 let D_168730298 = basicQuad (_1,`-- #0.30000`,`#0.03700`,`#0.2480`)
 273
 274 let D_563211815 = basicQuad (_1,`-- #0.30000`,`#0.22476`,`#0.5111`)
 275 let D_923665644 = basicQuad (_1,`-- #0.30000`,`#2.31852`,`#2.9625`)
 276
 277 (* false *)
 278 (* let D_131907821 = basicQuad (_1,_0,`-- #0.23227`,`-- #0.1042`) *)
 279
 280 let D_632783039 = basicQuad (_1,_0,`#0.07448`,`#0.5591`)
 281 let D_997560269 = basicQuad (_1,_0,`#0.22019`,`#0.7627`)
 282 let D_849090707 = basicQuad (_1,_0,`#0.80927`,`#1.5048`)
 283 let D_741613981 = basicQuad (_1,_0,`#5.84380`,`#7.3468`)
 284