proposition: Proposition rank_eigenspaces_quasi_homocyclic : exists2 n, `|q - h * n| = 1%N & exists i : 'I_h, [/\ `|'n_i - n| = 1%N, (q < h * n) = ('n_i < n) & forall j, j != i -> 'n_j = n].
proof: Proof. have [defV dxV] := mxdirect_sum_eigenspace_cycle. have sum_n: (\sum_(i < h) 'n_i)%N = q by rewrite -(mxdirectP dxV) defV mxrank1. suffices [n [i]]: exists n : nat, exists2 i : 'I_h, `|'n_i - n| == 1%N & forall i', i' != i -> 'n_i' = n. - move/eqP=> n_i n_i'; rewrite -{1 5}(prednK h_gt0). rewrite -sum_n (bigD1 i) //= (eq_bigr _ n_i') sum_nat_const cardC1 card_ord. by exists n; last exists i; rewrite ?distnDr ?ltn_add2r. case: (leqP h 1) sum_n {defV dxV} => [|h_gt1 _]. rewrite leq_eqVlt ltnNge h_gt0 orbF; move/eqP->; rewrite big_ord1 => n_0. by exists q', 0 => [|i']; rewrite ?(ord1 i') // n_0 distSn. pose dn1 i := `|'n_i - 'n_(i + 1)|. have sum_dn1: (\sum_(0 <= i < h) dn1 i ^ 2 == 2)%N. rewrite big_mkord -(eqn_add2l (2 * \rank 'E_1)) -diff_rank_quasi_cent_cycle. by rewrite -mulnSr -rankEm ?modn_small. pose diff_n := [seq i <- index_iota 0 h | dn1 i != 0%N]. have diff_n_1: all (fun i => dn1 i == 1%N) diff_n. apply: contraLR sum_dn1; case/allPn=> i; rewrite mem_filter. case def_i: (dn1 i) => [|[|ni]] //=; case/splitPr=> e e' _. by rewrite big_cat big_cons /= addnCA def_i -add2n sqrnD. have: sorted ltn diff_n. by rewrite (sorted_filter ltn_trans) // /index_iota subn0 iota_ltn_sorted. have: all (ltn^~ h) diff_n. by apply/allP=> i; rewrite mem_filter mem_index_iota; case/andP. have: size diff_n = 2%N. move: diff_n_1; rewrite size_filter -(eqnP sum_dn1) /diff_n. elim: (index_iota 0 h) => [|i e IHe]; rewrite (big_nil, big_cons) //=. by case def_i: (dn1 i) => [|[]] //=; rewrite def_i //; move/IHe->. case def_jk: diff_n diff_n_1 => [|j [|k []]] //=; case/and3P=> dn1j dn1k _ _. case/and3P=> lt_jh lt_kh _ /andP[lt_jk _]. have def_n i: i <= h -> 'n_i = if i <= j then 'n_0 else if i <= k then 'n_j.+1 else 'n_k.+1. - elim: i => // i IHi lt_ik; have:= IHi (ltnW lt_ik); rewrite !(leq_eqVlt i). have:= erefl (i \in diff_n); rewrite {2}def_jk !inE mem_filter mem_index_iota. case: (i =P j) => [-> _ _ | _]; first by rewrite ltnn lt_jk. case: (i =P k) => [-> _ _ | _]; first by rewrite ltnNge ltnW // ltnn. by rewrite distn_eq0 lt_ik addn1; case: eqP => [->|]. have n_j1: 'n_j.+1 = 'n_k by rewrite (def_n k (ltnW lt_kh)) leqnn leqNgt lt_jk. have n_k1: 'n_k.+1 = 'n_0. rewrite -(rank_step_eigenspace_cycle 0) (def_n h (leqnn h)). by rewrite leqNgt lt_jh leqNgt lt_kh; split. case: (leqP k j.+1) => [ | lt_j1_k]. rewrite leq_eqVlt ltnNge lt_jk orbF; move/eqP=> def_k. exists 'n_(k + 1); exists (Ordinal lt_kh) => [|i' ne_i'k]; first exact: dn1k. rewrite addn1 {1}(def_n _ (ltnW (valP i'))) n_k1. by rewrite -ltnS -def_k ltn_neqAle ne_i'k /=; case: leqP; split. case: (leqP h.-1 (k - j)) => [le_h1_kj | lt_kj_h1]. have k_h1: k = h.-1. apply/eqP; rewrite eqn_leq -ltnS (prednK h_gt0) lt_kh. exact: leq_trans (leq_subr j k). have j0: j = 0%N. apply/eqP; rewrite -leqn0 -(leq_add2l k) -{2}(subnK (ltnW lt_jk)). by rewrite addn0 leq_add2r {1}k_h1. exists 'n_(j + 1); exists (Ordinal lt_jh) => [|i' ne_i'j]; first exact: dn1j. rewrite addn1 {1}(def_n _ (ltnW (valP i'))) j0 leqNgt lt0n -j0. by rewrite ne_i'j -ltnS k_h1 (prednK h_gt0) (valP i'); split. suffices: \sum_(i < h) `|'n_i - 'n_(i + 2)| ^ 2 > 2. rewrite -(ltn_add2l (2 * \rank 'E_2)) -diff_rank_quasi_cent_cycle. rewrite -mulnSr -rankEm ?ltnn ?modn_small //. by rewrite -(prednK h_gt0) ltnS (leq_trans _ lt_kj_h1) // ltnS subn_gt0. have lt_k1h: k.-1 < h by rewrite ltnW // (ltn_predK lt_jk). rewrite (bigD1 (Ordinal lt_jh)) // (bigD1 (Ordinal lt_k1h)) /=; last first. by rewrite -val_eqE neq_ltn /= orbC -subn1 ltn_subRL lt_j1_k. rewrite (bigD1 (Ordinal lt_kh)) /=; last first. by rewrite -!val_eqE !neq_ltn /= lt_jk (ltn_predK lt_jk) leqnn !orbT. rewrite !addnA ltn_addr // !addn2 (ltn_predK lt_jk) n_k1. rewrite (def_n j (ltnW lt_jh)) leqnn (def_n _ (ltn_trans lt_j1_k lt_kh)). rewrite lt_j1_k -if_neg -leqNgt leqnSn n_j1. rewrite (def_n _ (ltnW lt_k1h)) leq_pred -if_neg -ltnNge. rewrite -subn1 ltn_subRL lt_j1_k n_j1. suffices ->: 'n_k.+2 = 'n_k.+1. by rewrite distnC -n_k1 -(addn1 k) -/(dn1 k) (eqP dn1k). case: (leqP k.+2 h) => [le_k2h | ]. by rewrite (def_n _ le_k2h) (leqNgt _ k) leqnSn n_k1 if_same. rewrite ltnS leq_eqVlt ltnNge lt_kh orbF; move/eqP=> def_h. rewrite -{1}def_h -add1n rank_step_eigenspace_cycle (def_n _ h_gt0). rewrite -(subSn (ltnW lt_jk)) def_h leq_subLR in lt_kj_h1. by rewrite -(leq_add2r k) lt_kj_h1 n_k1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gfunctor commutator gproduct) mathcomp(ssralg finalg zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)