1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Chapter: Tame Hypermap *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
11 Conclusions file for Tame Hypermap
15 flyspeck_needs "hypermap/hypermap.hl";;
16 flyspeck_needs "fan/fan_defs.hl";;
17 flyspeck_needs "packing/pack_defs.hl";;
18 flyspeck_needs "tame/tame_defs.hl";;
20 module Tame_concl = struct
22 let PPHEUFG_concl = `!(H:(A)hypermap). tame_hypermap H <=> tame_hypermap (opposite_hypermap H)`;;
24 let RUNOQPQ_concl = `!(H:(A)hypermap). tame_hypermap H ==> restricted_hypermap H`;;
26 (* WTEMDTA_concl skipped. Tame hypermap classification theorem. *)
28 let UBHDEUU1_concl = `! V. packing V /\ V SUBSET ball_annulus ==> FAN(vec 0, V, ESTD V)`;;
30 let UBHDEUU2_concl = `! V. packing V /\ V SUBSET ball_annulus ==> FAN(vec 0, V, ECTC V)`;;
32 let FATUGPD_concl = `!V. packing V /\ V SUBSET ball_annulus ==>
33 (?W phi. BIJ phi V W /\ (!v. v IN V ==> norm(v) = norm(phi v)) /\
34 (!w. w IN W ==> (set_of_edge w W (ECTC W) = {}) \/ (surrounded_node (W,(ECTC W)) w)))`;;
36 let FJLBXS_concl = `!V. packing V /\ V SUBSET ball_annulus ==>
37 (?W phi. BIJ phi V W /\ (!v. v IN V ==> norm(v) = norm(phi v)) /\
38 (!w. w IN W ==> (set_of_edge w W (ESTD W) = {}) \/ (surrounded_node (W,(ESTD W)) w)))`;;
40 let FCDJDOT_concl = `(?W. packing W /\ W SUBSET ball_annulus /\ scriptL W > &12) ==>
41 (?V. contravening V)`;;
43 let HRXEFDM_concl = `!V. contravening V ==>
44 ( sum (face_set_of_fan (V,ESTD V)) (\ f. tauVEF (V,ESTD V,f) ) < &4 * pi - &20 * sol0 )`;;
46 let JGTDEBU1_concl = `!V. contravening V ==>
47 planar_hypermap (hypermap_of_fan (V, ESTD V))`;;
49 let JGTDEBU2_concl = `!V. contravening V ==>
50 plain_hypermap (hypermap_of_fan (V, ESTD V))`;;
52 let JGTDEBU3_concl = `!V. contravening V ==>
53 connected_hypermap (hypermap_of_fan (V, ESTD V))`;;
55 let JGTDEBU4_concl = `!V. contravening V ==>
56 simple_hypermap (hypermap_of_fan (V, ESTD V))`;;
58 let JGTDEBU5_concl = `!V. contravening V ==>
59 is_edge_nondegenerate (hypermap_of_fan (V, ESTD V))`;;
61 let JGTDEBU6_concl = `!V. contravening V ==>
62 no_loops (hypermap_of_fan (V, ESTD V))`;;
64 let JGTDEBU7_concl = `!V. contravening V ==>
65 is_no_double_joints (hypermap_of_fan (V, ESTD V))`;;
67 let JGTDEBU8_concl = `!V. contravening V ==>
68 number_of_faces (hypermap_of_fan (V, ESTD V)) >= 3 `;;
70 let JGTDEBU10_concl = `!V. contravening V ==>
71 tame_10 (hypermap_of_fan (V, ESTD V))`;;
73 let JGTDEBU11_concl = `!V. contravening V ==>
74 tame_11a (hypermap_of_fan (V, ESTD V))`;;
76 let CDTETAT_concl = `!V x. contravening V /\ x IN dart_of_fan (V,ESTD V) /\ tame_hypermap_calcs ==>
77 (let (p,q,r) = type_of_node (hypermap_of_fan (V, ESTD V)) x in
78 ((p,q+r) IN { (0,3), (0,4), (0,5), (1,2), (1,3), (1,4),
79 (2,1), (2,2), (2,3), (3,1), (3,2), (3,3),
80 (4,0), (4,1),(4,2), (5,0), (5,1),
81 (6,0), (6,1), (7,0) }))`;;
83 let SZIPOAS_concl = `!V. contravening V /\ tame_hypermap_calcs ==>
84 tame_11b (hypermap_of_fan (V, ESTD V))`;;
86 let KCBLRQC_concl = `!V x. contravening V /\ x IN dart_of_fan (V,ESTD V) /\ tame_hypermap_calcs ==>
87 (let H = hypermap_of_fan (V,ESTD V) in
88 let (p,q,r) = type_of_node H x in
89 (r > 0) \/ (sum (set_of_face_meeting_node H x) (\ f. tauVEF (V,ESTD V,f)) >= b_tame p q))`;;
91 let BDJYFFB1_concl = `!V x. contravening V /\ x IN dart_of_fan (V, ESTD V) /\ tame_hypermap_calcs ==>
92 tame_12o ( hypermap_of_fan (V,ESTD V) ) `;;
94 let BDJYFFB2_concl = `!V x. contravening V /\ x IN dart_of_fan (V, ESTD V) /\ tame_hypermap_calcs ==>
95 (let H = hypermap_of_fan (V,ESTD V) in
96 (type_of_node H x = (5,0,1)) ==>
97 sum {f | f IN set_of_face_meeting_node H x /\ CARD(f)=3 } (\f. tauVEF (V, ESTD V,f)) > #0.63)`;;
99 let CRTTXAT_concl = `!V. contravening V /\ tame_hypermap_calcs /\ (perimeterbound (V, ESTD V))==>
100 tame_9a (hypermap_of_fan (V, ESTD V))`;;
103 (* main result of the chapter. *)
105 let MQMSMAB_concl = `!V. contravening V /\ tame_hypermap_calcs /\ (perimeterbound (V, ESTD V))==>
106 tame_hypermap (hypermap_of_fan (V, ESTD V))`;;