proposition: Lemma norm_clP m th cl : sat m th -> cl \in th -> let norm := norm_cl cl.2 in let beta := m cl.1 in [/\ (norm <= 3)%N, norm == 3%N -> beta = eval_cl m cl.2 & (norm < 3)%N -> size cl.2 == size m -> exists2 dk, dk \in dirr_constt beta & orthogonal (dchi dk) m].
proof: Proof. case: cl => ij kvs /satP thP /thP[wf_ij Uks clP] norm beta. have [[_ ZmL Dm] [o1m ZmR]] := (LmodelP m, RmodelP m). set ks := unzip1 kvs in Uks; pose Aij := [seq m`_k | k <- ks]. have lt_ks k: k \in ks -> (k < size m)%N by case/mapP=> kv /clP[ltk _] ->. have sAm: {subset Aij <= (m : seq _)} by move=> _ /mapP[k /lt_ks ltk ->]; rewrite mem_nth. have o1Aij: orthonormal Aij. have [Um _] := orthonormalP o1m; apply: sub_orthonormal o1m => //. rewrite map_inj_in_uniq // => k1 k2 /lt_ks ltk1 /lt_ks ltk2 /eqP. by apply: contraTeq; rewrite nth_uniq. have [X AijX [Y [defXY oXY oYij]]] := orthogonal_split Aij beta. have{AijX} defX: X = \sum_(xi <- Aij) '[beta, xi] *: xi. have [_ -> ->] := orthonormal_span o1Aij AijX; apply: eq_big_seq => xi CFxi. by rewrite defXY cfdotDl (orthoPl oYij) ?addr0. have ->: eval_cl m kvs = X. rewrite {}defX !big_map; apply: eq_big_seq => kv /clP[_ /eqP->]. by rewrite scaler_int. rewrite -leC_nat -ltC_nat -eqC_nat /=. have <-: '[beta] = 3%:R by rewrite Dm // /dot_ref !eqxx. have <-: '[X] = norm%:R. rewrite {}defX {}/norm cfnorm_sum_orthonormal // {o1Aij oYij sAm}/Aij. transitivity (\sum_(kv <- kvs) `|kv.2%:~R : algC| ^+ 2). by rewrite !big_map; apply: eq_big_seq => kv /clP[_ /eqP->]. rewrite unlock /=; elim: (kvs) => //= [[k v] kvs' ->]. by rewrite -intr_norm -natrX -natrD. rewrite defXY cfnormDd //; split; first by rewrite ler_wpDr ?cfnorm_ge0. by rewrite eq_sym addrC -subr_eq0 addrK cfnorm_eq0 => /eqP->; rewrite addr0. have{ZmL} Zbeta: beta \in 'Z[irr G] by apply: ZmL. have Z_X: X \in 'Z[irr G]. rewrite defX big_seq rpred_sum // => xi /sAm/ZmR Zxi. by rewrite rpredZ_Cint ?Cint_cfdot_vchar. rewrite -ltrBlDl subrr cnorm_dconstt; last first. by rewrite -[Y](addKr X) -defXY addrC rpredB. have [-> | [dk Ydk] _ /eqP sz_kvs] := set_0Vmem (dirr_constt Y). by rewrite big_set0 ltxx. have Dks: ks =i iota 0 (size m). have: {subset ks <= iota 0 (size m)} by move=> k /lt_ks; rewrite mem_iota. by case/uniq_min_size; rewrite // size_iota size_map sz_kvs. suffices o_dk_m: orthogonal (dchi dk) m. exists dk; rewrite // dirr_consttE defX cfdotDl cfdot_suml. rewrite big1_seq ?add0r -?dirr_consttE // => xi /sAm CFxi. by rewrite cfdotC cfdotZr (orthoPl o_dk_m) // mulr0 conjC0. apply/orthoPl=> _ /(nthP 0)[k ltk <-]; have [Um o_m] := orthonormalP o1m. have Z1k: m`_k \in dirr G by rewrite dirrE ZmR ?o_m ?eqxx ?mem_nth. apply: contraTeq Ydk => /eqP; rewrite dirr_consttE cfdot_dirr ?dirr_dchi //. have oYm: '[Y, m`_k] = 0 by rewrite (orthoPl oYij) ?map_f // Dks mem_iota. by do 2?case: eqP => [-> | _]; rewrite // ?cfdotNr oYm ?oppr0 ltxx. 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)