2 The actual definitions of these functions need to be supplied.
3 For now, the functions only get used in cfsqp and interval verifications.
5 The LC functions are implemented in intervals as locally constant functions.
8 (* true definitions in mdtau.hl *)
11 let mdtau_fake = new_definition
12 `mdtau (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) = &0`;;
14 let mdtau2_fake = new_definition
15 `mdtau2 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) = &0`;;
17 addtex (Section,"Main Estimate","Ears, top edges 2,2,long");;
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 [
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)
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 [
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)
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.
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 [
87 (delta_y_LC y1 y2 y3 y4 y5 y6 < &15) \/
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)
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 [
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)
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.
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 [
135 ( delta4_y y1 y2 y3 y4 y5 y6 < &0)
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.
147 This is a consequence of 2485876245. No separate verification is needed.
149 tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
150 ineq = all_forall `ineq [
159 ( delta4_y y1 y2 y3 y4 y5 y6 > &0)
163 addtex (Section,"Main Estimate","June Hexagons, top edges all 2.");;
165 addtex(Comment,"Main Estimate",
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.
178 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
179 ineq = all_forall `ineq [
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)
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.
204 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
205 ineq = all_forall `ineq [
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) \/
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...'
233 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
234 ineq = all_forall `ineq [
243 (y_of_x taum_2flat_x y1 y2 y3 y4 y5 y6
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) \/
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.
262 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
263 ineq = all_forall `ineq [
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 \/
276 ( y_of_x euler_1flat_x y1 y2 y3 y4 y5 y6< &0)
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...'
290 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
291 ineq = all_forall `ineq [
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)
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.
319 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
320 ineq = all_forall `ineq [
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 >
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)
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
351 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
352 ineq = all_forall `ineq [
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)
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.
378 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
379 ineq = all_forall `ineq [
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)
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.
408 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
409 ineq = all_forall `ineq [
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)
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.
442 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
443 ineq = all_forall `ineq [
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)
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.
478 tags=[Flypaper["SAUZWSD"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
479 ineq = all_forall `ineq [
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)
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. *)
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 [
517 ( dih_y y1 y2 y3 y4 y5 y6 < pi / &2 - #0.46)
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.
534 tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
535 ineq = all_forall `ineq [
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)
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 [
564 ( taum y1 y2 y3 y4 y5 y6 > &0)
571 doc="pent+hi+something that we can zero out.
572 This and '8199484193' do the case of no straight nodes.
574 tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
575 ineq = all_forall `ineq [
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
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.
596 tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
597 ineq = all_forall `ineq [
605 ( taum y1 y2 y3 y4 y5 y6 +
606 y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
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.
623 tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
624 ineq = all_forall `ineq [
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
635 y_of_x (delta_pent_x) y1 y2 y3 y4 y5 y6 > &0
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.
647 tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;
648 Xconvert;Tex;Penalty(500.0,5000.0)];
649 ineq = all_forall `ineq [
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
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. *)
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'
680 tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
681 ineq = all_forall `ineq [
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)
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'.
705 tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
706 ineq = all_forall `ineq [
714 ( dih_y y1 y2 y3 y4 y5 y6 < pi - #1.001)`;
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.)
728 tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
729 ineq = all_forall `ineq [
738 ( dih_y y1 y2 y3 y4 y5 y6 < pi - &2 * #1.001)
742 Functional_equation.functional_overload();;
744 (* May 9, 2013. taud function. taud_v4 seems to be the version that
745 works in all cases (pent and hex). *)
750 let skip = Ineq.skip;;
752 let all_forall = Sphere.all_forall;;
759 local fan/main estimate/terminal pent
760 LHS(135,delta=20) RHS(126,delta=0)
762 tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
763 ineq = all_forall `ineq [
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 +
775 // y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
777 y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
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 _ -> () ;;
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;
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;
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.";;
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;
823 map Function_list.function_remove [mu_y;taud_x;delta_x1;functional_edge_126_x;
824 functional_edge_135_x;];;
828 Parse_ineq.autogen_remove mudL_234_x;;
829 Function_list.function_remove mudL_234_x;;
835 flyspeck_needs "nonlinear/scripts.hl";;
838 let _ = Ineq.add s in
839 Scripts.one_cfsqp s.idv;;
841 rflyspeck_needs "nonlinear/auto_lib.hl";;
844 let _ = Ineq.add s in
845 Auto_lib.testsplit true s.idv;;
848 let _ = Ineq.add s in
849 Auto_lib.testsplit false s.idv;;
853 Auto_lib.testsplit true "7796879304";;
854 map (Auto_lib.testsplit true) cases;;
857 map Scripts.one_cfsqp cases;;
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";