proposition: Lemma RS_repair_is_correct : n.-primitive_root a -> t.-BDD (RS.code a n d, RS_repair a n.-1 d).
proof: Proof. move=> an; rewrite /BD_decoding /=. move=> c e. set y := c + e. set r0 : {poly F} := 'X^d. set r1 := \RSsynp_(rVexp a n, y, d). set vj := Euclid.v r0 r1 (stop (odd d + t) r0 r1). set rj := Euclid.r r0 r1 (stop (odd d + t) r0 r1). move=> Hc et. set r_ : {poly F} := \RSomega_(rVexp a n, e). rewrite /= /RS_repair. have same_syndrome : \RSsynp_(rVexp a n, y, d) = \RSsynp_(rVexp a n, e, d). rewrite syndromepD. move: Hc => /=. rewrite mem_kernel_syndrome0 -RS.codebook_syndrome //. rewrite -RS.RS_syndromep_codeword // => /eqP ->; by rewrite add0r. rewrite ffunE. case: ifPn => syndrome0. suff e0 : e = 0 by rewrite /y e0 addr0. suff yc : y = c. move/eqP : yc; by rewrite -subr_eq0 /y addrAC subrr add0r => /eqP. apply/eqP/negPn/negP => abs. suff : dH y c < min_dist (RS_not_trivial a dn). apply/negP; rewrite -leqNgt min_dist_prop //. move: syndrome0; by rewrite RS.RS_syndromep_codeword // -RS.lcode0_codebook // inE. rewrite (RS_min_dist dn _ an) // dH_sym dH_wH (@leq_ltn_trans t) //. move: (td d). rewrite /RS.errors_ub ltnS => /leq_trans; apply. by rewrite -{2}(half_bit_double d true) add1n half_leq // ltnS -addnn leq_addr. have H1 : distinct_non_zero (rVexp a n). apply distinct_non_zero_rVexp. by apply (primitive_uroot_neq0 an). by move/prim_root_not_uroot_on: an. have H2 := rVexp_neq0 _ (primitive_uroot_neq0 an). have r1_neq0 : \RSsynp_(rVexp a n, e, d) != 0. apply: contra syndrome0. rewrite syndromepD => /eqP ->. by rewrite addr0 RS.RS_syndromep_codeword // -RS.lcode0_codebook // inE. have K1 : size r1 <= size ('X^d : {poly F}). by rewrite /r1 size_polyXn (leq_trans (size_syndromep _ _ _)). have K2 : \RSsynp_(rVexp a n, y, d) != 0 by rewrite same_syndrome. have K3 : \sigma_(rVexp a n, e) * r1 = r_ + - RS_mod a e d * 'X^d. by rewrite /r1 same_syndrome RS_key_equation. have K4 : size \sigma_(rVexp a n, e) <= t.+1. rewrite (leq_trans (size_errloc _ _)) => //; by rewrite -wH_card_supp. have K5 : size r_ <= odd d + t. rewrite wH_card_supp in et. by rewrite (leq_trans (size_erreval (rVexp a n) (Errvec et) _)) // leq_addl. have K6 : (t.+1 + (odd d + t))%N = size ('X^d : {poly F}). rewrite size_polyXn addnCA addSn addnn addnS; congr S. by rewrite -[RHS](odd_double_half d). move: (@solve_key_equation_coprimep F 'X^d r1 K1 \sigma_(rVexp a n, e) r_ _ (errloc_neq0 (rVexp a n) (supp e)) K2 t.+1 _ K3 K4 K5 K6 (coprime_errloc_erreval H1 (@H2 n) _)). case=> l [l0 [Hvj Hrj]]. by rewrite -(@RS_err_is_correct _ _ _ _ (primitive_uroot_neq0 an) l e) // /y addrK ifT // RS.RS_syndromep_codeword // -RS.lcode0_codebook // inE. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code