text_formalization/tame/tame_concl.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Conclusions                                                                  *)
   5 (* Chapter: Tame Hypermap                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-27                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11 Conclusions file for Tame Hypermap
  12 *)
  13
  14
  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";;
  19
  20 module Tame_concl  = struct
  21
  22   let PPHEUFG_concl = `!(H:(A)hypermap). tame_hypermap H <=> tame_hypermap (opposite_hypermap H)`;;
  23
  24   let RUNOQPQ_concl = `!(H:(A)hypermap). tame_hypermap H ==> restricted_hypermap H`;;
  25
  26   (* WTEMDTA_concl skipped. Tame hypermap classification theorem. *)
  27
  28   let UBHDEUU1_concl = `! V.  packing V /\ V SUBSET ball_annulus ==> FAN(vec 0, V, ESTD V)`;;
  29
  30   let UBHDEUU2_concl = `! V.  packing V /\ V SUBSET ball_annulus ==> FAN(vec 0, V, ECTC V)`;;
  31
  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)))`;;
  35
  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)))`;;
  39
  40   let FCDJDOT_concl = `(?W. packing W /\ W SUBSET ball_annulus /\ scriptL W > &12) ==>
  41        (?V. contravening V)`;;
  42
  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 )`;;
  45
  46   let JGTDEBU1_concl = `!V. contravening V ==>
  47        planar_hypermap (hypermap_of_fan (V, ESTD V))`;;
  48
  49   let JGTDEBU2_concl = `!V. contravening V ==>
  50        plain_hypermap (hypermap_of_fan (V, ESTD V))`;;
  51
  52   let JGTDEBU3_concl = `!V. contravening V ==>
  53        connected_hypermap (hypermap_of_fan (V, ESTD V))`;;
  54
  55   let JGTDEBU4_concl = `!V. contravening V ==>
  56        simple_hypermap (hypermap_of_fan (V, ESTD V))`;;
  57
  58   let JGTDEBU5_concl = `!V. contravening V ==>
  59        is_edge_nondegenerate  (hypermap_of_fan (V, ESTD V))`;;
  60
  61   let  JGTDEBU6_concl = `!V. contravening V ==>
  62        no_loops  (hypermap_of_fan (V, ESTD V))`;;
  63
  64   let  JGTDEBU7_concl = `!V. contravening V ==>
  65        is_no_double_joints  (hypermap_of_fan (V, ESTD V))`;;
  66
  67   let  JGTDEBU8_concl = `!V. contravening V ==>
  68        number_of_faces  (hypermap_of_fan (V, ESTD V)) >= 3 `;;
  69
  70   let  JGTDEBU10_concl = `!V. contravening V ==>
  71        tame_10  (hypermap_of_fan (V, ESTD V))`;;
  72
  73   let  JGTDEBU11_concl = `!V. contravening V ==>
  74        tame_11a  (hypermap_of_fan (V, ESTD V))`;;
  75
  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)  }))`;;
  82
  83   let  SZIPOAS_concl = `!V. contravening V /\ tame_hypermap_calcs ==>
  84        tame_11b  (hypermap_of_fan (V, ESTD V))`;;
  85
  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))`;;
  90
  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) ) `;;
  93
  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)`;;
  98
  99   let  CRTTXAT_concl = `!V. contravening V /\ tame_hypermap_calcs /\ (perimeterbound (V, ESTD V))==>
 100        tame_9a  (hypermap_of_fan (V, ESTD V))`;;
 101
 102
 103 (* main result of the chapter. *)
 104
 105   let MQMSMAB_concl = `!V. contravening V /\ tame_hypermap_calcs /\ (perimeterbound (V, ESTD V))==>
 106         tame_hypermap (hypermap_of_fan (V, ESTD V))`;;
 107
 108 end;;