text_formalization/local/GBYCPXS.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Local Fan                                              *)
   6 (* Author: Hoang Le Truong                                        *)
   7 (* Date: 2012-04-01                                                           *)
   8 (* ========================================================================= *)
   9
  10
  11
  12
  13 module  Gbycpxs = struct
  14
  15
  16 open Wjscpro;;
  17 open Polyhedron;;
  18 open Sphere;;
  19 open Fan_defs;;
  20 open Hypermap;;
  21 open Vol1;;
  22 open Fan;;
  23 open Topology;;
  24 open Fan_misc;;
  25 open Planarity;;
  26 open Conforming;;
  27 open Sphere;;
  28 open Hypermap;;
  29 open Fan;;
  30 open Topology;;
  31 open Prove_by_refinement;;
  32 open Pack_defs;;
  33 open Wrgcvdr_cizmrrh;;
  34 open Local_lemmas;;
  35 open Collect_geom;;
  36 open Dih2k_hypermap;;
  37 open Tecoxbm;;
  38 open Hdplygy;;
  39 open Nkezbfc_local;;
  40 open Flyspeck_constants;;
  41
  42
  43 let CARD_F_SY_IN_B_SY=prove(`!s:stable_sy l:real^(M,3)finite_product.
  44 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
  45 /\ l IN B_SY1 (a_sy s) (b_sy s)
  46 ==>  CARD (F_SY (vecmats l))=k`,
  47 REPEAT STRIP_TAC
  48 THEN MP_TAC(ARITH_RULE`2<k==> 1<k`)
  49 THEN RESA_TAC
  50 THEN MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`][IN_NUMSEG;VECMATS_MATVEC_ID;SET_RULE`(1 <= i /\ i <= k) /\
  51           (1 <= j /\ j <= k) /\
  52           row i (vecmats x) = row j (vecmats x)
  53 <=> 1 <= i /\ i <= k /\
  54           1 <= j /\ j <= k /\
  55           row i (vecmats x) = row j (vecmats x)`]
  56 THEN MRESA1_TAC (GEN_ALL CARD_F_SY_EQ)`l:real^(M,3)finite_product`);;
  57
  58
  59 let SOL0_POS=prove(`&0< sol0`,
  60 REWRITE_TAC[sol0; REAL_ARITH`&0 < &3 * acs (&1 / &3) - pi
  61 <=> pi/ &3 < acs (&1 / &3) `]
  62 THEN MRESAL1_TAC Trigonometry2.ACS`&1/ &3`[REAL_ARITH`-- &1 <= &1 / &3 /\ &1 / &3 <= &1`]
  63 THEN MP_TAC(REAL_ARITH`&0< pi==> &0 <= pi / &3 /\ pi / &3 <= pi`)
  64 THEN ASM_REWRITE_TAC[PI_WORKS]
  65 THEN STRIP_TAC
  66 THEN MRESAL1_TAC COS_ACS`&1/ &3`[REAL_ARITH`-- &1 <= &1 / &3 /\ &1 / &3 <= &1`]
  67 THEN MRESA_TAC COS_MONO_LT_EQ[`acs (&1 / &3)`;`pi/ &3`]
  68 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
  69 THEN REWRITE_TAC[ARITH_RULE`pi/ &3= pi/ &2- pi/ &6`;Trigonometry.SCEZKRH2;SIN_PI6]
  70 THEN REAL_ARITH_TAC);;
  71
  72 let SIGMA_SY_LE1=prove(`!s:stable_sy. sigma_sy s<= &1`,
  73 GEN_TAC
  74 THEN REWRITE_TAC[sigma_sy]
  75 THEN DISJ_CASES_TAC(SET_RULE`(ear_sy s) \/ ~(ear_sy (s:stable_sy))`)
  76 THEN ASM_REWRITE_TAC[]
  77 THEN REAL_ARITH_TAC);;
  78
  79
  80 let B_SY_LE_CSTAB=prove(`!s:stable_sy l:real^(M,3)finite_product.
  81 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
  82 /\ 1<= i /\ i<= k
  83 /\ l IN B_SY1 (a_sy s) (b_sy s)
  84 ==> norm (row i (vecmats l) - row (SUC (i MOD k)) (vecmats l))<= cstab`,
  85 REPEAT STRIP_TAC
  86 THEN ASM_TAC
  87 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
  88 THEN REPEAT STRIP_TAC
  89 THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;CONDITION1_SY] THEN STRIP_TAC)
  90 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
  91 THEN POP_ASSUM MP_TAC
  92 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
  93 THEN POP_ASSUM MP_TAC
  94 THEN POP_ASSUM MP_TAC
  95 THEN POP_ASSUM MP_TAC
  96 THEN DISCH_THEN(LABEL_TAC"THY")
  97 THEN DISCH_THEN(LABEL_TAC"THY2")
  98 THEN STRIP_TAC
  99 THEN POP_ASSUM(fun th-> MP_TAC th
 100 THEN REWRITE_TAC[convex_local_fan]
 101 THEN STRIP_TAC
 102 THEN POP_ASSUM MP_TAC
 103 THEN POP_ASSUM(fun th1-> MP_TAC th1
 104 THEN REWRITE_TAC[local_fan]
 105 THEN LET_TAC
 106 THEN STRIP_TAC
 107 THEN POP_ASSUM MP_TAC
 108 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
 109 THEN STRIP_TAC
 110 THEN ASSUME_TAC th1)
 111 THEN DISCH_THEN(LABEL_TAC"THY1")
 112 THEN ASSUME_TAC th)
 113 THEN STRIP_TAC
 114 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
 115 THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\
 116       SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC
 117 THENL[
 118 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
 119 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
 120 THEN POP_ASSUM MP_TAC
 121 THEN ARITH_TAC;
 122 POP_ASSUM MP_TAC
 123 THEN RESA_TAC
 124 THEN REMOVE_THEN"THY2"(fun th-> MRESA_TAC th[`i:num`;`SUC(i MOD k)`])
 125 THEN POP_ASSUM MP_TAC
 126 THEN MP_TAC(ARITH_RULE`i<=k==> i<= k-1 \/ i=k`)
 127 THEN RESA_TAC
 128 THENL[
 129 MP_TAC(ARITH_RULE`2<k ==> 1<=k /\ 1<k`)
 130 THEN RESA_TAC
 131 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i+1`][ARITH_RULE`1*A=A`]
 132 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`i+1:num`;`k:num`]
 133 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num`;]
 134 THEN REMOVE_ASSUM_TAC
 135 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
 136 THEN POP_ASSUM MP_TAC
 137 THEN REMOVE_ASSUM_TAC
 138 THEN REMOVE_ASSUM_TAC
 139 THEN POP_ASSUM MP_TAC
 140 THEN REWRITE_TAC[constraint_system]
 141 THEN STRIP_TAC
 142 THEN REMOVE_ASSUM_TAC
 143 THEN REMOVE_ASSUM_TAC
 144 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`i+1:num`][ARITH_RULE`A+0=A`])
 145 THEN ONCE_REWRITE_TAC[ARITH_RULE`1+A=A+1`]
 146 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 147 THEN MP_TAC(ARITH_RULE`i <= k-1 /\ 1<=i ==> i< k`)
 148 THEN RESA_TAC
 149 THEN MRESA_TAC MOD_LT[`i:num`;`k:num`]
 150 THEN REWRITE_TAC[ADD1]
 151 THEN REAL_ARITH_TAC;
 152 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 153 THEN MP_TAC(ARITH_RULE`2<k ==> 0<= k-1/\ 1<k`)
 154 THEN RESA_TAC
 155 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
 156 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num`;]
 157 THEN REMOVE_ASSUM_TAC
 158 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0+1=1`])
 159 THEN POP_ASSUM MP_TAC
 160 THEN REMOVE_ASSUM_TAC
 161 THEN REMOVE_ASSUM_TAC
 162 THEN POP_ASSUM MP_TAC
 163 THEN REWRITE_TAC[constraint_system]
 164 THEN STRIP_TAC
 165 THEN REMOVE_ASSUM_TAC
 166 THEN REMOVE_ASSUM_TAC
 167 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1:num`;`k:num`][ARITH_RULE`A+0=A`])
 168 THEN MP_TAC(ARITH_RULE`2<k ==> 1<= k/\ 1<k /\ ~(k=0)`)
 169 THEN RESA_TAC
 170 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
 171 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ k+k=k *2`]
 172 THEN REAL_ARITH_TAC]]);;
 173
 174
 175
 176
 177
 178 let PROPERTIES_EAR_SY=prove(`!s:stable_sy. ear_sy s ==> ?i. J_SY s={{i,f_sy s i}} /\ i IN I_SY s`,
 179 GEN_TAC
 180 THEN REWRITE_TAC[ear_sy]
 181 THEN STRIP_TAC
 182 THEN MRESA1_TAC FINITE_J_SY`s:stable_sy`
 183 THEN MRESA1_TAC (GEN_ALL Local_lemmas.FINITE_CARD1_IMP_SINGLETON)`J_SY(s:stable_sy)`
 184 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num`;]
 185 THEN REMOVE_ASSUM_TAC
 186 THEN REMOVE_ASSUM_TAC
 187 THEN REMOVE_ASSUM_TAC
 188 THEN POP_ASSUM MP_TAC
 189 THEN ASM_REWRITE_TAC[constraint_system;SUBSET;IN_SING;IN_ELIM_THM;]
 190 THEN STRIP_TAC
 191 THEN REMOVE_ASSUM_TAC
 192 THEN ONCE_REWRITE_TAC[EXTENSION]
 193 THEN REWRITE_TAC[IN_SING]
 194 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:(num->bool)`)
 195 THEN EXISTS_TAC`i:num`
 196 THEN ASM_REWRITE_TAC[]);;
 197
 198
 199
 200
 201
 202 let SING_J1_SY=prove_by_refinement(`!s:stable_sy. ear_sy s /\ I_SY s=0.. k_sy s -1 /\ f_sy s=(\i. ((1+i):num MOD k))/\ k_sy s =k /\ 2<k ==> ?i. J1_SY s= {(i,SUC(i MOD k_sy s))} /\ J_SY s= {{i MOD k,f_sy s i}} /\ i<=k /\ 1<=i`,
 203 [REPEAT STRIP_TAC
 204 THEN MRESAL1_TAC PROPERTIES_EAR_SY`s:stable_sy`[IN_NUMSEG]
 205 THEN DISJ_CASES_TAC(ARITH_RULE`i=0 \/ 1<= i`);
 206 EXISTS_TAC`k_sy(s:stable_sy):num`
 207 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ k<=k /\ 1<=k`)
 208 THEN RESA_TAC
 209 THEN MRESA_TAC MOD_LT[`1:num`;`k_sy(s:stable_sy)`]
 210 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 211 THEN MRESA_TAC MOD_ADD_MOD[`1:num`;`k:num`;`k:num`]
 212 THEN REMOVE_ASSUM_TAC
 213 THEN REMOVE_ASSUM_TAC
 214 THEN REMOVE_ASSUM_TAC
 215 THEN REMOVE_ASSUM_TAC
 216 THEN REMOVE_ASSUM_TAC
 217 THEN REMOVE_ASSUM_TAC
 218 THEN REMOVE_ASSUM_TAC
 219 THEN ASM_REWRITE_TAC[J1_SY;IN_SING;]
 220 THEN ONCE_REWRITE_TAC[EXTENSION]
 221 THEN REWRITE_TAC[IN_ELIM_THM;IN_SING;IN_NUMSEG]
 222 THEN GEN_TAC
 223 THEN EQ_TAC;
 224 RESA_TAC
 225 THEN REWRITE_TAC[PAIR_EQ]
 226 THEN MP_TAC(ARITH_RULE`i' <= k_sy s==> i' < k_sy s \/ i' = k_sy (s:stable_sy)`)
 227 THEN RESA_TAC;
 228 MRESA_TAC MOD_LT[`i':num`;`k_sy(s:stable_sy)`]
 229 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th])
 230 THEN REPEAT DISCH_TAC
 231 THEN MP_TAC(ARITH_RULE`i' < k_sy s==> 1+i' < k_sy s \/ 1+i' = k_sy (s:stable_sy)`)
 232 THEN RESA_TAC;
 233 MRESA_TAC MOD_LT[`1+i':num`;`k_sy(s:stable_sy)`]
 234 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th])
 235 THEN REPEAT DISCH_TAC
 236 THEN MP_TAC(ARITH_RULE`1<= i' ==> ~(i'= 0) /\ ~(1+i'=0)`)
 237 THEN RESA_TAC
 238 THEN MP_TAC(SET_RULE`~(i'= 0) /\ ~(1+i'=0) ==> ~({i', 1+i'} = {0, (1+ 0) MOD k})`)
 239 THEN ASM_REWRITE_TAC[];
 240 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
 241 THEN REPEAT DISCH_TAC
 242 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
 243 THEN RESA_TAC
 244 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 245 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
 246 THEN REPEAT DISCH_TAC
 247 THEN MRESA_TAC MOD_LT[`1:num`;`k_sy(s:stable_sy)`]
 248 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`])
 249 THEN REPEAT DISCH_TAC
 250 THEN MP_TAC(SET_RULE`{i', 0} = {0, 1} /\ ~(0=1)==> i'=1`)
 251 THEN RESA_TAC
 252 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
 253 THEN REPEAT DISCH_TAC
 254 THEN POP_ASSUM MP_TAC
 255 THEN RESA_TAC;
 256 MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
 257 THEN RESA_TAC
 258 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO];
 259 RESA_TAC
 260 THEN EXISTS_TAC`k:num`
 261 THEN ASM_REWRITE_TAC[]
 262 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<=k/\ ~(0=1) /\ ~(1+1=k)`)
 263 THEN RESA_TAC
 264 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 265 THEN ARITH_TAC;
 266 EXISTS_TAC`i:num`
 267 THEN MP_TAC(ARITH_RULE`i<= k-1/\ 2<k==> i<k/\ i<=k`)
 268 THEN RESA_TAC
 269 THEN MRESA_TAC MOD_LT[`i:num`;`k_sy(s:stable_sy)`]
 270 THEN REMOVE_ASSUM_TAC
 271 THEN REMOVE_ASSUM_TAC
 272 THEN REMOVE_ASSUM_TAC
 273 THEN ASM_REWRITE_TAC[J1_SY;IN_SING;]
 274 THEN ONCE_REWRITE_TAC[EXTENSION]
 275 THEN REWRITE_TAC[IN_ELIM_THM;IN_SING;IN_NUMSEG]
 276 THEN GEN_TAC
 277 THEN EQ_TAC;
 278 RESA_TAC
 279 THEN REWRITE_TAC[PAIR_EQ]
 280 THEN MP_TAC(ARITH_RULE`i' <= k_sy s==>  i' = k_sy (s:stable_sy) \/ i' < k_sy s `)
 281 THEN RESA_TAC;
 282 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
 283 THEN REPEAT DISCH_TAC
 284 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
 285 THEN RESA_TAC
 286 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 287 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
 288 THEN REPEAT DISCH_TAC
 289 THEN MRESA_TAC MOD_LT[`1:num`;`k_sy(s:stable_sy)`]
 290 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`])
 291 THEN REPEAT DISCH_TAC
 292 THEN MP_TAC(ARITH_RULE`1<= i==> ~(i=0)/\ ~(0=2)`)
 293 THEN RESA_TAC
 294 THEN MP_TAC(SET_RULE`{0, 1} = {i, (1+i ) MOD k} /\ ~(i=0)==> i=1`)
 295 THEN RESA_TAC
 296 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+1=2`] )
 297 THEN REPEAT DISCH_TAC
 298 THEN MRESA_TAC MOD_LT[`2:num`;`k_sy(s:stable_sy)`]
 299 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+1=2`] )
 300 THEN REPEAT DISCH_TAC
 301 THEN SUBGOAL_THEN`~({0,1}={1,2})` MP_TAC;
 302 REWRITE_TAC[EXTENSION;SET_RULE`x IN {A,B}<=> x= A \/ x=B`;]
 303 THEN POP_ASSUM MP_TAC
 304 THEN SET_TAC[];
 305 RESA_TAC;
 306 MRESA_TAC MOD_LT[`i':num`;`k_sy(s:stable_sy)`]
 307 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th])
 308 THEN REPEAT DISCH_TAC
 309 THEN MP_TAC(ARITH_RULE`i' < k_sy s==> 1+i' = k_sy (s:stable_sy) \/ 1+ i'  < k_sy s `)
 310 THEN RESA_TAC;
 311 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
 312 THEN REPEAT DISCH_TAC
 313 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
 314 THEN RESA_TAC
 315 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 316 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
 317 THEN REPEAT DISCH_TAC
 318 THEN MP_TAC(ARITH_RULE`1<= i==> ~(i=0)/\ ~(0=2)`)
 319 THEN RESA_TAC
 320 THEN MP_TAC(SET_RULE`{i', 0} = {i, (1+i) MOD k} /\ ~(i=0)==> i=i'`)
 321 THEN RESA_TAC
 322 THEN MRESA_TAC MOD_LT[`i':num`;`k_sy(s:stable_sy)`];
 323 MP_TAC(ARITH_RULE`i <= k-1 /\ 2< k==> 1+i  = k \/ 1+i < k `)
 324 THEN RESA_TAC;
 325 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
 326 THEN REPEAT DISCH_TAC
 327 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ ~(1+1=k)`)
 328 THEN RESA_TAC
 329 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 330 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+0=1`] )
 331 THEN REPEAT DISCH_TAC
 332 THEN MRESA_TAC MOD_LT[`1+i':num`;`k_sy(s:stable_sy)`]
 333 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
 334 THEN REPEAT DISCH_TAC
 335 THEN MP_TAC(ARITH_RULE`1<= i' ==> ~(i'= 0) /\ ~(1+i'=0)`)
 336 THEN RESA_TAC
 337 THEN MP_TAC(SET_RULE`~(i'= 0) /\ ~(1+i'=0) ==> ~({i', 1+i' } = {i, 0})`)
 338 THEN RESA_TAC;
 339 MRESA_TAC MOD_LT[`1+i':num`;`k_sy(s:stable_sy)`]
 340 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
 341 THEN REPEAT DISCH_TAC
 342 THEN MRESA_TAC MOD_LT[`1+i:num`;`k_sy(s:stable_sy)`]
 343 THEN POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN ASSUME_TAC th)
 344 THEN REPEAT DISCH_TAC
 345 THEN MP_TAC(SET_RULE`{i',1+ i'} = {i,1+ i} ==> i= 1+i' \/ i=i'`)
 346 THEN RESA_TAC;
 347 POP_ASSUM(fun th-> ASM_TAC THEN ONCE_REWRITE_TAC[th] THEN REWRITE_TAC[ARITH_RULE`1+(1+i)=2+i`] )
 348 THEN REPEAT DISCH_TAC
 349 THEN MP_TAC(ARITH_RULE`~(i'= 2+i')`)
 350 THEN RESA_TAC
 351 THEN SUBGOAL_THEN`~({i', 1+i'} = {1+i', 2+i'})` MP_TAC;
 352 POP_ASSUM MP_TAC
 353 THEN MP_TAC(ARITH_RULE`~(i'= 1+i') /\ ~(1+i'= 2+i')`)
 354 THEN SET_TAC[];
 355 RESA_TAC;
 356 MRESA_TAC MOD_LT[`i:num`;`k_sy(s:stable_sy)`];
 357 RESA_TAC
 358 THEN EXISTS_TAC`i:num`
 359 THEN ASM_REWRITE_TAC[]
 360 THEN MP_TAC(ARITH_RULE`i<=k-1  /\ 2<k==> i<= k/\ i<k`)
 361 THEN RESA_TAC
 362 THEN MRESA_TAC MOD_LT[`i:num`;`k_sy(s:stable_sy)`]]);;
 363
 364
 365 let D_FUN_LE=prove_by_refinement(`!s:stable_sy l:real^(M,3)finite_product.
 366 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
 367 /\ d_sy s<= #0.9
 368 /\ pi<= sol_local (E_SY(vecmats l)) (F_SY(vecmats l))
 369 /\ l IN B_SY1 (a_sy s) (b_sy s)
 370 ==> d_fun (s,l) <= #0.92`,
 371 [REPEAT STRIP_TAC
 372 THEN SUBGOAL_THEN `d_fun(s:stable_sy,(l:real^(M,3)finite_product))<= d_sy s+ #0.1 *(cstab- sqrt(&8)) `
 373 ASSUME_TAC;
 374 REWRITE_TAC[d_fun;sigma_sy]
 375 THEN MATCH_MP_TAC(REAL_ARITH`b<=c==> a+ #0.1 * b<=a+ #0.1* c`)
 376 THEN DISJ_CASES_TAC(SET_RULE`~(ear_sy s) \/ (ear_sy (s:stable_sy))`)
 377 THEN ASM_REWRITE_TAC[];
 378 MATCH_MP_TAC(REAL_ARITH`&0<= a/\ &0<= b==> -- &1 *a<=b`);
 379 STRIP_TAC;
 380 MATCH_MP_TAC SUM_POS_LE
 381 THEN REWRITE_TAC[FINITE_J1_SY]
 382 THEN REWRITE_TAC[J1_SY;IN_ELIM_THM]
 383 THEN REPEAT STRIP_TAC
 384 THEN ASM_REWRITE_TAC[]
 385 THEN POP_ASSUM MP_TAC
 386 THEN POP_ASSUM MP_TAC
 387 THEN ASM_REWRITE_TAC[IN_NUMSEG]
 388 THEN STRIP_TAC
 389 THEN MRESA_TAC (GEN_ALL B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
 390 THEN POP_ASSUM MP_TAC
 391 THEN REAL_ARITH_TAC;
 392 REWRITE_TAC[REAL_ARITH`&0<= a-b<=> b<=a`;cstab]
 393 THEN MATCH_MP_TAC REAL_LE_LSQRT
 394 THEN REAL_ARITH_TAC;
 395 MRESAL_TAC(GEN_ALL SING_J1_SY)[`k:num`;`s:stable_sy`][SUM_SING;REAL_ARITH`&1 *A=A`;REAL_ARITH`A-B<= A-C<=> C<=B`]
 396 THEN MP_TAC(ARITH_RULE`i<=k==> i=k \/ i< k:num`)
 397 THEN RESA_TAC;
 398 MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ 1<=k/\ k<=k `)
 399 THEN RESA_TAC
 400 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
 401 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ k+k=k *2`]
 402 THEN MRESA_TAC MOD_LT[`1:num`;`k_sy(s:stable_sy)`]
 403 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
 404 THEN MRESA_TAC MOD_ADD_MOD[`1:num`;`k:num`;`k:num`]
 405 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
 406 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num/\ 1+0=1`;IN_SING]
 407 THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`1`])
 408 THEN REMOVE_ASSUM_TAC
 409 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 410 THEN REMOVE_ASSUM_TAC
 411 THEN REMOVE_ASSUM_TAC
 412 THEN POP_ASSUM MP_TAC
 413 THEN REWRITE_TAC[constraint_system]
 414 THEN STRIP_TAC
 415 THEN REMOVE_ASSUM_TAC
 416 THEN REMOVE_ASSUM_TAC
 417 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1`;`k:num`][ARITH_RULE`A+0=A/\ k+k= k* 2`])
 418 THEN REMOVE_ASSUM_TAC
 419 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 420 THEN FIND_ASSUM MP_TAC`(l:real^(M,3)finite_product) IN B_SY1 (a_sy s) (b_sy (s:stable_sy))`
 421 THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION1_SY]
 422 THEN STRIP_TAC
 423 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
 424 THEN REMOVE_ASSUM_TAC
 425 THEN REMOVE_ASSUM_TAC
 426 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`k:num`;`1:num`][ARITH_RULE`1<=1`]);
 427 MRESA_TAC MOD_LT[`i:num`;`k_sy(s:stable_sy)`]
 428 THEN MP_TAC(ARITH_RULE`2<k==> ~(k=0)/\ 1<k/\ ~(0=1) /\ 1<=k/\ k<=k `)
 429 THEN RESA_TAC
 430 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`1+i:num`;`k:num`]
 431 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ k+k=k *2`]
 432 THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`1+i:num`][ARITH_RULE`1*A=A`]
 433 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num/\ 0+1=1`;IN_SING]
 434 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`;`(1+i) MOD k`])
 435 THEN REMOVE_ASSUM_TAC
 436 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 437 THEN REMOVE_ASSUM_TAC
 438 THEN REMOVE_ASSUM_TAC
 439 THEN POP_ASSUM MP_TAC
 440 THEN REWRITE_TAC[constraint_system]
 441 THEN STRIP_TAC
 442 THEN REMOVE_ASSUM_TAC
 443 THEN REMOVE_ASSUM_TAC
 444 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`1+i:num`][ARITH_RULE`A+0=A`])
 445 THEN REMOVE_ASSUM_TAC
 446 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 447 THEN MP_TAC(ARITH_RULE`i<k==> 1<= 1+i /\ 1+i<=k`)
 448 THEN RESA_TAC
 449 THEN FIND_ASSUM MP_TAC`(l:real^(M,3)finite_product) IN B_SY1 (a_sy s) (b_sy (s:stable_sy))`
 450 THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION1_SY]
 451 THEN STRIP_TAC
 452 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID;ADD1]
 453 THEN REMOVE_ASSUM_TAC
 454 THEN REMOVE_ASSUM_TAC
 455 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`1+i:num`][ARITH_RULE`1<=1`])
 456 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=1/\ 1+i= SUC i`;ADD1]
 457 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+1=1+i`]
 458 THEN ASM_REWRITE_TAC[];
 459 MATCH_MP_TAC(REAL_ARITH`d_fun (s,l) <= d_sy s + #0.1 * (cstab - sqrt (&8))
 460 /\ d_sy s <= #0.9 /\ cstab - sqrt (&8)<= #0.2
 461 ==> d_fun (s,l) <= #0.92`)
 462 THEN ASM_REWRITE_TAC[cstab;REAL_ARITH`#3.01 - sqrt (&8) <= #0.2 <=> #2.81 <= sqrt (&8) `]
 463 THEN MATCH_MP_TAC REAL_LE_RSQRT
 464 THEN REAL_ARITH_TAC]);;
 465
 466
 467 let TAU_FUN_LE=prove_by_refinement(`!s:stable_sy l:real^(M,3)finite_product.
 468 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
 469 /\ pi<= sol_local (E_SY(vecmats l)) (F_SY(vecmats l))
 470 /\ l IN B_SY1 (a_sy s) (b_sy s)
 471 ==> #0.92< tau_fun (V_SY(vecmats l)) (E_SY(vecmats l)) (F_SY(vecmats l))`,
 472 [REPEAT STRIP_TAC
 473 THEN ASM_SIMP_TAC[tau_fun;rho_fun]
 474 THEN MRESA_TAC (GEN_ALL CARD_F_SY_IN_B_SY)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
 475 THEN MRESA1_TAC (GEN_ALL FINITE_F_SY)`l:real^(M,3)finite_product`
 476 THEN ASM_SIMP_TAC[REAL_ARITH`(&1+B)*C=C+B*C`;SUM_ADD]
 477 THEN SUBGOAL_THEN`&0<= sum (F_SY (vecmats l))
 478   (\x. (inv (&2 * h0 - &2) * inv pi * sol0 * (norm (FST x) - &2)) *
 479        azim_in_fan x (E_SY (vecmats (l:real^(M,3)finite_product))))`ASSUME_TAC;
 480 MATCH_MP_TAC SUM_POS_LE
 481 THEN ASM_REWRITE_TAC[]
 482 THEN REPEAT STRIP_TAC
 483 THEN MATCH_MP_TAC REAL_LE_MUL
 484 THEN STRIP_TAC;
 485 MATCH_MP_TAC REAL_LE_MUL
 486 THEN STRIP_TAC;
 487 REWRITE_TAC[REAL_LE_INV_EQ;h0]
 488 THEN REAL_ARITH_TAC;
 489 MATCH_MP_TAC REAL_LE_MUL
 490 THEN STRIP_TAC;
 491 REWRITE_TAC[REAL_LE_INV_EQ;]
 492 THEN MATCH_MP_TAC(REAL_ARITH`&0<a==> &0 <= a`)
 493 THEN REWRITE_TAC[PI_WORKS];
 494 MATCH_MP_TAC REAL_LE_MUL
 495 THEN STRIP_TAC;
 496 MATCH_MP_TAC(REAL_ARITH`&0<a==> &0 <= a`)
 497 THEN REWRITE_TAC[SOL0_POS];
 498 POP_ASSUM MP_TAC
 499 THEN REMOVE_ASSUM_TAC
 500 THEN REMOVE_ASSUM_TAC
 501 THEN POP_ASSUM MP_TAC
 502 THEN REWRITE_TAC[B_SY1;IN_ELIM_THM]
 503 THEN STRIP_TAC
 504 THEN POP_ASSUM MP_TAC
 505 THEN REMOVE_ASSUM_TAC
 506 THEN REMOVE_ASSUM_TAC
 507 THEN POP_ASSUM MP_TAC
 508 THEN DISCH_THEN(LABEL_TAC"THY")
 509 THEN STRIP_TAC
 510 THEN ASM_REWRITE_TAC[IN_ELIM_THM;F_SY]
 511 THEN RESA_TAC
 512 THEN REMOVE_THEN"THY"(fun th-> MRESAL1_TAC th `i:num`[VECMATS_MATVEC_ID;ball_annulus;IN_ELIM_THM;DIFF;ball;dist;VECTOR_ARITH`vec 0-A = --A`;NORM_NEG])
 513 THEN POP_ASSUM MP_TAC
 514 THEN REAL_ARITH_TAC;
 515 POP_ASSUM MP_TAC
 516 THEN REMOVE_ASSUM_TAC
 517 THEN REMOVE_ASSUM_TAC
 518 THEN POP_ASSUM MP_TAC
 519 THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;convex_local_fan]
 520 THEN STRIP_TAC
 521 THEN STRIP_TAC
 522 THEN ASM_SIMP_TAC[azim;VECMATS_MATVEC_ID]
 523 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`x:real^3#real^3`][VECMATS_MATVEC_ID;azim];
 524 MATCH_MP_TAC(REAL_ARITH`
 525 &0<= sum (F_SY (vecmats l))
 526   (\x. (inv (&2 * h0 - &2) * inv pi * sol0 * (norm (FST x) - &2)) *
 527        azim_in_fan x (E_SY (vecmats (l:real^(M,3)finite_product))))
 528 /\
 529 #0.92 <
 530 sum (F_SY (vecmats l)) (\x. azim_in_fan x (E_SY (vecmats l)))  -
 531  (pi + sol0) * &(k-2)
 532 ==> #0.92 <
 533  (sum (F_SY (vecmats l)) (\x. azim_in_fan x (E_SY (vecmats l))) +
 534   sum (F_SY (vecmats l))
 535   (\x. (inv (&2 * h0 - &2) * inv pi * sol0 * (norm (FST x) - &2)) *
 536        azim_in_fan x (E_SY (vecmats l)))) -
 537  (pi + sol0) * &(k-2)`)
 538 THEN ASM_REWRITE_TAC[]
 539 THEN ONCE_REWRITE_TAC[ARITH_RULE`azim_in_fan x (E_SY (vecmats l))
 540 =(azim_in_fan x (E_SY (vecmats l)) -pi)+pi`]
 541 THEN ASM_SIMP_TAC[SUM_ADD;SUM_CONST;]
 542 THEN MP_TAC(ARITH_RULE`2< k==> 2<=k `)
 543 THEN RESA_TAC
 544 THEN MRESA_TAC REAL_OF_NUM_SUB[`2`;`k:num`]
 545 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 546 THEN REWRITE_TAC[REAL_ARITH`(sum (F_SY (vecmats l)) (\x. azim_in_fan x (E_SY (vecmats l)) - pi) +
 547   &k * pi) -
 548  (pi + sol0) * (&k - &2)
 549 =(&2 *pi+ sum (F_SY (vecmats l)) (\x. azim_in_fan x (E_SY (vecmats l)) - pi)) +
 550  sol0 *  &2 - sol0 * &k`;GSYM sol_local]
 551 THEN MATCH_MP_TAC(REAL_ARITH`
 552 pi<=  sol_local (E_SY (vecmats l)) (F_SY (vecmats (l:real^(M,3)finite_product)))
 553 /\
 554 #0.92 <
 555 pi + sol0 * &2 - sol0 * &k
 556 ==>
 557 #0.92 <
 558  sol_local (E_SY (vecmats l)) (F_SY (vecmats l)) + sol0 * &2 - sol0 * &k`)
 559 THEN ASM_REWRITE_TAC[]
 560 THEN MRESA1_TAC stable_sy_lemma`s:stable_sy`
 561 THEN POP_ASSUM MP_TAC
 562 THEN REWRITE_TAC[stable_system;constraint_system]
 563 THEN STRIP_TAC
 564 THEN MRESA_TAC REAL_OF_NUM_LE[`k:num`;`6:num`]
 565 THEN MATCH_MP_TAC(REAL_ARITH`
 566 sol0 * &k<= sol0 * &6
 567 /\ #0.92 < pi + sol0 * &2 - sol0 * &6
 568 ==> #0.92 < pi + sol0 * &2 - sol0 * &k`)
 569 THEN STRIP_TAC;
 570 MATCH_MP_TAC REAL_LE_LMUL
 571 THEN ASM_REWRITE_TAC[]
 572 THEN MATCH_MP_TAC(REAL_ARITH`&0< a==> &0<= a`)
 573 THEN REWRITE_TAC[SOL0_POS];
 574 REWRITE_TAC[REAL_ARITH`pi + sol0 * &2 - sol0 * &6= pi - sol0 * &4`;]
 575 THEN MATCH_MP_TAC(REAL_ARITH`sol0 < #0.551286 /\ #3.14159 < pi ==> #0.92 < pi - sol0 * &4`)
 576 THEN REWRITE_TAC[Flyspeck_constants.bounds]]);;
 577
 578 let TAU_STAR_POS=prove(`!s:stable_sy l:real^(M,3)finite_product.
 579 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
 580 /\ d_sy s<= #0.9
 581 /\ pi<= sol_local (E_SY(vecmats l)) (F_SY(vecmats l))
 582 /\ l IN B_SY1 (a_sy s) (b_sy s)
 583 ==> &0< tau_star s l`,
 584 REWRITE_TAC[tau_star;]
 585 THEN REPEAT STRIP_TAC
 586 THEN MRESA_TAC (GEN_ALL TAU_FUN_LE)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
 587 THEN MRESA_TAC (GEN_ALL D_FUN_LE)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
 588 THEN POP_ASSUM MP_TAC
 589 THEN POP_ASSUM MP_TAC
 590 THEN REAL_ARITH_TAC);;
 591
 592 let CIRCULAR_SOL_EQ_2PI=prove(`convex_local_fan (V,E,FF) /\ circular V E
 593 ==> sol_local E FF= &2 *pi`,
 594 REPEAT STRIP_TAC
 595 THEN POP_ASSUM MP_TAC
 596 THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[convex_local_fan] THEN STRIP_TAC THEN ASSUME_TAC th)
 597 THEN STRIP_TAC
 598 THEN REWRITE_TAC[sol_local;REAL_ARITH`A+B=A<=> B= &0`]
 599 THEN MATCH_MP_TAC SUM_EQ_0
 600 THEN REPEAT STRIP_TAC
 601 THEN REWRITE_TAC[REAL_ARITH`A-B= &0<=> A=B`]
 602 THEN POP_ASSUM MP_TAC
 603 THEN DISCH_THEN(LABEL_TAC "THY")
 604 THEN MRESA_TAC (GEN_ALL LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;]
 605 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:real^3#real^3`)
 606 THEN REMOVE_THEN "THY"MP_TAC
 607 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 608 THEN STRIP_TAC
 609 THEN MRESA_TAC(GEN_ALL LOCAL_FAN_IMP_IN_V)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 (FF:real^3#real^3->bool) (FST (x:real^3#real^3))`;`V:real^3->bool`]
 610 THEN MRESA_TAC (GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`E:(real^3->bool)->bool`]
 611 THEN POP_ASSUM(fun th-> MRESA1_TAC th`FST (x:real^3#real^3)`)
 612 THEN MRESA_TAC (GEN_ALL Local_lemmas.KCHMAMG)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;]
 613 THEN REMOVE_ASSUM_TAC
 614 THEN REMOVE_ASSUM_TAC
 615 THEN REMOVE_ASSUM_TAC
 616 THEN REMOVE_ASSUM_TAC
 617 THEN REMOVE_ASSUM_TAC
 618 THEN REMOVE_ASSUM_TAC
 619 THEN POP_ASSUM(fun th-> MRESA1_TAC th`FST (x:real^3#real^3)`));;
 620
 621 let NOT_CIRCULAR_SY=prove(`!s:stable_sy l:real^(M,3)finite_product.
 622 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
 623 /\ d_sy s<= #0.9
 624 /\ tau_star s l <= &0
 625 /\ l IN B_SY1 (a_sy s) (b_sy s)
 626 ==> ~(circular (V_SY(vecmats l)) (E_SY(vecmats l)))`,
 627 REPEAT STRIP_TAC
 628 THEN ASM_TAC
 629 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
 630 THEN REPEAT STRIP_TAC
 631 THEN POP_ASSUM MP_TAC
 632 THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;CONDITION1_SY] THEN STRIP_TAC)
 633 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
 634 THEN POP_ASSUM MP_TAC
 635 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 636 THEN POP_ASSUM MP_TAC
 637 THEN POP_ASSUM MP_TAC
 638 THEN POP_ASSUM MP_TAC
 639 THEN DISCH_THEN(LABEL_TAC"THY")
 640 THEN DISCH_THEN(LABEL_TAC"THY2")
 641 THEN STRIP_TAC
 642 THEN POP_ASSUM(fun th-> MP_TAC th
 643 THEN REWRITE_TAC[convex_local_fan]
 644 THEN STRIP_TAC
 645 THEN POP_ASSUM MP_TAC
 646 THEN POP_ASSUM(fun th1-> MP_TAC th1
 647 THEN REWRITE_TAC[local_fan]
 648 THEN LET_TAC
 649 THEN STRIP_TAC
 650 THEN POP_ASSUM MP_TAC
 651 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
 652 THEN STRIP_TAC
 653 THEN ASSUME_TAC th1)
 654 THEN DISCH_THEN(LABEL_TAC"THY1")
 655 THEN ASSUME_TAC th)
 656 THEN STRIP_TAC
 657 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
 658 THEN  STRIP_TAC
 659 THEN MRESA_TAC(GEN_ALL CIRCULAR_SOL_EQ_2PI)[`V_SY(vecmats (l:real^(M,3)finite_product))`;`E_SY(vecmats (l:real^(M,3)finite_product))`;`F_SY(vecmats (l:real^(M,3)finite_product))`]
 660 THEN MP_TAC(REAL_ARITH`&0< pi ==> pi <= &2 * pi`)
 661 THEN REWRITE_TAC[PI_WORKS]
 662 THEN RESA_TAC
 663 THEN MRESA_TAC (GEN_ALL TAU_STAR_POS)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
 664 THEN POP_ASSUM MP_TAC
 665 THEN ASM_REWRITE_TAC[REAL_ARITH`~(&0< A) <=> A <= &0`]);;
 666
 667
 668 let GBYCPXS
 669 = prove(`!s:stable_sy l:real^(M,3)finite_product.
 670 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
 671 /\ l IN B_SY1 (a_sy s) (b_sy s)
 672 ==>
 673 (d_sy s<= #0.9
 674 /\ pi<= sol_local (E_SY(vecmats l)) (F_SY(vecmats l))
 675 /\ l IN B_SY1 (a_sy s) (b_sy s)
 676 ==> &0< tau_star s l)
 677 /\ (d_sy s<= #0.9
 678 /\ tau_star s l <= &0
 679 ==> ~(circular (V_SY(vecmats l)) (E_SY(vecmats l))))`,
 680 REPEAT STRIP_TAC
 681 THEN MRESA_TAC (GEN_ALL TAU_STAR_POS)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
 682 THEN MRESA_TAC (GEN_ALL NOT_CIRCULAR_SY)[`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]);;
 683
 684
 685
 686
 687
 688 end;;
 689
 690