(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)




module   Pcrttid= struct





open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;



let tri_stable=new_definition
`tri_stable k d s a b J f<=> 
constraint_system k d s a b J f /\ k=3
/\ 
(!i j. i IN s /\ j IN s /\ ~(i=j) ==> &2<= a(i,j)) /\
(!i. i IN s==> a(i,i)= &0 /\ b(i,f i)< &4)/\
(!i j.  {i,j} IN J ==> a(i,j)= sqrt(&8) /\ b(i,j) =cstab)`;;


let EAR_TRI_STABLE_SYSTEM=
prove_by_refinement(
`tri_stable 3 ((#0.11)) (0..2) (a_ear0 {{1,2}}) (b_ear0 {{1,2}})  ({{1,2}}) (\i. (1 + i) MOD 3)`,

[
MRESAL_TAC HAS_SIZE_NUMSEG[`0`;`2`][ARITH_RULE`(2+1)-0=3`]
THEN ASM_SIMP_TAC[tri_stable;constraint_system;torsor;ARITH_RULE`3<= 3 /\3<=6/\ 1+3<=6/\ (2+1)-0=3/\ 3=3`;CARD_NUMSEG;Hypermap.CARD_SINGLETON;]
THEN REMOVE_ASSUM_TAC
THEN STRIP_TAC;
STRIP_TAC;
STRIP_TAC;
REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`2`[ARITH_RULE`SUC 2=3`];
STRIP_TAC;
REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`3`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=3<=> A<=2)`]
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;
STRIP_TAC;
REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`0<i==> 1<= i /\ 1<3`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`i:num`]
THEN MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC
THEN ARITH_TAC;
REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
THEN REPEAT STRIP_TAC
THEN ASSUME_TAC(ARITH_RULE`1<=3 /\1<3/\ 1<=2`)
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`3:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`x:num`][ARITH_RULE`1*3=3`]
THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC
THEN ARITH_TAC;
STRIP_TAC;
REWRITE_TAC[b_ear0;a_ear0]
THEN REPEAT GEN_TAC
THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =j MOD 3 \/ ~(i  MOD 3 =j MOD 3:num)`);
ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`];
ASM_REWRITE_TAC[]
THEN  DISJ_CASES_TAC(SET_RULE`{i MOD 3,j MOD 3} IN {{1,2}} \/ ~({i MOD 3,j MOD 3} IN {{1,2}})`);
ASM_REWRITE_TAC[IN_SING]
THEN ONCE_REWRITE_TAC[SET_RULE`{i  MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i  MOD 3}= {1,2}`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN_SING;cstab]
THEN RESA_TAC
THEN MATCH_MP_TAC REAL_LE_LSQRT
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[IN_SING]
THEN ONCE_REWRITE_TAC[SET_RULE`{i MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i MOD 3}= {1,2}`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[IN_SING;h0]
THEN RESA_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC;
REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`1<= 3 /\ 1<3`)
THEN RESA_TAC
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`j:num`][ARITH_RULE`1*3=3`]
THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`j:num`;`3:num`]
THEN SIMP_TAC[b_ear0;a_ear0;ARITH_RULE`A+0=A`;MOD_MOD_REFL;ARITH_RULE`~(3=0)`];
REWRITE_TAC[SUBSET;IN_SING;IN_ELIM_THM;IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[ARITH_RULE`0<=1 /\ 1<=2/\ (1 +1 ) MOD 3= 2`];
STRIP_TAC;
REWRITE_TAC[a_ear0;IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`i<= 2/\ j<= 2==> i< 3 /\ j< 3`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`i:num`;`3`]
THEN MRESA_TAC MOD_LT[`j:num`;`3`]
THEN  DISJ_CASES_TAC(SET_RULE`{i,j} IN {{1,2}} \/ ~({i,j} IN {{1,2}})`);
ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC REAL_LE_RSQRT
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;
STRIP_TAC;
REWRITE_TAC[b_ear0;a_ear0;MOD_MOD_REFL]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =(1+i) MOD 3 MOD 3\/ ~(i  MOD 3 =(1+i) MOD 3 MOD 3:num)`);
ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`;cstab]
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[]
THEN  DISJ_CASES_TAC(SET_RULE`{i MOD 3,(1+i) MOD 3 MOD 3} IN {{1,2}} \/ ~({i MOD 3,(1+i) MOD 3 MOD 3} IN {{1,2}})`);
ASM_REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;
REWRITE_TAC[IN_SING;a_ear0;b_ear0]
THEN REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`{i,j}={1,2} /\ ~(1=2) ==> ~(i=j) /\ (i =1\/ i=2) /\ (j=1\/ j=2)`)
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=2)`]
THEN DISCH_TAC
THEN MP_TAC(ARITH_RULE`(i =1\/ i=2) /\ (j=1\/ j=2)==> i< 3 /\ j< 3`)
THEN RESA_TAC
THEN MRESA_TAC MOD_LT[`i:num`;`3`]
THEN MRESA_TAC MOD_LT[`j:num`;`3`]]);;



let exist_tri_stable=
prove_by_refinement(`?s:(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num)). tri_stable (FST s) (FST (SND s)) (FST (SND (SND s))) (FST (SND (SND (SND s)))) (FST(SND (SND (SND (SND s))))) (FST (SND (SND (SND (SND (SND s)))))) 
(SND(SND (SND (SND (SND (SND s))))))`,

[EXISTS_TAC`3, (#0.11), (0..2), (a_ear0 {{1,2}}), (b_ear0 {{1,2}}), ({{1,2}}),(\i. (1 + i) MOD 3)`
THEN REWRITE_TAC[EAR_TRI_STABLE_SYSTEM]]);;

let tri_sy_tybij = (new_type_definition "tri_sy" ("tri_sy", "tuple_tri_sy")exist_tri_stable);;


let k_ts = new_definition `k_ts (s:tri_sy) = FST (tuple_tri_sy s)`;;
let d_ts = new_definition `d_ts (s:tri_sy) = (FST (SND (tuple_tri_sy s)))`;;
let I_TS = new_definition `I_TS (s:tri_sy) = (FST (SND (SND  (tuple_tri_sy s))))`;;
let a_ts = new_definition `a_ts (s:tri_sy) = (FST (SND (SND (SND (tuple_tri_sy s)))))`;;
let b_ts = new_definition `b_ts (s:tri_sy) = (FST(SND (SND (SND (SND (tuple_tri_sy s)))))) `;;

let J_TS = new_definition `J_TS (s:tri_sy) = (FST (SND (SND (SND (SND (SND  (tuple_tri_sy s))))))) `;;
let f_ts = new_definition `f_ts (s:tri_sy) = (SND(SND (SND (SND (SND (SND  (tuple_tri_sy s)))))))`;;


let tri_sy_lemma=
prove(`!s:tri_sy. tri_stable (k_ts s) (d_ts s) (I_TS s) (a_ts s) (b_ts s) (J_TS s) (f_ts s)`,

   ASM_REWRITE_TAC[tri_sy_tybij;k_ts;d_ts;I_TS; a_ts; b_ts; J_TS; f_ts]);;





let augmented_constraint_system1=new_definition
`augmented_constraint_system1 (s:stable_sy) I_lo I_str a b m <=>
d_sy s <= # 0.9
/\ m=CARD {i | i IN I_SY s /\ (?j. j IN I_SY s /\( &2< a_sy s (i,j) \/ &2* h0< b_sy s (i,j)))} DIV 2
/\ m+k_sy s <= 6
/\ (!i j. i IN I_SY s /\ j IN I_SY s ==>
a_sy s (i,j)<= a (i,j)
/\ a (i,j)<= b (i,j)
/\ b (i,j)<= b_sy s (i,j))`;;


let augmented_constraint_system2=new_definition
`augmented_constraint_system3 (s:tri_sy) I_lo I_str a b m <=>
d_ts s <= # 0.9
/\ m=CARD {i | i IN I_TS s /\ (?j. j IN I_TS s /\( &2< a_ts s (i,j) \/ &2* h0< b_ts s (i,j)))} DIV 2
/\ m+k_ts s <= 6
/\ (!i j. i IN I_TS s /\ j IN I_TS s ==>
a_ts s (i,j)<= a (i,j)
/\ a (i,j)<= b (i,j)
/\ b (i,j)<= b_ts s (i,j))`;;



let CLOSED_TRI_SY=
prove_by_refinement(`
tri_stable k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
/\ 2<k
==> 
closed {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }`,

[REWRITE_TAC[CONDITION2_SY;CONDITION1_SY;tri_stable]
THEN  REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN  REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist] 
THEN REPEAT STRIP_TAC
THEN ASM_TAC
THEN DISCH_THEN(LABEL_TAC"THYGIANG2")
THEN DISCH_THEN(LABEL_TAC"THYGIANG")
THEN DISCH_THEN(LABEL_TAC"THYGIANG1")
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`vecmats (l:real^(M,3)finite_product)`
THEN SIMP_TAC[MATVEC_VECMATS_ID]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN   REWRITE_TAC[SKOLEM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN  DISCH_THEN(LABEL_TAC"THY1")
THEN  DISCH_THEN(LABEL_TAC"THY2")
THEN SUBGOAL_THEN`
!i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M)
==>
((\n. row i (v n) - row j ((v:num->real^3^M) n)) --> row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product)))
 sequentially`ASSUME_TAC;
SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]
THEN REPEAT STRIP_TAC
THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`]
THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`)
THEN RESA_TAC
THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e/ &2:real`)
THEN POP_ASSUM MP_TAC
THEN  DISCH_THEN(LABEL_TAC"THY2")
THEN EXISTS_TAC`N:num`
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`)
THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\  SUC(i-1)=i`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\  SUC(j-1)=j`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`]
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`]
THEN POP_ASSUM MP_TAC
THEN SIMP_TAC[MATVEC_VECMATS_ID]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`((v:num->real^3^M) n)`]
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`vecmats (l:real^(M,3)finite_product)`]
THEN POP_ASSUM MP_TAC
THEN SIMP_TAC[MATVEC_VECMATS_ID]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`j-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]
THEN MRESAL_TAC NORM_TRIANGLE[`row i ((v:num->real^3^M) n) - row i (vecmats (l:real^(M,3)finite_product))`;`--(row j ((v:num->real^3^M) n) - row j (vecmats (l:real^(M,3)finite_product)))`][NORM_NEG;VECTOR_ARITH`A+ --B=A-B:real^N` ]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
SUBGOAL_THEN`
!i. 1 <= i /\ i <= dimindex (:M) ==>
((\n. row i ((v:num->real^3^M) n)) --> row i (vecmats (l:real^(M,3)finite_product)))
 sequentially`ASSUME_TAC;
SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]
THEN REPEAT STRIP_TAC
THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`]
THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`)
THEN RESA_TAC
THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e:real`)
THEN POP_ASSUM MP_TAC
THEN  DISCH_THEN(LABEL_TAC"THY2")
THEN EXISTS_TAC`N:num`
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`)
THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\  SUC(i-1)=i`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\  SUC(j-1)=j`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`]
THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`]
THEN POP_ASSUM MP_TAC
THEN SIMP_TAC[MATVEC_VECMATS_ID]
THEN STRIP_TAC
THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB]
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"YEU2")
THEN SUBGOAL_THEN`(!i j.
      1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M)
      ==> (a:num#num->real) (i,j) <= norm (row i (vecmats l) - row j (vecmats l)) /\
          norm (row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))) <= (b:num#num->real) (i,j))` ASSUME_TAC;
REPEAT STRIP_TAC;
MRESA_TAC LIM_NORM_LBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(a:num#num->real)(i,j)`]
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY];
MRESA_TAC LIM_NORM_UBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(b:num#num->real)(i,j)`]
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY];
ASM_REWRITE_TAC[]
THEN MP_TAC COMPACT_BALL_ANNULUS
THEN ASM_SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED]
THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN  REWRITE_TAC[ IN_ELIM_THM; dist] 
THEN   REWRITE_TAC[SKOLEM_THM]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"YEU")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`(\n. row i ((v:num->real^3^M) n)) `;` row i (vecmats (l:real^(M,3)finite_product))`])
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_SIMP_TAC[]]);;




let BOUNDED_TRI_SY=
prove(`
tri_stable k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
/\  2<k
==> 
bounded {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v}`,

REPEAT STRIP_TAC
THEN MATCH_MP_TAC BOUNDED_SUBSET
THEN EXISTS_TAC`{matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) }`
THEN MP_TAC COMPACT_BALL_ANNULUS_MATVEC
THEN SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED]
THEN RESA_TAC
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM]
THEN SET_TAC[]);;
let COMPACT_TRI_STABLE= 
prove (`
tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
/\ 2<k
==> 
compact {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  }`,

SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED; BOUNDED_TRI_SY; CLOSED_TRI_SY;]
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`2<k ==> 1<k`)
THEN RESA_TAC
THENL[ MRESA_TAC (GEN_ALL BOUNDED_TRI_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;];
MRESA_TAC (GEN_ALL CLOSED_TRI_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;]]);;






let PCRTTID=
prove(`(!d J k a b.
tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
/\ 2<k
==> 
compact {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v  })
/\ (!d J k a b.
stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
/\ 2<k
==> 
compact {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY a b v /\ CONDITION2_SY v })`,

STRIP_TAC
THEN REPEAT GEN_TAC
THEN MESON_TAC[COMPACT_TRI_STABLE;WJSCPRO]);;




end;;