proposition: Lemma FTtype345_noncoherence_main : False.
proof: Proof. have [S pairMS [xdefW [U StypeP]]] := FTtypeP_pair_witness maxM MtypeP. have [[_ _ maxS] _] := pairMS; rewrite {1}(negPf notMtype2) /= => Stype2 _ _. pose H := (S`_\F)%G; pose HU := (S^`(1))%G. have [[_ hallW2 _ defS] [_ _ nUW2 defHU] _ [_ _ sW1H _ _] _] := StypeP. have ntU: U :!=: 1%g by have [[]] := compl_of_typeII maxS StypeP Stype2. pose G01 := [set g : gT | coprime #[g] w1]. pose G0 := ~: 'A~(M) :&: G01; pose G1 := ~: 'A~(M) :\: G01. pose chi := zeta^\tau1; pose ddAM := FT_Dade_hyp maxM; pose rho := invDade ddAM. have Suzuki: #|G|%:R^-1 * (\sum_(g in ~: 'A~(M)) `|chi g| ^+ 2 - #|~: 'A~(M)|%:R) + '[rho chi] - #|'A(M)|%:R / #|M|%:R <= 0. - pose A_ (_ : 'I_1) := ddAM; pose Atau i := Dade_support (A_ i). have tiA i j : i != j -> [disjoint Atau i & Atau j] by rewrite !ord1. have Nchi1: '[chi] = 1 by have [[->]] := cohS; rewrite ?mem_zchar ?irrWnorm. have:= Dade_cover_inequality tiA Nchi1; rewrite /= !big_ord1 -/rho -addrA. by congr (_ * _ + _ <= 0); rewrite FT_Dade_supportE setTD. have{Suzuki} ub_rho: '[rho chi] <= #|'A(M)|%:R / #|M|%:R + #|G1|%:R / #|G|%:R. rewrite addrC -subr_le0 opprD addrCA (le_trans _ Suzuki) // -addrA. rewrite lerD2r -(cardsID G01 (~: _)) (big_setID G01) -/G0 -/G1 /=. rewrite mulrC mulrBr lerBrDl -mulrBr natrD addrK. rewrite ler_wpM2l ?invr_ge0 ?ler0n // -sumr_const ler_wpDr //. by apply: sumr_ge0 => g; rewrite exprn_ge0 ?normr_ge0. apply: ler_sum => g; rewrite !inE => /andP[notAg] /(zeta_tau1_coprime notAg). by rewrite expr_ge1 ?normr_ge0. have lb_M'bar: (w1 * 2 <= #|M' / M''|%g.-1)%N. suffices ->: w1 = #|W1 / M''|%g. rewrite muln2 -ltnS prednK ?cardG_gt0 //. by rewrite (ltn_odd_Frobenius_ker frobMbar) ?quotient_odd ?mFT_odd. have [_ sW1M _ _ tiM'W1] := sdprod_context defM. apply/card_isog/quotient_isog; first exact: subset_trans (der_norm 2 M). by apply/trivgP; rewrite -tiM'W1 setSI ?normal_sub. have lb_rho: 1 - w1%:R / #|M'|%:R <= '[rho chi]. have cohS_A: coherent_with calS M^# (Dade ddAM) tau1. have [Itau1 _] := cohS; split=> // phi; rewrite zcharD1_seqInd // => Sphi. by rewrite Dtau1 // FT_DadeE // defA (zchar_on Sphi). rewrite {ub_rho}/rho [w1](index_sdprod defM); rewrite defA in (ddAM) cohS_A *. have [||_ [_ _ [] //]] := Dade_Ind1_sub_lin cohS_A _ irr_zeta Szeta. - by apply: seqInd_nontrivial Szeta; rewrite ?mem_irr ?mFT_odd. - by rewrite -(index_sdprod defM). rewrite -(index_sdprod defM) ler_pdivlMr ?ltr0n // -natrM. rewrite -leC_nat in lb_M'bar; apply: le_trans lb_M'bar _. rewrite lerBrDl -mulrS prednK ?cardG_gt0 // leC_nat. by rewrite dvdn_leq ?dvdn_quotient. have{lb_rho ub_rho}: 1 - #|G1|%:R / #|G|%:R - w1%:R^-1 < w1%:R / #|M'|%:R :> algC. - rewrite -addrA -opprD ltrBlDr -ltrBlDl. apply: le_lt_trans (le_trans lb_rho ub_rho) _; rewrite addrC ltrD2l. rewrite ltr_pdivrMr ?gt0CG // mulrC -(sdprod_card defM) natrM. by rewrite mulfK ?neq0CG // defA ltC_nat (cardsD1 1%g M') group1. have frobHU: [Frobenius HU with kernel H] by apply: Frob_der1_type2. have tiH: normedTI H^# G S. by have [_ _] := FTtypeII_ker_TI maxS Stype2; rewrite FTsupp1_type2. have sG1_HVG: G1 \subset class_support H^# G :|: class_support V G. apply/subsetP=> x; rewrite !inE coprime_has_primes ?cardG_gt0 // negbK. case/andP=> /hasP[p W1p]; rewrite /= mem_primes => /and3P[p_pr _ p_dv_x] _. have [a x_a a_p] := Cauchy p_pr p_dv_x. have nta: a != 1%g by rewrite -order_gt1 a_p prime_gt1. have ntx: x != 1%g by apply: contraTneq x_a => ->; rewrite /= cycle1 inE. have cxa: a \in 'C[x] by rewrite -cent_cycle (subsetP (cycle_abelian x)). have hallH: \pi(H).-Hall(G) H by apply: Hall_pi; have [] := FTcore_facts maxS. have{a_p} p_a: p.-elt a by rewrite /p_elt a_p pnat_id. have piHp: p \in \pi(H) by rewrite (piSg _ W1p). have [y _ Hay] := Hall_pJsub hallH piHp (subsetT _) p_a. do [rewrite -cycleJ cycle_subG; set ay := (a ^ y)%g] in Hay. rewrite -[x](conjgK y); set xy := (x ^ y)%g. have caxy: xy \in 'C[ay] by rewrite cent1J memJ_conjg cent1C. have [ntxy ntay]: xy != 1%g /\ ay != 1%g by rewrite !conjg_eq1. have Sxy: xy \in S. have H1ay: ay \in H^# by apply/setD1P. by rewrite (subsetP (cent1_normedTI tiH H1ay)) ?setTI. have [HUxy | notHUxy] := boolP (xy \in HU). rewrite memJ_class_support ?inE ?ntxy //=. have [_ _ _ regHUH] := Frobenius_kerP frobHU. by rewrite (subsetP (regHUH ay _)) // inE ?HUxy // inE ntay. suffices /imset2P[xyz z Vxzy _ ->]: xy \in class_support V S. by rewrite -conjgM orbC memJ_class_support ?in_setT //=. rewrite /V setUC -(FTsupp0_typeP maxS StypeP) !inE Sxy. rewrite andb_orr andNb (contra (subsetP _ _) notHUxy) /=; last first. by apply/bigcupsP=> z _; rewrite (eqP Stype2) setDE -setIA subsetIl. have /Hall_pi hallHU: Hall S HU by rewrite (sdprod_Hall defS). rewrite (eqP Stype2) -(mem_normal_Hall hallHU) ?gFnormal // notHUxy. have /mulG_sub[sHHU _] := sdprodW defHU. rewrite (contra (fun p'xy => pi'_p'group p'xy (piSg sHHU piHp))) //. by rewrite pgroupE p'natE // cycleJ cardJg p_dv_x. have ub_G1: #|G1|%:R / #|G|%:R <= #|H|%:R / #|S|%:R + #|V|%:R / #|W|%:R :> algC. rewrite ler_pdivrMr ?ltr0n ?cardG_gt0 // mulrC mulrDr !mulrA. rewrite ![_ * _ / _]mulrAC -!natf_indexg ?subsetT //= -!natrM -natrD ler_nat. apply: leq_trans (subset_leq_card sG1_HVG) _. rewrite cardsU (leq_trans (leq_subr _ _)) //. have unifJG B C: C \in B :^: G -> #|C| = #|B|. by case/imsetP=> z _ ->; rewrite cardJg. have oTI := card_uniform_partition (unifJG _) (partition_class_support _ _). have{tiH} [ntH tiH /eqP defNH] := and3P tiH. have [_ _ /and3P[ntV tiV /eqP defNV]] := ctiWG. rewrite !oTI // !card_conjugates defNH defNV /= leq_add2r ?leq_mul //. by rewrite subset_leq_card ?subsetDl. rewrite le_gtF // addrAC lerBrDl -lerBrDr (le_trans ub_G1) //. rewrite -(sdprod_card defS) -(sdprod_card defHU) addrC. rewrite -mulnA !natrM invfM mulVKf ?natrG_neq0 // -/w1 -/w2. have sW12_W: W1 :|: W2 \subset W by rewrite -(dprodWY defW) sub_gen. rewrite cardsD (setIidPr sW12_W) natrB ?subset_leq_card // mulrBl. rewrite divff ?natrG_neq0 // -!addrA lerD2l. rewrite cardsU -(dprod_card defW) -/w1 -/w2; have [_ _ _ ->] := dprodP defW. rewrite cards1 natrB ?addn_gt0 ?cardG_gt0 // addnC natrD -addrA mulrDl mulrBl. rewrite {1}mulnC !natrM !invfM !mulVKf ?natrG_neq0 // opprD -addrA lerD2l. rewrite mul1r -{1}[_^-1]mul1r addrC lerNr [- _]opprB -!mulrBl. rewrite -addrA -opprD ler_pdivlMr; last by rewrite natrG_gt0. apply: le_trans (_ : 1 - (3%:R^-1 + 7%:R^-1) <= _); last first. rewrite lerD2l lerN2. rewrite lerD // lef_pV2 ?qualifE/= ?gt0CG ?ltr0n ?ler_nat //. have notStype5: FTtype S != 5%N by rewrite (eqP Stype2). have frobUW2 := Ptype_compl_Frobenius maxS StypeP notStype5. apply: leq_ltn_trans (ltn_odd_Frobenius_ker frobUW2 (mFT_odd _)). by rewrite (leq_double 3). apply: le_trans (_ : 2%:R^-1 <= _); last by rewrite -!CratrE; compute. rewrite mulrAC ler_pdivrMr 1?gt0CG // ler_pdivlMl ?ltr0n //. rewrite -!natrM ler_nat mulnA -(Lagrange (normal_sub nsM''M')) mulnC leq_mul //. by rewrite subset_leq_card //; have [_ _ _ []] := MtypeP. by rewrite -card_quotient ?normal_norm // mulnC -(prednK (cardG_gt0 _)) leqW. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum algC classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9)