proposition: Lemma O ij12 : is_sat_test (sat_test Otest ij12).
proof: Proof. apply: sat_testP => m th [ij1 kvs1] [ij2 kvs2] /= m_th th_cl1 th_cl2. set cl1eq := _ == 3%N; set cl2eq := _ == 3%N; have [_ _ Dm] := LmodelP m. pose goal (s1 : algCnum) s2 := cl2eq ==> (`|s1 - (dot_ref ij1 ij2)%:~R| <= s2%:R). set kvs := kvs2; set s1 := 0; set s2 := {2}0%N; have thP := satP m_th. have{thP} [[wf_cl1 _ cl1P] [wf_cl2 _ cl2P]] := (thP _ th_cl1, thP _ th_cl2). have: goal (s1%:~R + '[m ij1, eval_cl m kvs]) (if cl1eq then 0%N else s2). apply/implyP=> /(norm_cl_eq3 m_th th_cl2) <-. by rewrite if_same Dm // addrK normr0. have /allP: {subset kvs <= kvs2} by []. rewrite cfdot_sumr unlock; elim: kvs s1 s2 => [|[k v2] kvs IHkvs] s1 s2 /=. by rewrite addr0 /goal -rmorphB pmulrn -!CintrE. case/andP=> kvs2_v /IHkvs{}IHkvs; have{cl2P} [ltk _] := cl2P _ kvs2_v. have [v1 /cl1P[_ /eqP/=Dv1] | kvs1'k] := get_litP. rewrite addrA => gl12; apply: IHkvs; congr (goal (_ + _) _): gl12. by rewrite raddfMz addrC /= Dv1 -mulrzA -rmorphD. move=> gl12; apply: IHkvs; case: ifP gl12 => [/(norm_cl_eq3 m_th th_cl1)->|_]. rewrite cfdot_suml big1_seq ?add0r //= => kv1 kvs1_kv1. have [[ltk1 _] [/orthonormalP[Um oom] _]] := (cl1P _ kvs1_kv1, RmodelP m). rewrite -!scaler_int cfdotZl cfdotZr oom ?mem_nth ?nth_uniq // mulrb. by rewrite ifN ?mulr0 //; apply: contraNneq kvs1'k => <-; apply: map_f. rewrite /goal -(lerD2r 1) -mulrSr; case: (cl2eq) => //; apply: le_trans. set s := '[_, _]; rewrite -[_ + _](addrK s) (le_trans (ler_normB _ _)) //. rewrite 2![_ + s]addrAC addrA lerD2l {}/s -scaler_int cfdotZr rmorph_int. have [|v1 _] := sat_cases k m_th th_cl1; first exact/andP. have [th1 -> /= [th1_cl1 _] m_th1] := ext_clP k v1 th_cl1. have [_ _ /(_ _ (mem_head _ _))[_ /eqP->]] := satP m_th1 _ th1_cl1. have ubv1: (`|v1| <= 1)%N := norm_lit m_th1 th1_cl1 (mem_head _ _). have ubv2: (`|v2| <= 1)%N := norm_lit m_th th_cl2 kvs2_v. by rewrite -rmorphM -intr_norm lern1 abszM /= (leq_mul ubv2 ubv1). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)