(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section ‹Correctness of the LLL factorization algorithm› text ‹This theory connects short vectors of lattices and factors of polynomials. From this connection, we derive soundness of the lattice based factorization algorithm. › theory LLL_Factorization imports LLL_Factorization_Impl Berlekamp_Zassenhaus.Factorize_Int_Poly begin subsection ‹Basic facts about the auxiliary functions› hide_const (open) module.smult lemma nth_factorization_lattice: fixes u and d defines "n ≡ degree u" assumes "i < n + d" shows "factorization_lattice u d m ! i = vec_of_poly_n (if i < d then u * monom 1 (d - Suc i) else monom m (n+d-Suc i)) (n+d)" using assms by (unfold factorization_lattice_def, auto simp: nth_append smult_monom Let_def not_less) lemma length_factorization_lattice[simp]: shows "length (factorization_lattice u d m) = degree u + d" by (auto simp: factorization_lattice_def Let_def) lemma dim_factorization_lattice: assumes "x < degree u + d" shows "dim_vec (factorization_lattice u d m ! x) = degree u + d" unfolding factorization_lattice_def using assms nth_append by (simp add: nth_append Let_def) lemma dim_factorization_lattice_element: assumes "x ∈ set (factorization_lattice u d m)" shows "dim_vec x = degree u + d" using assms by (auto simp: factorization_lattice_def Let_def) lemma set_factorization_lattice_in_carrier[simp]: "set (factorization_lattice u d m) ⊆ carrier_vec (degree u + d)" using dim_factorization_lattice by (auto simp: factorization_lattice_def Let_def) lemma choose_u_Cons: "choose_u (x#xs) = (if xs = [] then x else min_degree_poly x (choose_u xs))" by (cases xs, auto) lemma choose_u_member: "xs ≠ [] ⟹ choose_u xs ∈ set xs" by (induct xs, auto simp: choose_u_Cons) declare choose_u.simps[simp del] subsection ‹Facts about Sylvester matrices and norms› lemma (in LLL) lattice_is_span [simp]: "lattice_of xs = span_list xs" by (unfold lattice_of_def span_list_def lincomb_list_def image_def, auto) lemma sq_norm_row_sylvester_mat1: fixes f g :: "'a :: conjugatable_ring poly" assumes i: "i < degree g" shows "∥(row (sylvester_mat f g) i)∥⇧^{2}= ∥f∥⇧^{2}" proof (cases "f = 0") case True thus ?thesis by (auto simp add: sylvester_mat_def row_def sq_norm_vec_def o_def interv_sum_list_conv_sum_set_nat i intro!: sum_list_zero) next case False note f = False let ?f = "λj. if i ≤ j ∧ j - i ≤ degree f then coeff f (degree f + i - j) else 0" let ?h = "λj. j + i" let ?row = "vec (degree f + degree g) ?f " let ?g = "λj. degree f - j" have image_g: "?g ` {0..<Suc (degree f)} = {0..<Suc (degree f)}" by (auto simp add: image_def) (metis (no_types, hide_lams) Nat.add_diff_assoc add.commute add_diff_cancel_left' atLeastLessThan_iff diff_Suc_Suc diff_Suc_less less_Suc_eq_le zero_le) have bij_h: "bij_betw ?h {0..<Suc (degree f)} {i..< Suc (degree f + i)}" unfolding bij_betw_def image_def by (auto, metis atLeastLessThan_iff le_add_diff_inverse2 less_diff_conv linorder_not_less not_less_eq zero_order(3)) have "∥row (sylvester_mat f g) i∥⇧^{2}= ∥?row∥⇧^{2}" by (rule arg_cong[of _ _ "sq_norm_vec"], insert i, auto simp add: row_def sylvester_mat_def sylvester_mat_sub_def) also have "... = sum_list (map (sq_norm ∘ ?f) [0..<degree f + degree g])" unfolding sq_norm_vec_def by auto also have "... = sum (sq_norm ∘ ?f) {0..<degree f + degree g}" unfolding interv_sum_list_conv_sum_set_nat by auto also have "... = sum (sq_norm ∘ ?f) {i..< Suc (degree f + i)}" by (rule sum.mono_neutral_right, insert i, auto) also have "... = sum ((sq_norm ∘ ?f) ∘ ?h) {0..<Suc (degree f)}" by (unfold o_def, rule sum.reindex_bij_betw[symmetric, OF bij_h]) also have "... = sum (λj. sq_norm (coeff f (degree f - j))) {0..<Suc (degree f)}" by (rule sum.cong, auto) also have "... = sum ((λj. sq_norm (coeff f j)) ∘ ?g) {0..<Suc (degree f)}" unfolding o_def .. also have "... = sum (λj. sq_norm (coeff f j)) (?g ` {0..<Suc (degree f)})" by (rule sum.reindex[symmetric], auto simp add: inj_on_def) also have "... = sum (sq_norm ∘ coeff f) {0..<Suc (degree f)}" unfolding image_g by simp also have "... = sum_list (map sq_norm (coeffs f))" unfolding coeffs_def using f by (simp add: interv_sum_list_conv_sum_set_nat) finally show ?thesis unfolding sq_norm_poly_def by auto qed lemma sq_norm_row_sylvester_mat2: fixes f g :: "'a :: conjugatable_ring poly" assumes i1: "degree g ≤ i" and i2: "i < degree f + degree g" shows "∥row (sylvester_mat f g) i∥⇧^{2}= ∥g∥⇧^{2}" proof - let ?f = "λj. if i - degree g ≤ j ∧ j ≤ i then coeff g (i - j) else 0" let ?row = "vec (degree f + degree g) ?f" let ?h = "λj. j + i - degree g" let ?g = "λj. degree g - j" have image_g: "?g ` {0..<Suc (degree g)} = {0..<Suc (degree g)}" by (auto simp add: image_def) (metis atLeastLessThan_iff diff_diff_cancel diff_le_self less_Suc_eq_le zero_le) have x: "x - (i - degree g) ≤ degree g" if x: "x < Suc i" for x using x by auto have bij_h: "bij_betw ?h {0..<Suc (degree g)} {i - degree g..<Suc i}" unfolding bij_betw_def inj_on_def using i1 i2 unfolding image_def by (auto, metis (no_types) Nat.add_diff_assoc atLeastLessThan_iff x less_Suc_eq_le less_eq_nat.simps(1) ordered_cancel_comm_monoid_diff_class.diff_add) have "∥row (sylvester_mat f g) i∥⇧^{2}= ∥?row∥⇧^{2}" by (rule arg_cong[of _ _ "sq_norm_vec"], insert i1 i2, auto simp add: row_def sylvester_mat_def sylvester_mat_sub_def) also have "... = sum_list (map (sq_norm ∘ ?f) [0..<degree f + degree g])" unfolding sq_norm_vec_def by auto also have "... = sum (sq_norm ∘ ?f) {0..<degree f + degree g}" unfolding interv_sum_list_conv_sum_set_nat by auto also have "... = sum (sq_norm ∘ ?f) {i - degree g..< Suc i}" by (rule sum.mono_neutral_right, insert i2, auto) also have "... = sum ((sq_norm ∘ ?f) ∘ ?h) {0..<Suc (degree g)}" by (unfold o_def, rule sum.reindex_bij_betw[symmetric, OF bij_h]) also have "... = sum (λj. sq_norm (coeff g (degree g - j))) {0..<Suc (degree g)}" by (rule sum.cong, insert i1, auto) also have "... = sum ((λj. sq_norm (coeff g j)) ∘ ?g) {0..<Suc (degree g)}" unfolding o_def .. also have "... = sum (λj. sq_norm (coeff g j)) (?g ` {0..<Suc (degree g)})" by (rule sum.reindex[symmetric], auto simp add: inj_on_def) also have "... = sum (sq_norm ∘ coeff g) {0..<Suc (degree g)}" unfolding image_g by simp also have "... = sum_list (map sq_norm (coeffs g))" unfolding coeffs_def by (simp add: interv_sum_list_conv_sum_set_nat) finally show ?thesis unfolding sq_norm_poly_def by auto qed lemma Hadamard's_inequality_int: fixes A::"int mat" assumes A: "A ∈ carrier_mat n n" shows "¦det A¦ ≤ sqrt (of_int (prod_list (map sq_norm (rows A))))" proof - let ?A = "map_mat real_of_int A" have "¦det A¦ = ¦det ?A¦" unfolding of_int_hom.hom_det by simp also have "… ≤ sqrt (prod_list (map sq_norm (rows ?A)))" by (rule Hadamard's_inequality[of ?A n], insert A, auto) also have "… = sqrt (of_int (prod_list (map sq_norm (rows A))))" unfolding of_int_hom.hom_prod_list map_map by (rule arg_cong[of _ _ "λ x. sqrt (prod_list x)"], rule nth_equalityI, force, auto simp: sq_norm_of_int[symmetric] row_def intro!: arg_cong[of _ _ sq_norm_vec]) finally show ?thesis . qed lemma resultant_le_prod_sq_norm: fixes f g::"int poly" defines "n ≡ degree f" and "k ≡ degree g" shows "¦resultant f g¦ ≤ sqrt (of_int (∥f∥⇧^{2}^k * ∥g∥⇧^{2}^n))" proof - let ?S = "sylvester_mat f g" let ?f = "sq_norm ∘ row ?S" have map_rw1: "map ?f [0..<degree g] = replicate k ∥f∥⇧^{2}" proof (rule nth_equalityI) let ?M = "map (sq_norm ∘ row (sylvester_mat f g)) [0..<degree g]" show "length ?M = length (replicate k ∥f∥⇧^{2})" using k_def by auto show "?M ! i = replicate k ∥f∥⇧^{2}! i" if i: "i < length ?M" for i proof - have ik: "i<k" using i k_def by auto hence i_deg_g: "i < degree g" using k_def by auto have "replicate k ∥f∥⇧^{2}! i = ∥f∥⇧^{2}" by (rule nth_replicate[OF ik]) also have "... = (sq_norm ∘ row (sylvester_mat f g)) (0 + i)" using sq_norm_row_sylvester_mat1 ik k_def by force also have "... = ?M ! i" by (rule nth_map_upt[symmetric], simp add: i_deg_g) finally show "?M ! i = replicate k ∥f∥⇧^{2}! i" .. qed qed have map_rw2: "map ?f [degree g..<degree f + degree g] = replicate n ∥g∥⇧^{2}" proof (rule nth_equalityI) let ?M = "map (sq_norm ∘ row (sylvester_mat f g)) [degree g..<degree f + degree g]" show "length ?M = length (replicate n ∥g∥⇧^{2})" by (simp add: n_def) show "?M ! i = replicate n ∥g∥⇧^{2}! i" if "i<length ?M" for i proof - have i_n: "i<n" using n_def that by auto hence i_deg_f: "i < degree f" using n_def by auto have "replicate n ∥g∥⇧^{2}! i = ∥g∥⇧^{2}" by (rule nth_replicate[OF i_n]) also have "... = (sq_norm ∘ row (sylvester_mat f g)) (degree g + i)" using i_n n_def by (simp add: sq_norm_row_sylvester_mat2) also have "... = ?M ! i" by (simp add: i_deg_f) finally show "?M ! i = replicate n ∥g∥⇧^{2}! i" .. qed qed have p1: "prod_list (map ?f [0..<degree g]) = ∥f∥⇧^{2}^k" unfolding map_rw1 by (rule prod_list_replicate) have p2: "prod_list (map ?f [degree g..<degree f + degree g]) = ∥g∥⇧^{2}^n" unfolding map_rw2 by (rule prod_list_replicate) have list_rw: "[0..<degree f + degree g] = [0..<degree g] @ [degree g..<degree f + degree g]" by (metis add.commute upt_add_eq_append zero_le) have "¦resultant f g¦ = ¦det ?S¦" unfolding resultant_def .. also have "... ≤ sqrt (of_int (prod_list (map sq_norm (rows ?S))))" by (rule Hadamard's_inequality_int, auto) also have "map sq_norm (rows ?S) = map ?f [0..<degree f + degree g]" unfolding Matrix.rows_def by auto also have "... = map ?f ([0..<degree g] @ [degree g..<degree f + degree g])" by (simp add: list_rw) also have "prod_list ... = prod_list (map ?f [0..<degree g]) * prod_list (map ?f [degree g..<degree f + degree g])" by auto finally show ?thesis unfolding p1 p2 . qed subsection ‹Proof of the key lemma 16.20› (* Lemma 16.20 *) lemma common_factor_via_short: fixes f g u :: "int poly" defines "n ≡ degree f" and "k ≡ degree g" assumes n0: "n > 0" and k0: "k > 0" and monic: "monic u" and deg_u: "degree u > 0" and uf: "poly_mod.dvdm m u f" and ug: "poly_mod.dvdm m u g" and short: "∥f∥⇧^{2}^k * ∥g∥⇧^{2}^n < m⇧^{2}" and m: "m ≥ 0" shows "degree (gcd f g) > 0" proof - interpret poly_mod m . have f_not0: "f ≠ 0" and g_not0: "g ≠ 0" using n0 k0 k_def n_def by auto have deg_f: "degree f > 0" using n0 n_def by simp have deg_g: "degree g > 0" using k0 k_def by simp obtain s t where deg_s: "degree s < degree g" and deg_t: "degree t < degree f" and res_eq: "[:resultant f g:] = s * f + t * g" and s_not0: "s ≠ 0" and t_not0: "t ≠ 0" using resultant_as_nonzero_poly[OF deg_f deg_g] by auto have res_eq_modulo: "[:resultant f g:] =m s * f + t * g" using res_eq by simp have u_dvdm_res: "u dvdm [:resultant f g:]" proof (unfold res_eq, rule dvdm_add) show "u dvdm s * f" using dvdm_factor[OF uf, of s] unfolding mult.commute[of f s] by auto show "u dvdm t * g" using dvdm_factor[OF ug, of t] unfolding mult.commute[of g t] by auto qed have res_0_mod: "resultant f g mod m = 0" by (rule monic_dvdm_constant[OF u_dvdm_res monic deg_u]) have res0: "resultant f g = 0" proof (rule mod_0_abs_less_imp_0) show "[resultant f g = 0] (mod m)" using res_0_mod unfolding cong_def by auto have "¦resultant f g¦ ≤ sqrt ((sq_norm_poly f)^k * (sq_norm_poly g)^n)" unfolding k_def n_def by (rule resultant_le_prod_sq_norm) also have "... < m" proof (rule real_less_lsqrt) show "0 ≤ real_of_int (∥f∥⇧^{2}^ k * ∥g∥⇧^{2}^ n)" by (simp add: sq_norm_poly_ge_0) show "0 ≤ real_of_int m" using m by simp show "real_of_int (∥f∥⇧^{2}^ k * ∥g∥⇧^{2}^ n) < (real_of_int m)⇧^{2}" by (metis of_int_less_iff of_int_power short) qed finally show "¦resultant f g¦ < m" using of_int_less_iff by blast qed have "¬ coprime f g" by (rule resultant_zero_imp_common_factor, auto simp add: deg_f res0) thus ?thesis using res0 resultant_0_gcd by auto qed subsection ‹Properties of the computed lattice and its connection with Sylvester matrices› lemma factorization_lattice_as_sylvester: fixes p :: "'a :: semidom poly" assumes dj: "d ≤ j" and d: "degree p = d" shows "mat_of_rows j (factorization_lattice p (j-d) m) = sylvester_mat_sub d (j-d) p [:m:]" proof (cases "p=0") case True have deg_p: "d = 0" using True d by simp show ?thesis by (auto simp add: factorization_lattice_def True deg_p mat_of_rows_def d) next case p0: False note 1 = degree_mult_eq[OF p0, of "monom _ _", unfolded monom_eq_0_iff, OF one_neq_zero] from dj show ?thesis apply (cases "m = 0") apply (auto simp: mat_eq_iff d[symmetric] 1 coeff_mult_monom sylvester_mat_sub_index mat_of_rows_index nth_factorization_lattice vec_index_of_poly_n degree_monom_eq coeff_const) done qed context inj_comm_semiring_hom begin lemma map_poly_hom_mult_monom [hom_distribs]: "map_poly hom (p * monom a n) = map_poly hom p * monom (hom a) n" by (auto intro!: poly_eqI simp:coeff_mult_monom hom_mult) lemma hom_vec_of_poly_n [hom_distribs]: "map_vec hom (vec_of_poly_n p n) = vec_of_poly_n (map_poly hom p) n" by (auto simp: vec_index_of_poly_n) lemma hom_factorization_lattice [hom_distribs]: shows "map (map_vec hom) (factorization_lattice u k m) = factorization_lattice (map_poly hom u) k (hom m)" by (auto intro!:arg_cong[of _ _ "λp. vec_of_poly_n p _"] simp: list_eq_iff_nth_eq nth_factorization_lattice hom_vec_of_poly_n map_poly_hom_mult_monom) end subsection ‹Proving that @{const factorization_lattice} returns a basis of the lattice› context LLL begin sublocale idom_vec n "TYPE(int)". (*In this context, "n" is fixed by the locale and corresponds to "j" in the book*) lemma upper_triangular_factorization_lattice: fixes u :: "'a :: semidom poly" and d :: nat assumes d: "d ≤ n" and du: "d = degree u" shows "upper_triangular (mat_of_rows n (factorization_lattice u (n-d) k))" (is "upper_triangular ?M") proof (intro upper_triangularI, unfold mat_of_rows_carrier length_factorization_lattice) fix i j assume ji: "j < i" and i: "i < degree u + (n - d)" with d du have jn: "j < n" by auto show "?M $$ (i,j) = 0" proof (cases "u=0") case True with ji i show ?thesis by (auto simp: factorization_lattice_def mat_of_rows_def) next case False then show ?thesis using d ji i apply (simp add: du mat_of_rows_index nth_factorization_lattice) apply (auto simp: vec_index_of_poly_n[OF jn] degree_mult_eq degree_monom_eq) done qed qed lemma factorization_lattice_diag_nonzero: fixes u :: "'a :: semidom poly" and d assumes d: "d=degree u" and dn: "d≤n" and u: "u≠0" and m0: "k≠0" and i: "i<n" shows "(factorization_lattice u (n-d) k) ! i $ i ≠ 0" proof- have 1: "monom (1::'a) (n - Suc (degree u + i)) ≠ 0" using m0 by auto have 2: "i < degree u + (n - d)" using i d by auto let ?p = "u * monom 1 (n - Suc (degree u + i))" have 3: "i < n - degree u ⟹ degree (?p) = n - Suc i" using assms by (auto simp: degree_mult_eq[OF _ 1] degree_monom_eq) show ?thesis apply (unfold nth_factorization_lattice[OF 2] vec_index_of_poly_n[OF 2]) using assms leading_coeff_0_iff[of ?p] apply (cases "i < n - degree u", auto simp: d 3 degree_monom_eq) done qed corollary factorization_lattice_diag_nonzero_RAT: fixes d assumes "d=degree u" and "d≤n" and "u≠0" and "k≠0" and "i<n" shows "RAT (factorization_lattice u (n-d) k) ! i $ i ≠ 0" using factorization_lattice_diag_nonzero[OF assms] assms by (auto simp: nth_factorization_lattice) sublocale gs: vec_space "TYPE(rat)" n. lemma lin_indpt_list_factorization_lattice: fixes d assumes d: "d = degree u" and dn: "d ≤ n" and u: "u ≠ 0" and k: "k ≠ 0" shows "gs.lin_indpt_list (RAT (factorization_lattice u (n-d) k))" (is "gs.lin_indpt_list (RAT ?vs)") proof- have 1: "rows (mat_of_rows n (map (map_vec rat_of_int) ?vs)) = map (map_vec rat_of_int) ?vs" using dn d by (subst rows_mat_of_rows, auto dest!: subsetD[OF set_factorization_lattice_in_carrier]) note 2 = factorization_lattice_diag_nonzero_RAT[OF d dn u k] show ?thesis apply (intro gs.upper_triangular_imp_lin_indpt_list[of "mat_of_rows n (RAT ?vs)", unfolded 1]) using assms 2 by (auto simp: diag_mat_def mat_of_rows_index hom_distribs intro!:upper_triangular_factorization_lattice) qed end subsection ‹Being in the lattice is being a multiple modulo› lemma (in semiring_hom) hom_poly_of_vec: "map_poly hom (poly_of_vec v) = poly_of_vec (map_vec hom v)" by (auto simp add: coeff_poly_of_vec poly_eq_iff) abbreviation "of_int_vec ≡ map_vec of_int" context LLL begin lemma lincomb_to_dvd_modulo: fixes u d defines "d ≡ degree u" assumes d: "d ≤ n" and lincomb: "lincomb_list c (factorization_lattice u (n-d) k) = g" (is "?l = ?r") shows "poly_mod.dvdm k u (poly_of_vec g)" proof- let ?S = "sylvester_mat_sub d (n - d) u [:k:]" define q where "q ≡ poly_of_vec (vec_first (vec n c) (n - d))" define r where "r ≡ poly_of_vec (vec_last (vec n c) d)" have "?l = ?S⇧^{T}*⇩_{v}vec n c" apply (subst lincomb_list_as_mat_mult) using d d_def apply (force simp:factorization_lattice_def) apply (fold transpose_mat_of_rows) using d d_def by (simp add: factorization_lattice_as_sylvester) also have "poly_of_vec … = q * u + smult k r" apply (subst sylvester_sub_poly) using d_def d q_def r_def by auto finally have "… = poly_of_vec g" unfolding lincomb of_int_hom.hom_poly_of_vec by auto then have "poly_of_vec g = q * u + Polynomial.smult k r" by auto then have "poly_mod.Mp k (poly_of_vec g) = poly_mod.Mp k (q * u + Polynomial.smult k r)" by auto also have "... = poly_mod.Mp k (q * u + poly_mod.Mp k (Polynomial.smult k r))" using poly_mod.plus_Mp(2) by auto also have "... = poly_mod.Mp k (q * u)" using poly_mod.plus_Mp(2) unfolding poly_mod.Mp_smult_m_0 by simp also have "... = poly_mod.Mp k (u * q)" by (simp add: mult.commute) finally show ?thesis unfolding poly_mod.dvdm_def by auto qed (* There is a typo in the textbook (page 476). The book states q' = q'' * u + r'' and the correct fact is r' = q'' * u+r'' *) lemma dvd_modulo_to_lincomb: fixes u :: "int poly" and d defines "d ≡ degree u" assumes d: "d < n" and dvd: "poly_mod.dvdm k u (poly_of_vec g)" and k_not0: "k≠0" and monic_u: "monic u" and dim_g: "dim_vec g = n" and deg_u: "degree u > 0" shows "∃c. lincomb_list c (factorization_lattice u (n-d) k) = g" proof - interpret p: poly_mod k . have u_not0: "u ≠ 0" using monic_u by auto hence n[simp]: "0 < n" using d by auto obtain q' r' where g: "poly_of_vec g = q' * u + smult k r'" using p.dvdm_imp_div_mod[OF dvd] by auto obtain q'' r'' where r': "r' = q'' * u + r''" and deg_r'': "degree r''<degree u" using monic_imp_div_mod_int_poly_degree2[OF monic_u deg_u, of r'] by auto (*The following fact is explained in the paragraph below equation (6) in page 476 of the textbook*) have g1: "poly_of_vec g = (q' + smult k q'') * u + smult k r''" unfolding g r' by (metis (no_types, lifting) combine_common_factor mult_smult_left smult_add_right) define q where q: "q = (q' + smult k q'')" define r where r: "r = r''" have degree_q: "q = 0 ∨ degree (q' + smult k q'') < n - d" proof (cases "q = 0",auto, rule degree_div_mod_smult[OF _ _ _ g1]) show "degree (poly_of_vec g) < n" by (rule degree_poly_of_vec_less, auto simp add: dim_g) show "degree r'' < d" using deg_r'' unfolding d_def . assume "q≠0" thus "q' + smult k q'' ≠ 0" unfolding q . show "k ≠ 0" by fact show "degree u = d" using d_def by auto qed have g2: "(vec_of_poly_n (q*u) n) + (vec_of_poly_n (smult k r) n) = g" proof - have "g = vec_of_poly_n (poly_of_vec g) n" by (rule vec_of_poly_n_poly_of_vec[symmetric], auto simp add: dim_g) also have "… = vec_of_poly_n ((q' + smult k q'') * u + smult k r'') n" using g1 by auto also have "... = vec_of_poly_n (q * u + smult k r'') n" unfolding q by auto also have "... = vec_of_poly_n (q * u) n + vec_of_poly_n (smult k r'') n" by (rule vec_of_poly_n_add) finally show ?thesis unfolding r by simp qed let ?c = "λi. if i < n - d then coeff q (n - d - 1 - i) else coeff r (n - Suc i)" let ?c1 = "λi. ?c i ⋅⇩_{v}factorization_lattice u (n-d) k ! i" show ?thesis proof (rule exI[of _ ?c]) let ?part1 = "map (λi. vec_of_poly_n (u * monom 1 i) n) [n-d>..0]" let ?part2 = "map (λi. vec_of_poly_n (monom k i) n) [d>..0]" have [simp]: "dim_vec (M.sumlist (map ?c1 [0..<n - d])) = n" by (rule dim_sumlist, auto simp add: dim_factorization_lattice d_def) have [simp]: "dim_vec (M.sumlist (map ?c1 [n-d..<n])) = n" by (rule dim_sumlist, insert d, auto simp add: dim_factorization_lattice d_def) have [simp]: "factorization_lattice u (n-d) k ! x ∈ carrier_vec n" if x: "x < n" for x using x dim_factorization_lattice_element nth_factorization_lattice[of x u "n-d"] d by (auto simp: d_def) have "[0..<length (factorization_lattice u (n-d) k)] = [0..<n]" using d by (simp add: d_def less_imp_le_nat) also have "... = [0..<n - d] @ [n-d..<n]" by (rule upt_minus_eq_append, auto) finally have list_rw: "[0..<length (factorization_lattice u (n-d) k)] = [0..<n - d] @ [n-d..<n]" . have qu1: "poly_of_vec (M.sumlist (map ?c1 [0..<n - d])) = q*u" proof - have "poly_of_vec (M.sumlist (map ?c1 [0..<n - d])) = poly_of_vec (⨁⇘_{V⇙}i∈{0..<n-d}. ?c1 i)" by (subst sumlist_map_as_finsum, auto) also have "... = poly_of_vec (⨁⇘_{V⇙}i∈set [0..<n-d]. ?c1 i)" by auto also have "... = sum (λi. poly_of_vec (?c1 i)) (set [0..<n-d])" by (auto simp:poly_of_vec_finsum) also have "... = sum (λi. poly_of_vec (?c1 i)) {0..<n-d}" by auto also have "... = q*u" proof - have deg: "degree (u * monom 1 (n - Suc (d + i))) < n" if i: "i < n - d" for i proof - let ?m="monom (1::int) (n - Suc (d + i))" have monom_not0: "?m ≠ 0" using i by auto have deg_m: "degree ?m = n - Suc (d + i)" by (rule degree_monom_eq, auto) have "degree (u * ?m) = d + (n - Suc (d + i))" using degree_mult_eq[OF u_not0 monom_not0] d_def deg_m by auto also have "... < n" using i by auto finally show ?thesis . qed have lattice_rw: "factorization_lattice u (n-d) k ! i = vec_of_poly_n (u * monom 1 (n - Suc (d + i))) n" if i: "i< n - d" for i apply (subst nth_factorization_lattice) using i by (auto simp:d_def) have q_rw: "q = (∑i = 0..<n - d. (smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))" proof (auto simp add: poly_eq_iff coeff_sum) fix j let ?m = "n-d-1-j" let ?f = "λx. coeff q (n - Suc (d + x)) * (if n - Suc (d + x) = j then 1 else 0)" have set_rw: "{0..<n-d} = insert ?m ({0..<n-d} - {?m})" using d by auto have sum0: "(∑x ∈ {0..<n-d} - {?m}. ?f x) = 0" by (rule sum.neutral, auto) have "(∑x = 0..<n - d. ?f x) = (∑x ∈ insert ?m ({0..<n-d} - {?m}). ?f x)" using set_rw by presburger also have "... = ?f ?m + (∑x ∈ {0..<n-d} - {?m}. ?f x)" by (rule sum.insert, auto) also have "... = ?f ?m" unfolding sum0 by auto also have "... = coeff q j" proof (cases "j < n - d") case True then show ?thesis by auto next case False have "j>degree q" using degree_q q False d by auto then show ?thesis using coeff_eq_0 by auto qed finally show "coeff q j = (∑i = 0..<n - d. coeff q (n - Suc (d + i)) * (if n - Suc (d + i) = j then 1 else 0))" .. qed have "sum (λi. poly_of_vec (?c1 i)) {0..<n-d} = (∑i = 0..<n - d. poly_of_vec (coeff q (n - Suc (d + i)) ⋅⇩_{v}factorization_lattice u (n-d) k ! i))" by (rule sum.cong, auto) also have "... = (∑i = 0..<n - d. (poly_of_vec (coeff q (n - Suc (d + i)) ⋅⇩_{v}(vec_of_poly_n (u * monom 1 (n - Suc (d + i))) n))))" by (rule sum.cong, auto simp add: lattice_rw) also have "... = (∑i = 0..<n - d. smult (coeff q (n - Suc (d + i))) (u * monom 1 (n - Suc (d + i))))" by (rule sum.cong, auto simp add: poly_of_vec_scalar_mult[OF deg]) also have "... = (∑i = 0..<n - d. u*(smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))" by auto also have "... = u *(∑i = 0..<n - d. (smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))" by (rule sum_distrib_left[symmetric]) also have "... = u * q" using q_rw by auto also have "... = q*u" by auto finally show ?thesis . qed finally show ?thesis . qed have qu: "M.sumlist (map ?c1 [0..<n - d]) = vec_of_poly_n (q*u) n" proof - have "vec_of_poly_n (q*u) n = vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [0..<n - d]))) n" using qu1 by auto also have "vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [0..<n - d]))) n = M.sumlist (map ?c1 [0..<n - d])" by (rule vec_of_poly_n_poly_of_vec, auto) finally show ?thesis .. qed have rm1: "poly_of_vec (M.sumlist (map ?c1 [n-d..<n])) = smult k r" proof - have "poly_of_vec (M.sumlist (map ?c1 [n-d..<n])) = poly_of_vec (⨁⇘_{V⇙}i∈{n-d..<n}. ?c1 i)" by (subst sumlist_map_as_finsum, auto) also have "... = poly_of_vec (⨁⇘_{V⇙}i∈set [n-d..<n]. ?c1 i)" by auto also have "... = sum (λi. poly_of_vec (?c1 i)) {n-d..<n}" by (auto simp: poly_of_vec_finsum) also have "... = smult k r" proof - have deg: "degree (monom k (n - Suc i)) < n" if i: "n-d≤i" and i2: "i<n" for i using degree_monom_le i i2 by (simp add: degree_monom_eq k_not0) have lattice_rw: "factorization_lattice u (n-d) k ! i = vec_of_poly_n (monom k (n - Suc i)) n" if i: "n - d ≤ i" and i2: "i<n" for i using i2 i d d_def by (subst nth_factorization_lattice, auto) have r_rw: "r = (∑i ∈ {n-d..<n}. (monom (coeff r (n - Suc i)) (n - Suc i)))" proof (auto simp add: poly_eq_iff coeff_sum) fix j show "coeff r j = (∑i = n - d..<n. if n - Suc i = j then coeff r (n - Suc i) else 0)" proof (cases "j<d") case True have j_eq: "n - Suc (n - 1 - j) = j" using d True by auto let ?i = "n-1-j" let ?f ="λi. if n - Suc i = j then coeff r (n - Suc i) else 0" have sum0: "sum ?f ({n-d..<n} - {?i}) = 0" by (rule sum.neutral, auto) have "{n-d..<n} = insert ?i ({n-d..<n} - {?i})" using True by auto hence "sum ?f {n - d..<n} = sum ?f (insert ?i ({n-d..<n} - {?i}))" by auto also have "... = ?f ?i + sum ?f ({n-d..<n} - {?i})" by (rule sum.insert, auto) also have "... = coeff r j" unfolding sum0 j_eq by simp finally show ?thesis .. next case False hence "(∑i = n - d..<n. if n - Suc i = j then coeff r (n - Suc i) else 0) = 0" by (intro sum.neutral ballI, insert False, simp, linarith) also have "... = coeff r j" by (rule coeff_eq_0[symmetric], insert False deg_r'' r d_def, auto) finally show ?thesis .. qed qed have "sum (λi. poly_of_vec (?c1 i)) {n-d..<n} = (∑i ∈ {n-d..<n}. poly_of_vec (coeff r (n - Suc i) ⋅⇩_{v}factorization_lattice u (n-d) k ! i))" by (rule sum.cong, auto) also have "... = (∑i ∈ {n-d..<n}. (poly_of_vec (coeff r (n - Suc i) ⋅⇩_{v}vec_of_poly_n (monom k (n - Suc i)) n)))" by (rule sum.cong, auto simp add: lattice_rw) also have "... = (∑i ∈ {n-d..<n}. smult (coeff r (n - Suc i)) (monom k (n - Suc i)))" by (rule sum.cong, auto simp add: poly_of_vec_scalar_mult[OF deg]) also have "... = (∑i ∈ {n-d..<n}. smult k (monom (coeff r (n - Suc i)) (n - Suc i)))" by (rule sum.cong, auto simp add: smult_monom smult_sum2) also have "... = smult k (∑i ∈ {n-d..<n}. (monom (coeff r (n - Suc i)) (n - Suc i)))" by (simp add: smult_sum2) also have "... = smult k r" using r_rw by auto finally show ?thesis . qed finally show ?thesis . qed have rm: "(M.sumlist (map ?c1 [n-d..<n])) = vec_of_poly_n (smult k r) n" proof - have "vec_of_poly_n (smult k r) n = vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [n-d..<n]))) n" using rm1 by auto also have "vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [n-d..<n]))) n = M.sumlist (map ?c1 [n-d..<n])" by (rule vec_of_poly_n_poly_of_vec, auto) finally show ?thesis .. qed have "lincomb_list ?c (factorization_lattice u (n-d) k) = M.sumlist (map ?c1 ([0..<n - d] @ [n-d..<n]))" unfolding lincomb_list_def list_rw by auto also have "... = M.sumlist (map ?c1 [0..<n - d] @ map ?c1 [n-d..<n])" by auto also have "... = M.sumlist (map ?c1 [0..<n - d]) + M.sumlist (map ?c1 [n-d..<n])" using d by (auto simp add: d_def nth_factorization_lattice intro!: M.sumlist_append) also have "... = vec_of_poly_n (q*u) n + vec_of_poly_n (smult k r) n" unfolding qu rm by auto also have "... = g" using g2 by simp finally show "lincomb_list ?c (factorization_lattice u (n-d) k) = g" . qed qed text ‹The factorization lattice precisely characterises the polynomials of a certain degree which divide $u$ modulo $M$.› lemma factorization_lattice: fixes M assumes deg_u: "degree u ≠ 0" and M: "M ≠ 0" shows "degree u ≤ n ⟹ n ≠ 0 ⟹ f ∈ poly_of_vec ` lattice_of (factorization_lattice u (n - degree u) M) ⟹ degree f < n ∧ poly_mod.dvdm M u f" "monic u ⟹ degree u < n ⟹ degree f < n ⟹ poly_mod.dvdm M u f ⟹ f ∈ poly_of_vec ` lattice_of (factorization_lattice u (n - degree u) M)" proof - from deg_u have deg_u: "degree u > 0" by auto let ?L = "factorization_lattice u (n - degree u) M" { assume deg: "degree f < n" and dvd: "poly_mod.dvdm M u f" and mon: "monic u" and deg_u_lt: "degree u < n" define fv where "fv = vec n (λ i. (coeff f (n - Suc i)))" have f: "f = poly_of_vec fv" unfolding fv_def poly_of_vec_def Let_def using deg by (auto intro!: poly_eqI coeff_eq_0 simp: coeff_sum) have dim_fv: "dim_vec fv = n" unfolding fv_def by simp from dvd_modulo_to_lincomb[OF deg_u_lt _ M mon _ deg_u(1), of fv, folded f, OF dvd dim_fv] obtain c where gv: "fv = lincomb_list c ?L" by auto have "fv ∈ lattice_of ?L" unfolding gv lattice_is_span by (auto simp: in_span_listI) thus "f ∈ poly_of_vec ` lattice_of ?L" unfolding f by auto } moreover { assume "f ∈ poly_of_vec ` lattice_of ?L" and deg_u: "degree u ≤ n" and n: "n ≠ 0" then obtain fv where f: "f = poly_of_vec fv" and fv: "fv ∈ lattice_of ?L" by auto from in_span_listE[OF fv[unfolded lattice_is_span]] obtain c where fv: "fv = lincomb_list c ?L" by auto from lincomb_to_dvd_modulo[OF _ fv[symmetric]] deg_u f have dvd: "poly_mod.dvdm M u f" by auto have "set ?L ⊆ carrier_vec n" unfolding factorization_lattice_def using deg_u by auto hence "fv ∈ carrier_vec n" unfolding fv by (metis lincomb_list_carrier) hence "degree f < n" unfolding f using degree_poly_of_vec_less[of fv n] using n by auto with dvd show "degree f < n ∧ poly_mod.dvdm M u f" by auto } qed end subsection ‹Soundness of the LLL factorization algorithm› lemma LLL_short_polynomial: assumes deg_u_0: "degree u ≠ 0" and deg_le: "degree u ≤ n" and pl1: "pl > 1" and monic: "monic u" shows "degree (LLL_short_polynomial pl n u) < n" and "LLL_short_polynomial pl n u ≠ 0" and "poly_mod.dvdm pl u (LLL_short_polynomial pl n u)" and "degree u < n ⟹ f ≠ 0 ⟹ poly_mod.dvdm pl u f ⟹ degree f < n ⟹ ∥LLL_short_polynomial pl n u∥⇧^{2}≤ 2 ^ (n - 1) * ∥f∥⇧^{2}" proof - interpret poly_mod_2 pl by (unfold_locales, insert pl1, auto) from pl1 have pl0: "pl ≠ 0" by auto let ?d = "degree u" let ?u = "Mp u" let ?iu = "inv_Mp ?u" from Mp_inv_Mp_id[of ?u] have "?iu =m ?u" . also have "… =m u" by simp finally have iu_u: "?iu =m u" by simp have degu[simp]: "degree ?u = degree u" using monic by simp have mon: "monic ?u" using monic by (rule monic_Mp) have "degree ?iu = degree ?u" unfolding inv_Mp_def by (rule degree_map_poly, unfold mon, insert mon pl1, auto simp: inv_M_def) with degu have deg_iu: "degree ?iu = degree u" by simp have mon_iu: "monic ?iu" unfolding deg_iu unfolding inv_Mp_def Mp_def inv_M_def M_def by (insert pl1, auto simp: coeff_map_poly monic) let ?L = "factorization_lattice ?iu (n - ?d) pl" let ?sv = "short_vector_hybrid 2 ?L" from deg_u_0 deg_le have n: "n ≠ 0" by auto from deg_u_0 have u0: "u ≠ 0" by auto have id: "LLL_short_polynomial pl n u = poly_of_vec ?sv" unfolding LLL_short_polynomial_def by blast have id': "∥?sv∥⇧^{2}= ∥LLL_short_polynomial pl n u∥⇧^{2}" unfolding id by simp interpret vec_module "TYPE(int)" n. interpret L: LLL n n "?L" 2 . from deg_le deg_iu have deg_iu_le: "degree ?iu ≤ n" by simp have len: "length ?L = n" unfolding factorization_lattice_def using deg_le deg_iu by auto from deg_u_0 deg_iu have deg_iu0: "degree ?iu ≠ 0" by auto hence iu0: "?iu ≠ 0" by auto from L.lin_indpt_list_factorization_lattice[OF refl deg_iu_le iu0 pl0] have *: "4/3 ≤ (2 :: rat)" "L.gs.lin_indpt_list (L.RAT ?L)" by (auto simp: deg_iu) interpret L: LLL_with_assms n n ?L 2 by (unfold_locales, insert *, auto simp: deg_iu deg_le) note short = L.short_vector_hybrid[OF refl n, unfolded id' L.L_def] from short(2) have mem: "LLL_short_polynomial pl n u ∈ poly_of_vec ` lattice_of ?L" unfolding id by auto note fact = L.factorization_lattice(1)[OF deg_iu0 pl0 deg_iu_le n, unfolded deg_iu, OF mem] show "degree (LLL_short_polynomial pl n u) < n" using fact by auto from fact have "?iu dvdm (LLL_short_polynomial pl n u)" by auto then obtain h where "LLL_short_polynomial pl n u =m ?iu * h" unfolding dvdm_def by auto also have "?iu * h =m Mp ?iu * h" unfolding mult_Mp by simp also have "Mp ?iu * h =m u * h" unfolding iu_u unfolding mult_Mp by simp finally show "u dvdm (LLL_short_polynomial pl n u)" unfolding dvdm_def by auto from short have sv1: "?sv ∈ carrier_vec n" by auto from short have "?sv ≠ 0⇩_{v}j" for j by auto thus "LLL_short_polynomial pl n u ≠ 0" unfolding id by simp assume degu: "degree u < n" and dvd: "u dvdm f" and degf: "degree f < n" and f0: "f ≠ 0" from dvd obtain h where "f =m u * h" unfolding dvdm_def by auto also have "u * h =m Mp u * h" unfolding mult_Mp by simp also have "Mp u * h =m Mp ?iu * h" unfolding iu_u by simp also have "Mp ?iu * h =m ?iu * h" unfolding mult_Mp by simp finally have dvd: "?iu dvdm f" unfolding dvdm_def by auto from degu deg_iu have deg_iun: "degree ?iu < n" by auto from L.factorization_lattice(2)[OF deg_iu0 pl0 mon_iu deg_iun degf dvd] have "f ∈ poly_of_vec ` lattice_of ?L" using deg_iu by auto then obtain fv where f: "f = poly_of_vec fv" and fv: "fv ∈ lattice_of ?L" by auto have norm: "∥fv∥⇧^{2}= ∥f∥⇧^{2}" unfolding f by simp have fv0: "fv ≠ 0⇩_{v}n" using f0 unfolding f by auto with fv have fvL: "fv ∈ lattice_of ?L - {0⇩_{v}n}" by auto from short(3)[OF this, unfolded norm] have "rat_of_int ∥LLL_short_polynomial pl n u∥⇧^{2}≤ rat_of_int (2 ^ (n - 1) * ∥f∥⇧^{2})" by simp thus "∥LLL_short_polynomial pl n u∥⇧^{2}≤ 2 ^ (n - 1) * ∥f∥⇧^{2}" by linarith qed context LLL_implementation begin lemma LLL_reconstruction: assumes "LLL_reconstruction f us = fs" and "degree f ≠ 0" and "poly_mod.unique_factorization_m pl f (lead_coeff f, mset us)" and "f dvd F" and "⋀ ui. ui ∈ set us ⟹ poly_mod.Mp pl ui = ui" and F0: "F ≠ 0" and cop: "coprime (lead_coeff F) p" and sf: "poly_mod.square_free_m p F" and pl1: "pl > 1" and plp: "pl = p^l" and p: "prime p" and large: "2^(5 * (degree F - 1) * (degree F - 1)) * ∥F∥⇧^{2}^(2 * (degree F - 1)) < pl⇧^{2}" shows "f = prod_list fs ∧ (∀ fi ∈ set fs. irreducible⇩_{d}fi)" proof - interpret p: poly_mod_prime p by (standard, rule p) interpret pl: poly_mod_2 "pl" by (standard, rule pl1) from pl1 plp have l0: "l ≠ 0" by (cases l, auto) show ?thesis using assms(1-5) proof (induct f us arbitrary: fs rule: LLL_reconstruction.induct) case (1 f us fs) define u where "u = choose_u us" define g where "g = LLL_short_polynomial pl (degree f) u" define k where "k = gcd f g" note res = 1(3) note degf = 1(4) note uf = 1(5) note fF = 1(6) note norm = 1(7) note to_fact = pl.unique_factorization_m_imp_factorization note fact = to_fact[OF uf] have mon_gs: "ui ∈ set us ⟹ monic ui" for ui using norm fact unfolding pl.factorization_m_def by auto from p.coprime_lead_coeff_factor[OF p.prime] fF cop have cop: "coprime (lead_coeff f) p" unfolding dvd_def by blast have plf0: "pl.Mp f ≠ 0" using fact pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf by fastforce have "degree f = pl.degree_m f" by (rule sym, rule poly_mod.degree_m_eq[OF _ pl.m1], insert cop p, simp add: l0 p.coprime_exp_mod plp) also have "… = sum_mset (image_mset pl.degree_m (mset us))" unfolding pl.factorization_m_degree[OF fact plf0] .. also have "… = sum_list (map pl.degree_m us)" unfolding sum_mset_sum_list[symmetric] by auto also have "… = sum_list (map degree us)" by (rule arg_cong[OF map_cong, OF refl], rule pl.monic_degree_m, insert mon_gs, auto) finally have degf_gs: "degree f = sum_list (map degree us)" by auto hence gs: "us ≠ []" using degf by (cases us, auto) from choose_u_member[OF gs] have u_gs: "u ∈ set us" unfolding u_def by auto from fact u_gs have irred: "pl.irreducible⇩_{d}_m u" unfolding pl.factorization_m_def by auto hence deg_u: "degree u ≠ 0" unfolding pl.irreducible⇩_{d}_m_def norm[OF u_gs] by auto have deg_uf: "degree u ≤ degree f" unfolding degf_gs using split_list[OF u_gs] by auto from mon_gs[OF u_gs] have mon_u: "monic u" and u0: "u ≠ 0" by auto have f0: "f ≠ 0" using degf by auto from norm have norm': "image_mset pl.Mp (mset us) = mset us" by (induct us, auto) have pl0: "pl ≠ 0" using pl1 by auto note short_main = LLL_short_polynomial[OF deg_u deg_uf pl1 mon_u] from short_main(1-2)[folded g_def] have "degree k < degree f" unfolding k_def by (smt Suc_leI Suc_less_eq degree_gcd1 gcd.commute le_imp_less_Suc le_trans) hence deg_fk: "(degree k = 0 ∨ degree f ≤ degree k) = (degree k = 0)" by auto note res = res[unfolded LLL_reconstruction.simps[of f us] Let_def, folded u_def, folded g_def, folded k_def, unfolded deg_fk] show ?case proof (cases "degree k = 0") case True with res have fs: "fs = [f]" by auto from sf fF have sf: "p.square_free_m f" using p.square_free_m_factor(1)[of f] unfolding dvd_def by auto have irr: "irreducible⇩_{d}f" proof (rule ccontr) assume "¬ irreducible⇩_{d}f" from reducible⇩_{d}E[OF this] degf obtain f1 f2 where f: "f = f1 * f2" and deg12: "degree f1 ≠ 0" "degree f2 ≠ 0" "degree f1 < degree f" "degree f2 < degree f" by (simp, metis) from pl.unique_factorization_m_factor[OF p uf[unfolded f], folded f, OF cop sf l0 plp] obtain us1 us2 where uf12: "pl.unique_factorization_m f1 (lead_coeff f1, us1)" "pl.unique_factorization_m f2 (lead_coeff f2, us2)" and gs: "mset us = us1 + us2" and norm12: "image_mset pl.Mp us2 = us2" "image_mset pl.Mp us1 = us1" unfolding pl.Mf_def norm' split by (auto simp: pl.Mf_def) note norm_u = norm[OF u_gs] from u_gs have u_gs': "u ∈# mset us" by auto with pl.factorization_m_mem_dvdm[OF fact, of u] have u_f: "pl.dvdm u f" by auto from u_gs'[unfolded gs] have "u ∈# us1 ∨ u ∈# us2" by auto with pl.factorization_m_mem_dvdm[OF to_fact[OF uf12(1)], of u] pl.factorization_m_mem_dvdm[OF to_fact[OF uf12(2)], of u] have "pl.dvdm u f1 ∨ pl.dvdm u f2" unfolding norm12 norm_u by auto from this have "∃ f1 f2. f = f1 * f2 ∧ degree f1 ≠ 0 ∧ degree f2 ≠ 0 ∧ degree f1 < degree f ∧ degree f2 < degree f ∧ pl.dvdm u f1" proof assume "pl.dvdm u f1" thus ?thesis using f deg12 by auto next from f have f: "f = f2 * f1" by auto assume "pl.dvdm u f2" thus ?thesis using f deg12 by auto qed then obtain f1 f2 where prod: "f = f1 * f2" and deg: "degree f1 ≠ 0" "degree f2 ≠ 0" "degree f1 < degree f" "degree f2 < degree f" and uf1: "pl.dvdm u f1" by auto from pl.unique_factorization_m_factor[OF p uf[unfolded prod], folded prod, OF cop sf l0 plp] obtain us1 where fact_f1: "pl.unique_factorization_m f1 (lead_coeff f1, us1)" by auto have plf1: "pl.Mp f1 ≠ 0" using to_fact[OF fact_f1] pl.factorization_m_lead_coeff pl.unique_factorization_m_zero fact_f1 by fastforce have "degree u ≤ degree f1" by (rule pl.dvdm_degree[OF mon_u uf1 plf1]) with deg have deg_uf: "degree u < degree f" by auto have pl0: "pl ≠ 0" using pl.m1 plp by linarith let ?n = "degree f" let ?n1 = "degree f1" let ?d = "degree u" from prod fF have f1F: "f1 dvd F" unfolding dvd_def by auto from deg_uf have deg_uf': "?d ≤ ?n" by auto from deg have f1_0: "f1 ≠ 0" by auto have ug: "pl.dvdm u g" using short_main(3) unfolding g_def . have g0: "g ≠ 0" using short_main(2) unfolding g_def . have deg_gf: "degree g < degree f" using short_main(1) unfolding g_def . let ?N = "degree F" from fF prod have f1F: "f1 dvd F" unfolding dvd_def by auto have "∥g∥⇧^{2}≤ 2 ^ (?n - 1) * ∥f1∥⇧^{2}" unfolding g_def by (rule short_main(4)[OF deg_uf _ uf1], insert deg, auto) also have "… ≤ 2 ^ (?n - 1) * (2 ^ (2 * degree f1) * ∥F∥⇧^{2})" by (rule mult_left_mono[OF sq_norm_factor_bound[OF f1F F0]], simp) also have "… = 2 ^ ((?n - 1) + 2 * degree f1) * ∥F∥⇧^{2}" unfolding power_add by simp also have "… ≤ 2 ^ ((?n - 1) + 2 * (?n - 1)) * ∥F∥⇧^{2}" by (rule mult_right_mono, insert deg(3), auto) also have "… = 2 ^ (3 * (?n - 1)) * ∥F∥⇧^{2}" by simp finally have ineq_g: "∥g∥⇧^{2}≤ 2 ^ (3 * (?n - 1)) * ∥F∥⇧^{2}" . from power_mono[OF this, of ?n1] have ineq1: "∥g∥⇧^{2}^ ?n1 ≤ (2 ^ (3 * (?n - 1)) * ∥F∥⇧^{2})^?n1" by auto from F0 have normF: "∥F∥⇧^{2}≥ 1" using sq_norm_poly_pos[of F] by presburger from g0 have normg: "∥g∥⇧^{2}≥ 1" using sq_norm_poly_pos[of g] by presburger from f0 have normf: "∥f∥⇧^{2}≥ 1" using sq_norm_poly_pos[of f] by presburger from f1_0 have normf1: "∥f1∥⇧^{2}≥ 1" using sq_norm_poly_pos[of f1] by presburger from power_mono[OF sq_norm_factor_bound[OF f1F F0], of "degree g"] have ineq2: "∥f1∥⇧^{2}^ degree g ≤ (2 ^ (2 * ?n1) * ∥F∥⇧^{2}) ^ degree g" by auto also have "… ≤ (2 ^ (2 * ?n1) * ∥F∥⇧^{2}) ^ (?n - 1)" by (rule pow_mono_exp, insert deg_gf normF, auto) finally have ineq2: "∥f1∥⇧^{2}^ degree g ≤ (2 ^ (2 * ?n1) * ∥F∥⇧^{2}) ^ (?n - 1)" . have nN: "?n ≤ ?N" using fF F0 by (metis dvd_imp_degree_le) from deg nN have n1N: "?n1 ≤ ?N - 1" by auto have "∥f1∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ ?n1 ≤ (2 ^ (2 * ?n1) * ∥F∥⇧^{2}) ^ (?n - 1) * (2 ^ (3 * (?n - 1)) * ∥F∥⇧^{2})^?n1" by (rule mult_mono[OF ineq2 ineq1], force+) also have "… ≤ (2 ^ (2 * (?N - 1)) * ∥F∥⇧^{2}) ^ (?N - 1) * (2 ^ (3 * (?N - 1)) * ∥F∥⇧^{2}) ^ (?N - 1)" by (rule mult_mono[OF power_both_mono[OF _ _ mult_mono] power_both_mono], insert normF n1N nN, auto intro: power_both_mono mult_mono) also have "… = 2 ^ (2 * (?N -1) * (?N - 1) + 3 * (?N - 1) * (?N - 1)) * (∥F∥⇧^{2})^((?N - 1) + (?N - 1))" unfolding power_mult_distrib power_add power_mult by simp also have "2 * (?N - 1) * (?N - 1) + 3 * (?N - 1) * (?N - 1) = 5 * (?N - 1) * (?N - 1)" by simp also have "?N - 1 + (?N - 1) = 2 * (?N - 1)" by simp also have "2^(5 * (?N - 1) * (?N - 1)) * ∥F∥⇧^{2}^(2 * (?N - 1)) < pl^2" by (rule large) finally have large: "∥f1∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree f1 < pl⇧^{2}" . have deg_ug: "degree u ≤ degree g" proof (rule pl.dvdm_degree[OF mon_u ug], standard) assume "pl.Mp g = 0" from arg_cong[OF this, of "λ p. coeff p (degree g)"] have "pl.M (coeff g (degree g)) = 0" by (auto simp: pl.Mp_def coeff_map_poly) from this[unfolded pl.M_def] obtain c where lg: "lead_coeff g = pl * c" by auto with g0 have c0: "c ≠ 0" by auto hence "pl^2 ≤ (lead_coeff g)^2" unfolding lg abs_le_square_iff[symmetric] by (rule aux_abs_int) also have "… ≤ ∥g∥⇧^{2}^ 1" using coeff_le_sq_norm[of g] by auto also have "… ≤ ∥g∥⇧^{2}^ degree f1" by (rule pow_mono_exp, insert deg normg, auto) also have "… = 1 * …" by simp also have "… ≤ ∥f1∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree f1" by (rule mult_right_mono, insert normf1, auto) also have "… < pl⇧^{2}" by (rule large) finally show False by auto qed from deg deg_u deg_ug have "degree f1 > 0" "degree g > 0" by auto from common_factor_via_short[OF this mon_u _ uf1 ug large] deg_u pl.m1 have "0 < degree (gcd f1 g)" by auto moreover from True[unfolded k_def] have "degree (gcd f g) = 0" . moreover have dvd: "gcd f1 g dvd gcd f g" using f0 unfolding prod by simp ultimately show False using divides_degree[OF dvd] using f0 by simp qed show ?thesis unfolding fs using irr by auto next case False define f1 where "f1 = f div k" have f: "f = f1 * k" unfolding f1_def k_def by auto with arg_cong[OF this, of degree] f0 have deg_f1k: "degree f = degree f1 + degree k" by (auto simp: degree_mult_eq) from f fF have dvd: "f1 dvd F" "k dvd F" unfolding dvd_def by auto obtain gs1 gs2 where part: "List.partition (λgi. p.dvdm gi f1) us = (gs1, gs2)" by force note IH = 1(1-2)[OF refl u_def g_def k_def refl, unfolded deg_fk, OF False f1_def part[symmetric] refl] obtain fs1 where fs1: "LLL_reconstruction f1 gs1 = fs1" by auto obtain fs2 where fs2: "LLL_reconstruction k gs2 = fs2" by auto from False res[folded f1_def, unfolded part split fs1 fs2] have fs: "fs = fs1 @ fs2" by auto from short_main(1) have deg_gf: "degree g < degree f" unfolding g_def by auto from short_main(2) have g0: "g ≠ 0" unfolding g_def by auto have deg_kg: "degree k ≤ degree g" unfolding k_def gcd.commute[of f g] by (rule degree_gcd1[OF g0]) from deg_gf deg_kg have deg_kf: "degree k < degree f" by auto with deg_f1k have deg_f1: "degree f1 ≠ 0" by auto have sf_f: "p.square_free_m f" using sf fF p.square_free_m_factor unfolding dvd_def by blast from p.unique_factorization_m_factor_partition[OF l0 uf[unfolded plp] f cop sf_f part] have uf: "pl.unique_factorization_m f1 (lead_coeff f1, mset gs1)" "pl.unique_factorization_m k (lead_coeff k, mset gs2)" by (auto simp: plp) have "set us = set gs1 ∪ set gs2" using part by auto with norm have norm_12: "gi ∈ set gs1 ∨ gi ∈ set gs2 ⟹ pl.Mp gi = gi" for gi by auto note IH1 = IH(1)[OF fs1 deg_f1 uf(1) dvd(1) norm_12] note IH2 = IH(2)[OF fs2 False uf(2) dvd(2) norm_12] show ?thesis unfolding fs f using IH1 IH2 by auto qed qed qed lemma LLL_many_reconstruction: assumes "LLL_many_reconstruction f us = fs" and "degree f ≠ 0" and "poly_mod.unique_factorization_m pl f (lead_coeff f, mset us)" and "f dvd F" and "⋀ ui. ui ∈ set us ⟹ poly_mod.Mp pl ui = ui" and F0: "F ≠ 0" and cop: "coprime (lead_coeff F) p" and sf: "poly_mod.square_free_m p F" and pl1: "pl > 1" and plp: "pl = p^l" and p: "prime p" and large: "2^(5 * (degree F div 2) * (degree F div 2)) * ∥F∥⇧^{2}^(2 * (degree F div 2)) < pl⇧^{2}" shows "f = prod_list fs ∧ (∀ fi ∈ set fs. irreducible⇩_{d}fi)" proof - interpret p: poly_mod_prime p by (standard, rule p) interpret pl: poly_mod_2 "pl" by (standard, rule pl1) from pl1 plp have l0: "l ≠ 0" by (cases l, auto) show ?thesis using assms(1-5) proof (induct f us arbitrary: fs rule: LLL_many_reconstruction.induct) case (1 f us fs) note res = 1(3) note degf = 1(4) note uf = 1(5) note fF = 1(6) note norm = 1(7) note to_fact = pl.unique_factorization_m_imp_factorization note fact = to_fact[OF uf] have mon_gs: "ui ∈ set us ⟹ monic ui" for ui using norm fact unfolding pl.factorization_m_def by auto from p.coprime_lead_coeff_factor[OF p.prime] fF cop have cop: "coprime (lead_coeff f) p" unfolding dvd_def by blast have plf0: "pl.Mp f ≠ 0" using fact pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf by fastforce have "degree f = pl.degree_m f" by (rule sym, rule poly_mod.degree_m_eq[OF _ pl.m1], insert cop p, simp add: l0 p.coprime_exp_mod plp) also have "… = sum_mset (image_mset pl.degree_m (mset us))" unfolding pl.factorization_m_degree[OF fact plf0] .. also have "… = sum_list (map pl.degree_m us)" unfolding sum_mset_sum_list[symmetric] by auto also have "… = sum_list (map degree us)" by (rule arg_cong[OF map_cong, OF refl], rule pl.monic_degree_m, insert mon_gs, auto) finally have degf_gs: "degree f = sum_list (map degree us)" by auto hence gs: "us ≠ []" using degf by (cases us, auto) from 1(4) have f0: "f ≠ 0" and df0: "degree f ≠ 0" by auto from norm have norm': "image_mset pl.Mp (mset us) = mset us" by (induct us, auto) have pl0: "pl ≠ 0" using pl1 by auto let ?D2 = "degree F div 2" let ?d2 = "degree f div 2" define gg where "gg = LLL_short_polynomial pl (Suc ?d2)" let ?us = "filter (λu. degree u ≤ ?d2) us" note res = res[unfolded LLL_many_reconstruction.simps[of f us], unfolded Let_def, folded gg_def] let ?f2_opt = "find_map_filter (λu. gcd f (gg u)) (λf2. 0 < degree f2 ∧ degree f2 < degree f) ?us" show ?case proof (cases ?f2_opt) case (Some f2) from find_map_filter_Some[OF this] obtain g where deg_f2: "degree f2 ≠ 0" "degree f2 < degree f" and dvd: "f2 dvd f" and gcd: "f2 = gcd f g" by auto note res = res[unfolded Some option.simps] define f1 where "f1 = f div f2" have f: "f = f1 * f2" unfolding f1_def using dvd by auto with arg_cong[OF this, of degree] f0 have deg_sum: "degree f = degree f1 + degree f2" by (auto simp: degree_mult_eq) with deg_f2 have deg_f1: "degree f1 ≠ 0" "degree f1 < degree f" by auto from f fF have dvd: "f1 dvd F" "f2 dvd F" unfolding dvd_def by auto obtain gs1 gs2 where part: "List.partition (λgi. p.dvdm gi f1) us = (gs1, gs2)" by force note IH = 1(1-2)[OF refl refl refl, unfolded Let_def, folded gg_def, OF Some f1_def part[symmetric] refl] obtain fs1 where fs1: "LLL_many_reconstruction f1 gs1 = fs1" by blast obtain fs2 where fs2: "LLL_many_reconstruction f2 gs2 = fs2" by blast from res[folded f1_def, unfolded part split fs1 fs2] have fs: "fs = fs1 @ fs2" by auto have sf_f: "p.square_free_m f" using sf fF p.square_free_m_factor unfolding dvd_def by blast from p.unique_factorization_m_factor_partition[OF l0 uf[unfolded plp] f cop sf_f part] have uf: "pl.unique_factorization_m f1 (lead_coeff f1, mset gs1)" "pl.unique_factorization_m f2 (lead_coeff f2, mset gs2)" by (auto simp: plp) have "set us = set gs1 ∪ set gs2" using part by auto with norm have norm_12: "gi ∈ set gs1 ∨ gi ∈ set gs2 ⟹ pl.Mp gi = gi" for gi by auto note IH1 = IH(1)[OF fs1 deg_f1(1) uf(1) dvd(1) norm_12] note IH2 = IH(2)[OF fs2 deg_f2(1) uf(2) dvd(2) norm_12] show ?thesis unfolding fs f using IH1 IH2 by auto next case None from res[unfolded None option.simps] have fs_f: "fs = [f]" by simp from sf fF have sf: "p.square_free_m f" using p.square_free_m_factor(1)[of f] unfolding dvd_def by auto have "irreducible⇩_{d}f" proof (rule ccontr) assume "¬ irreducible⇩_{d}f" from reducible⇩_{d}E[OF this] degf obtain f1 f2 where f: "f = f1 * f2" and deg12: "degree f1 ≠ 0" "degree f2 ≠ 0" "degree f1 < degree f" "degree f2 < degree f" by (simp, metis) from f0 have "degree f = degree f1 + degree f2" unfolding f by (auto simp: degree_mult_eq) hence "degree f1 ≤ degree f div 2 ∨ degree f2 ≤ degree f div 2" by auto then obtain f1 f2 where f: "f = f1 * f2" and deg12: "degree f1 ≠ 0" "degree f2 ≠ 0" "degree f1 ≤ degree f div 2" "degree f2 < degree f" proof (standard, goal_cases) case 1 from 1(1)[of f1 f2] 1(2) f deg12 show ?thesis by auto next case 2 from 2(1)[of f2 f1] 2(2) f deg12 show ?thesis by auto qed from f0 f have f10: "f1 ≠ 0" by auto from sf f have sf1: "p.square_free_m f1" using p.square_free_m_factor(1)[of f1] by auto from p.coprime_lead_coeff_factor[OF p.prime cop[unfolded f]] have cop1: "coprime (lead_coeff f1) p" by auto have deg_m1: "pl.degree_m f1 = degree f1" by (rule poly_mod.degree_m_eq[OF _ pl.m1], insert cop1 p, simp add: l0 p.coprime_exp_mod plp) from pl.unique_factorization_m_factor[OF p uf[unfolded f], folded f, OF cop sf l0 plp] obtain us1 us2 where uf12: "pl.unique_factorization_m f1 (lead_coeff f1, us1)" "pl.unique_factorization_m f2 (lead_coeff f2, us2)" and gs: "mset us = us1 + us2" and norm12: "image_mset pl.Mp us2 = us2" "image_mset pl.Mp us1 = us1" unfolding pl.Mf_def norm' split by (auto simp: pl.Mf_def) from gs have "x ∈# us1 ⟹ x ∈# mset us" for x by auto hence sub1: "x ∈# us1 ⟹ x ∈ set us" for x by auto from to_fact[OF uf12(1)] have fact1: "pl.factorization_m f1 (lead_coeff f1, us1)" . have plf10: "pl.Mp f1 ≠ 0" using fact1 pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf12(1) by fastforce have "degree f1 = pl.degree_m f1" using deg_m1 by simp also have "… = sum_mset (image_mset pl.degree_m us1)" unfolding pl.factorization_m_degree[OF fact1 plf10] .. also have "… = sum_mset (image_mset degree us1)" by (rule arg_cong[of _ _ sum_mset], rule image_mset_cong, rule pl.monic_degree_m, rule mon_gs, rule sub1) finally have degf1_sum: "degree f1 = sum_mset (image_mset degree us1)" by auto with deg12 have "us1 ≠ {#}" by auto then obtain u us11 where us1: "us1 = {#u#} + us11" by (cases us1, auto) hence u1: "u ∈# us1" by auto hence u: "u ∈ set us" by (rule sub1) let ?g = "gg u" from pl.factorization_m_mem_dvdm[OF fact1, of u] u1 have u_f1: "pl.dvdm u f1" by auto note norm_u = norm[OF u] from fact u have irred: "pl.irreducible⇩_{d}_m u" unfolding pl.factorization_m_def by auto hence deg_u: "degree u ≠ 0" unfolding pl.irreducible⇩_{d}_m_def norm[OF u] by auto have "degree u ≤ degree f1" unfolding degf1_sum unfolding us1 by simp also have "… ≤ degree f div 2" by fact finally have deg_uf: "degree u ≤ degree f div 2" . hence deg_uf': "degree u ≤ Suc (degree f div 2)" "degree u < Suc (degree f div 2)" by auto from mon_gs[OF u] have mon_u: "monic u" . note short = LLL_short_polynomial[OF deg_u deg_uf'(1) pl1 mon_u, folded gg_def] note short = short(1-3) short(4)[OF deg_uf'(2)] from short(1,2) deg12(1,3) f10 have "degree (gcd f ?g) ≤ degree f div 2" by (metis Suc_leI Suc_le_mono degree_gcd1 gcd.commute le_trans) also have "… < degree f" using degf by simp finally have "degree (gcd f ?g) < degree f" by simp with find_map_filter_None[OF None, simplified, rule_format, of u] deg_uf u have deg_gcd: "degree (gcd f (?g)) = 0" by (auto simp: gcd.commute) have "gcd f1 (?g) dvd gcd f (?g)" using f0 unfolding f by simp from divides_degree[OF this, unfolded deg_gcd] f0 have deg_gcd1: "degree (gcd f1 (?g)) = 0" by auto from F0 have normF: "∥F∥⇧^{2}≥ 1" using sq_norm_poly_pos[of F] by presburger have g0: "?g ≠ 0" using short(2) . from g0 have normg: "∥?g∥⇧^{2}≥ 1" using sq_norm_poly_pos[of "?g"] by presburger from f10 have normf1: "∥f1∥⇧^{2}≥ 1" using sq_norm_poly_pos[of f1] by presburger from fF f have f1F: "f1 dvd F" unfolding dvd_def by auto have pl_ge0: "pl ≥ 0" using pl.poly_mod_2_axioms poly_mod_2_def by auto from fF have "degree f ≤ degree F" using F0 f0 by (metis dvd_imp_degree_le) hence d2D2: "?d2 ≤ ?D2" by simp with deg12(3) have df1_D2: "degree f1 ≤ ?D2" by linarith from short(1) d2D2 have dg_D2: "degree (gg u) ≤ ?D2" by linarith have "∥f1∥⇧^{2}^ degree (gg u) * ∥gg u∥⇧^{2}^ degree f1 ≤ ∥f1∥⇧^{2}^ ?D2 * ∥gg u∥⇧^{2}^ ?D2" by (rule mult_mono[OF pow_mono_exp pow_mono_exp], insert normf1 normg, auto intro: df1_D2 dg_D2) also have "… = (∥f1∥⇧^{2}* ∥gg u∥⇧^{2})^?D2" by (simp add: power_mult_distrib) also have "… ≤ (∥f1∥⇧^{2}* (2^?D2 * ∥f1∥⇧^{2}))^?D2" by (rule power_mono[OF mult_left_mono[OF order.trans[OF short(4)[OF f10 u_f1]]]], insert deg12 d2D2, auto intro!: mult_mono) also have "… = ∥f1∥⇧^{2}^ (?D2 + ?D2) * 2^(?D2 * ?D2)" unfolding power_add power_mult_distrib power_mult by simp also have "… ≤ (2 ^ (2 * ?D2) * ∥F∥⇧^{2}) ^ (?D2 + ?D2) * 2^(?D2 * ?D2)" by (rule mult_right_mono[OF order.trans[OF power_mono[OF sq_norm_factor_bound[OF f1F F0]]]], auto intro!: power_mono mult_right_mono df1_D2) also have "… = 2 ^ (2 * ?D2 * (?D2 + ?D2) + ?D2 * ?D2) * ∥F∥⇧^{2}^ (?D2 + ?D2)" unfolding power_mult_distrib power_mult power_add by simp also have "2 * ?D2 * (?D2 + ?D2) + ?D2 * ?D2 = 5 * ?D2 * ?D2" by simp also have "?D2 + ?D2 = 2 * ?D2" by simp finally have large: "∥f1∥⇧^{2}^ degree (gg u) * ∥gg u∥⇧^{2}^ degree f1 < pl^2" using large by simp have "degree u ≤ degree (?g)" proof (rule pl.dvdm_degree[OF mon_u short(3)], standard) assume "pl.Mp (?g) = 0" from arg_cong[OF this, of "λ p. coeff p (degree ?g)"] have "pl.M (coeff ?g (degree ?g)) = 0" by (auto simp: pl.Mp_def coeff_map_poly) from this[unfolded pl.M_def] obtain c where lg: "lead_coeff ?g = pl * c" by auto with g0 have c0: "c ≠ 0" by auto hence "pl^2 ≤ (lead_coeff ?g)^2" unfolding lg abs_le_square_iff[symmetric] by (rule aux_abs_int) also have "… ≤ ∥?g∥⇧^{2}" using coeff_le_sq_norm[of ?g] by auto also have "… = ∥?g∥⇧^{2}^ 1" by simp also have "… ≤ ∥?g∥⇧^{2}^ degree f1" by (rule pow_mono_exp, insert deg12 normg, auto) also have "… = 1 * …" by simp also have "… ≤ ∥f1∥⇧^{2}^ degree ?g * ∥?g∥⇧^{2}^ degree f1" by (rule mult_right_mono, insert normf1, auto) also have "… < pl⇧^{2}" by (rule large) finally show False by auto qed with deg_u have deg_g: "0 < degree (gg u)" by auto have pl_ge0: "pl ≥ 0" using pl.poly_mod_2_axioms poly_mod_2_def by auto from fF have "degree f ≤ degree F" using F0 f0 by (metis dvd_imp_degree_le) hence d2D2: "?d2 ≤ ?D2" by simp with deg12(3) have df1_D2: "degree f1 ≤ ?D2" by linarith from short(1) d2D2 have dg_D2: "degree (gg u) ≤ ?D2" by linarith have "0 < degree f1" "0 < degree u" using deg12 deg_u by auto from common_factor_via_short[of f1 "gg u", OF this(1) deg_g mon_u this(2) u_f1 short(3) _ pl_ge0] deg_gcd1 have "pl^2 ≤ ∥f1∥⇧^{2}^ degree (gg u) * ∥gg u∥⇧^{2}^ degree f1" by linarith also have "… < pl^2" by (rule large) finally show False by simp qed thus ?thesis using fs_f by simp qed qed qed end lemma LLL_factorization: assumes res: "LLL_factorization f = gs" and sff: "square_free f" and deg: "degree f ≠ 0" shows "f = prod_list gs ∧ (∀g∈set gs. irreducible⇩_{d}g)" proof - let ?lc = "lead_coeff f" define p where "p ≡ suitable_prime_bz f" obtain c gs where fff: "finite_field_factorization_int p f = (c,gs)" by force let ?degs = "map degree gs" note res = res[unfolded LLL_factorization_def Let_def, folded p_def, unfolded fff split, folded] from suitable_prime_bz[OF sff refl] have prime: "prime p" and cop: "coprime ?lc p" and sf: "poly_mod.square_free_m p f" unfolding p_def by auto note res from prime interpret p: poly_mod_prime p by unfold_locales define K where "K = 2^(5 * (degree f - 1) * (degree f - 1)) * ∥f∥⇧^{2}^(2 * (degree f - 1))" define N where "N = sqrt_int_ceiling K" have K0: "K ≥ 0" unfolding K_def by fastforce have N0: "N ≥ 0" unfolding N_def sqrt_int_ceiling using K0 by (smt of_int_nonneg real_sqrt_ge_0_iff zero_le_ceiling) define n where "n = find_exponent p N" note res = res[folded n_def[unfolded N_def K_def]] note n = find_exponent[OF p.m1, of N, folded n_def] note bh = p.berlekamp_and_hensel_separated(1)[OF cop sf refl fff n(2)] from deg have f0: "f ≠ 0" by auto from n p.m1 have pn1: "p ^ n > 1" by auto note res = res[folded bh(1)] note * = p.berlekamp_hensel_unique[OF cop sf bh n(2)] note ** = p.berlekamp_hensel_main[OF n(2) bh cop sf fff] from res * ** have uf: "poly_mod.unique_factorization_m (p ^ n) f (lead_coeff f, mset (berlekamp_hensel p n f))" and norm: "⋀ui. ui ∈ set (berlekamp_hensel p n f) ⟹ poly_mod.Mp (p ^ n) ui = ui" unfolding berlekamp_hensel_def fff split by auto have K: "K < (p ^ n)⇧^{2}" using n sqrt_int_ceiling_bound[OF K0] by (smt N0 N_def n(1) power2_le_imp_le) show ?thesis by (rule LLL_implementation.LLL_reconstruction[OF res deg uf dvd_refl norm f0 cop sf pn1 refl prime K[unfolded K_def]]) qed lemma LLL_many_factorization: assumes res: "LLL_many_factorization f = gs" and sff: "square_free f" and deg: "degree f ≠ 0" shows "f = prod_list gs ∧ (∀g∈set gs. irreducible⇩_{d}g)" proof - let ?lc = "lead_coeff f" define p where "p ≡ suitable_prime_bz f" obtain c gs where fff: "finite_field_factorization_int p f = (c,gs)" by force let ?degs = "map degree gs" note res = res[unfolded LLL_many_factorization_def Let_def, folded p_def, unfolded fff split, folded] from suitable_prime_bz[OF sff refl] have prime: "prime p" and cop: "coprime ?lc p" and sf: "poly_mod.square_free_m p f" unfolding p_def by auto note res from prime interpret p: poly_mod_prime p by unfold_locales define K where "K = 2^(5 * (degree f div 2) * (degree f div 2)) * ∥f∥⇧^{2}^(2 * (degree f div 2))" define N where "N = sqrt_int_ceiling K" have K0: "K ≥ 0" unfolding K_def by fastforce have N0: "N ≥ 0" unfolding N_def sqrt_int_ceiling using K0 by (smt of_int_nonneg real_sqrt_ge_0_iff zero_le_ceiling) define n where "n = find_exponent p N" note res = res[folded n_def[unfolded N_def K_def]] note n = find_exponent[OF p.m1, of N, folded n_def] note bh = p.berlekamp_and_hensel_separated(1)[OF cop sf refl fff n(2)] from deg have f0: "f ≠ 0" by auto from n p.m1 have pn1: "p ^ n > 1" by auto note res = res[folded bh(1)] note * = p.berlekamp_hensel_unique[OF cop sf bh n(2)] note ** = p.berlekamp_hensel_main[OF n(2) bh cop sf fff] from res * ** have uf: "poly_mod.unique_factorization_m (p ^ n) f (lead_coeff f, mset (berlekamp_hensel p n f))" and norm: "⋀ui. ui ∈ set (berlekamp_hensel p n f) ⟹ poly_mod.Mp (p ^ n) ui = ui" unfolding berlekamp_hensel_def fff split by auto have K: "K < (p ^ n)⇧^{2}" using n sqrt_int_ceiling_bound[OF K0] by (smt N0 N_def n(1) power2_le_imp_le) show ?thesis by (rule LLL_implementation.LLL_many_reconstruction[OF res deg uf dvd_refl norm f0 cop sf pn1 refl prime K[unfolded K_def]]) qed lift_definition one_lattice_LLL_factorization :: int_poly_factorization_algorithm is LLL_factorization using LLL_factorization by auto lift_definition many_lattice_LLL_factorization :: int_poly_factorization_algorithm is LLL_many_factorization using LLL_many_factorization by auto lemma LLL_factorization_primitive: assumes "LLL_factorization f = fs" "square_free f" "0 < degree f" "primitive f" shows "f = prod_list fs ∧ (∀fi∈set fs. irreducible fi ∧ 0 < degree fi ∧ primitive fi)" using assms(1) by (intro int_poly_factorization_algorithm_irreducible[of one_lattice_LLL_factorization, OF _ assms(2-)], transfer, auto) thm factorize_int_poly[of one_lattice_LLL_factorization] thm factorize_int_poly[of many_lattice_LLL_factorization] end