Theory Hensels_Lemma
theory Hensels_Lemma
imports Padic_Int_Polynomials
begin
text‹
The following proof of Hensel's Lemma is directly adapted from Keith Conrad's proof which is
given in an online note \<^cite>‹"keithconrad"›. The same note was used as the basis for a
formalization of Hensel's Lemma by Robert Lewis in the Lean proof assistant
\<^cite>‹"Thi"›. ›
section‹Auxiliary Lemmas for Hensel's Lemma›
lemma(in ring) minus_sum:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
shows "⊖ (a ⊕ b) = ⊖ a ⊕ ⊖ b"
by (simp add: assms(1) assms(2) local.minus_add)
context padic_integers
begin
lemma poly_diff_val:
assumes "f ∈ carrier Zp_x"
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
shows "val_Zp (f∙a ⊖ f∙b) ≥ val_Zp (a ⊖ b)"
proof-
obtain c where c_def: "c ∈ carrier Zp ∧ (f∙a ⊖ f∙b) = (a ⊖ b) ⊗ c"
using assms
by (meson to_fun_diff_factor)
have 1: "val_Zp c ≥ 0"
using c_def val_pos by blast
have 2: "val_Zp (f∙a ⊖ f∙b) = val_Zp (a ⊖ b) + (val_Zp c)"
using c_def val_Zp_mult
by (simp add: assms(2) assms(3))
then show ?thesis
using "1" by auto
qed
text‹Restricted p-adic division›
definition divide where
"divide x y = (if x = 𝟬 then 𝟬 else
(𝗉[^](nat (ord_Zp x - ord_Zp y)) ⊗ ac_Zp x ⊗ (inv ac_Zp y)))"
lemma divide_closed:
assumes "x ∈ carrier Zp"
assumes "y ∈ carrier Zp"
assumes "y ≠ 𝟬"
shows "divide x y ∈ carrier Zp"
unfolding divide_def
apply(cases "x = 𝟬")
apply auto[1]
using assms ac_Zp_is_Unit
by (simp add: ac_Zp_in_Zp)
lemma divide_formula:
assumes "x ∈ carrier Zp"
assumes "y ∈ carrier Zp"
assumes "y ≠ 𝟬"
assumes "val_Zp x ≥ val_Zp y"
shows "y ⊗ divide x y = x"
apply(cases "x = 𝟬")
apply (simp add: divide_def mult_zero_l)
proof- assume A: "x ≠ 𝟬"
have 0: "y ⊗ divide x y = 𝗉[^] nat (ord_Zp y) ⊗ ac_Zp y ⊗ (𝗉[^](nat (ord_Zp x - ord_Zp y)) ⊗ ac_Zp x ⊗ (inv ac_Zp y))"
using assms ac_Zp_factors_x[of x] ac_Zp_factors_x[of y] A divide_def
by auto
hence 1: "y ⊗ divide x y = 𝗉[^] nat (ord_Zp y) ⊗ (𝗉[^](nat (ord_Zp x - ord_Zp y)) ⊗ ac_Zp x ⊗ ac_Zp y ⊗ (inv ac_Zp y))"
using mult_assoc mult_comm by auto
have 2: "(nat (ord_Zp y) + nat (ord_Zp x - ord_Zp y)) = nat (ord_Zp x)"
using assms ord_pos[of x] ord_pos[of y] A val_ord_Zp by auto
have "y ⊗ divide x y = 𝗉[^] nat (ord_Zp y) ⊗ 𝗉[^](nat (ord_Zp x - ord_Zp y)) ⊗ ac_Zp x"
using 1 A assms
by (simp add: ac_Zp_in_Zp ac_Zp_is_Unit mult_assoc)
thus "y ⊗ divide x y = x"
using "2" A ac_Zp_factors_x(1) assms(1) p_natpow_prod by auto
qed
lemma divide_nonzero:
assumes "x ∈ nonzero Zp"
assumes "y ∈ nonzero Zp"
assumes "val_Zp x ≥ val_Zp y"
shows "divide x y ∈ nonzero Zp"
by (metis assms(1) assms(2) assms(3) divide_closed divide_formula mult_zero_l nonzero_closed nonzero_memE(2) nonzero_memI)
lemma val_of_divide:
assumes "x ∈ carrier Zp"
assumes "y ∈ nonzero Zp"
assumes "val_Zp x ≥ val_Zp y"
shows "val_Zp (divide x y) = val_Zp x - val_Zp y"
proof-
have 0: "y ⊗ divide x y = x"
by (simp add: assms(1) assms(2) assms(3) divide_formula nonzero_closed nonzero_memE(2))
hence "val_Zp y + val_Zp (divide x y) = val_Zp x"
using assms(1) assms(2) divide_closed nonzero_closed not_nonzero_memI val_Zp_mult by fastforce
thus ?thesis
by (metis Extended_Int.eSuc_minus_1 add_0 assms(2) eint_minus_comm p_nonzero val_Zp_eq_frac_0 val_Zp_p)
qed
lemma val_of_divide':
assumes "x ∈ carrier Zp"
assumes "y ∈ carrier Zp"
assumes "y ≠ 𝟬"
assumes "val_Zp x ≥ val_Zp y"
shows "val_Zp (divide x y) = val_Zp x - val_Zp y"
using Zp_def assms(1) assms(2) assms(3) assms(4) padic_integers.not_nonzero_Zp
padic_integers.val_of_divide padic_integers_axioms by blast
end
lemma(in UP_cring) taylor_deg_1_eval''':
assumes "f ∈ carrier P"
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
assumes "c = to_fun (shift (2::nat) (T⇘a⇙ f)) (⊖b)"
assumes "b ⊗ (deriv f a) = (to_fun f a)"
shows "to_fun f (a ⊖ b) = (c ⊗ b[^](2::nat))"
proof-
have 0: "to_fun f (a ⊖ b) = (to_fun f a) ⊖ (deriv f a ⊗ b) ⊕ (c ⊗ b[^](2::nat))"
using assms taylor_deg_1_eval''
by blast
have 1: "(to_fun f a) ⊖ (deriv f a ⊗ b) = 𝟬"
using assms
proof -
have "∀f a. f ∉ carrier P ∨ a ∉ carrier R ∨ to_fun f a ∈ carrier R"
using to_fun_closed by presburger
then show ?thesis
using R.m_comm R.r_right_minus_eq assms(1) assms(2) assms(3) assms(5)
by (simp add: deriv_closed)
qed
have 2: "to_fun f (a ⊖ b) = 𝟬 ⊕ (c ⊗ b[^](2::nat))"
using 0 1
by simp
then show ?thesis using assms
by (simp add: taylor_closed to_fun_closed shift_closed)
qed
lemma(in padic_integers) res_diff_zero_fact:
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "(a ⊖ b) k = 0"
shows "a k = b k" "a k ⊖⇘Zp_res_ring k⇙ b k = 0"
apply(cases "k = 0")
apply (metis assms(1) assms(2) p_res_ring_0 p_res_ring_0' p_res_ring_car p_residue_padic_int p_residue_range' zero_le)
apply (metis R.add.inv_closed R.add.m_lcomm R.minus_eq R.r_neg R.r_zero Zp_residue_add_zero(2) assms(1) assms(2) assms(3))
using assms(2) assms(3) residue_of_diff by auto
lemma(in padic_integers) res_diff_zero_fact':
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "a k = b k"
shows "a k ⊖⇘Zp_res_ring k⇙ b k = 0"
by (simp add: assms(3) residue_minus)
lemma(in padic_integers) res_diff_zero_fact'':
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "a k = b k"
shows "(a ⊖ b) k = 0"
by (simp add: assms(2) assms(3) res_diff_zero_fact' residue_of_diff)
lemma(in padic_integers) is_Zp_cauchyI':
assumes "s ∈ closed_seqs Zp"
assumes "∀n::nat. ∃ k::int.∀m. m ≥ k ⟶ val_Zp (s (Suc m) ⊖ s m) ≥ n"
shows "is_Zp_cauchy s"
proof(rule is_Zp_cauchyI)
show A0: "s ∈ closed_seqs Zp"
by (simp add: assms(1))
show "⋀n. ∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ s n0 n = s n1 n"
proof-
fix n
show "∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ s n0 n = s n1 n"
proof(induction n)
case 0
then show ?case
proof-
have "∀n0 n1. 0 < n0 ∧ 0 < n1 ⟶ s n0 0 = s n1 0"
apply auto
proof-
fix n0 n1::nat
assume A: "n0 > 0" "n1 > 0"
have 0: "s n0 ∈ carrier Zp"
using A0
by (simp add: closed_seqs_memE)
have 1: "s n1 ∈ carrier Zp"
using A0
by (simp add: closed_seqs_memE)
show " s n0 (0::nat) = s n1 (0::nat)"
using A0 Zp_def 0 1 residues_closed
by (metis p_res_ring_0')
qed
then show ?thesis
by blast
qed
next
case (Suc n)
fix n
assume IH: "∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ s n0 n = s n1 n"
show " ∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ s n0 (Suc n) = s n1 (Suc n)"
proof-
obtain N where N_def: "∀n0 n1. N < n0 ∧ N < n1 ⟶ s n0 n = s n1 n"
using IH
by blast
obtain k where k_def: "∀m. (Suc m) ≥ k ⟶ val_Zp (s (Suc (Suc m)) ⊖ s (Suc m)) ≥ Suc (Suc n)"
using assms Suc_n_not_le_n
by (meson nat_le_iff)
have "∀n0 n1. Suc (max N (max n k)) < n0 ∧ Suc (max N (max n k))< n1 ⟶ s n0 (Suc n) = s n1 (Suc n)"
apply auto
proof-
fix n0 n1
assume A: "Suc (max N (max n k)) < n0" " Suc (max N (max n k)) < n1"
show "s n0 (Suc n) = s n1 (Suc n) "
proof-
obtain K where K_def: "K = Suc (max N (max n k))"
by simp
have P0: "⋀m. s ((Suc m)+ K) (Suc n) = s (Suc K) (Suc n)"
apply auto
proof-
fix m
show "s (Suc (m + K)) (Suc n) = s (Suc K) (Suc n)"
apply(induction m)
apply auto
proof-
fix m
assume A0: " s (Suc (m + K)) (Suc n) = s (Suc K) (Suc n)"
show " s (Suc (Suc (m + K))) (Suc n) = s (Suc K) (Suc n)"
proof-
have I: "k < m + K"
using K_def
by linarith
have "val_Zp (s (Suc (Suc (m + K))) ⊖ s (Suc (m + K))) ≥ Suc (Suc n)"
proof-
have "(Suc (m + K)) > k"
by (simp add: I less_Suc_eq)
then show ?thesis
using k_def less_imp_le_nat
by blast
qed
hence D: "val_Zp (s (Suc (Suc (m + K))) ⊖ s (Suc (m + K))) > (Suc n)"
using Suc_ile_eq by fastforce
have "s (Suc (Suc (m + K))) (Suc n) = s (Suc (m + K)) (Suc n)"
proof-
have "(s (Suc (Suc (m + K))) ⊖ s (Suc (m + K))) (Suc n) = 0"
using D assms(1) res_diff_zero_fact''[of "s (Suc (Suc (m + K)))" "s (Suc (m + K)) " "Suc n"]
val_Zp_dist_res_eq[of "s (Suc (Suc (m + K)))" "s (Suc (m + K)) " "Suc n"] unfolding val_Zp_dist_def
by (simp add: closed_seqs_memE)
hence 0: "(s (Suc (Suc (m + K))) (Suc n) ⊖⇘Zp_res_ring (Suc n)⇙ (s (Suc (m + K))) (Suc n)) = 0"
using res_diff_zero_fact(2)[of "s (Suc (Suc (m + K)))" "s (Suc (m + K))" "Suc n" ]
assms(1)
by (simp add: closed_seqs_memE)
show ?thesis
proof-
have 00: "cring (Zp_res_ring (Suc n))"
using R_cring by blast
have 01: " s (Suc (Suc (m + K))) (Suc n) ∈ carrier (Zp_res_ring (Suc n))"
using assms(1) closed_seqs_memE residues_closed by blast
have 02: "(⊖⇘Zp_res_ring (Suc n)⇙ (s (Suc (m + K)) (Suc n))) ∈ carrier (Zp_res_ring (Suc n)) "
by (meson "00" assms(1) cring.cring_simprules(3) closed_seqs_memE residues_closed)
show ?thesis
unfolding a_minus_def
using 00 01 02
cring.sum_zero_eq_neg[of "Zp_res_ring (Suc n)" "s (Suc (Suc (m + K))) (Suc n)"
"⊖⇘Zp_res_ring (Suc n)⇙s (Suc (m + K)) (Suc n)"]
by (metis 0 a_minus_def assms(1) cring.cring_simprules(21) closed_seqs_memE
p_res_ring_zero residues_closed)
qed
qed
then show ?thesis using A0 assms(1)
by simp
qed
qed
qed
have "∃m0. n0 = (Suc m0) + K"
proof-
have "n0 > K"
by (simp add: A(1) K_def)
then have "n0 = (Suc (n0 - K - 1)) + K"
by auto
then show ?thesis by blast
qed
then obtain m0 where m0_def: "n0 = (Suc m0) + K"
by blast
have "∃m0. n1 = (Suc m0) + K"
proof-
have "n1 > K"
by (simp add: A(2) K_def)
then have "n1 = (Suc (n1 - K - 1)) + K"
by auto
then show ?thesis by blast
qed
then obtain m1 where m1_def: "n1 = (Suc m1) + K"
by blast
have 0: "s n0 (Suc n) = s (Suc K) (Suc n)"
using m0_def P0[of "m0"] by auto
have 1: "s n1 (Suc n) = s (Suc K) (Suc n)"
using m1_def P0[of "m1"] by auto
show ?thesis using 0 1
by auto
qed
qed
then show ?thesis
by blast
qed
qed
qed
qed
section‹The Proof of Hensel's Lemma›
subsection‹Building a Locale for the Proof of Hensel's Lemma›
locale hensel = padic_integers+
fixes f::padic_int_poly
fixes a::padic_int
assumes f_closed[simp]: "f ∈ carrier Zp_x"
assumes a_closed[simp]: "a ∈ carrier Zp"
assumes fa_nonzero[simp]: "f∙a ≠𝟬"
assumes hensel_hypothesis[simp]: "(val_Zp (f∙a) > 2* val_Zp ((pderiv f)∙a))"
sublocale hensel < cring Zp
by (simp add: R.is_cring)
context hensel
begin
abbreviation f' where
"f' ≡ pderiv f"
lemma f'_closed:
"f' ∈ carrier Zp_x"
using f_closed pderiv_closed by blast
lemma f'_vals_closed:
assumes "a ∈ carrier Zp"
shows "f'∙a ∈ carrier Zp"
by (simp add: UP_cring.to_fun_closed Zp_x_is_UP_cring f'_closed)
lemma fa_closed:
"(f∙a) ∈ carrier Zp"
by (simp add: UP_cring.to_fun_closed Zp_x_is_UP_cring)
lemma f'a_closed:
"(f'∙a) ∈ carrier Zp"
proof-
have "f' ∈ carrier Zp_x"
by (simp add: f'_closed)
then show ?thesis
by (simp add: f'_vals_closed)
qed
lemma fa_nonzero':
"(f∙a) ∈ nonzero Zp"
using fa_closed fa_nonzero not_nonzero_Zp by blast
lemma f'a_nonzero[simp]:
"(f'∙a) ≠ 𝟬"
proof(rule ccontr)
assume "¬ (f'∙a) ≠ 𝟬"
then have "(f'∙a) = 𝟬"
by blast
then have "∞ < val_Zp (f∙a)" using hensel_hypothesis
by (simp add: val_Zp_def)
thus False
using eint_ord_simps(6) by blast
qed
lemma f'a_nonzero':
"(f'∙a) ∈ nonzero Zp"
using f'a_closed f'a_nonzero not_nonzero_Zp by blast
lemma f'a_not_infinite[simp]:
"val_Zp (f'∙a) ≠ ∞"
by (metis eint_ord_code(3) hensel_hypothesis linorder_not_less times_eint_simps(4))
lemma f'a_nonneg_val[simp]:
"val_Zp ((f'∙a)) ≥ 0"
using f'a_closed val_pos by blast
lemma hensel_hypothesis_weakened:
"val_Zp (f∙a) > val_Zp (f'∙a)"
proof-
have 0: "0 ≤ val_Zp (f'∙a) ∧ val_Zp (f'∙a) ≠ ∞"
using f'a_closed val_ord_Zp val_pos by force
have 1: "1 < eint 2 "
by (simp add: one_eint_def)
thus ?thesis using 0 eint_mult_mono'[of "val_Zp (f'∙a)" 1 2] hensel_hypothesis
by (metis linorder_not_less mult_one_left order_trans)
qed
subsection‹Constructing the Newton Sequence›
definition newton_step :: "padic_int ⇒ padic_int" where
"newton_step x = x ⊖ (divide (f∙x) (f'∙x))"
lemma newton_step_closed:
"newton_step a ∈ carrier Zp"
using divide_closed unfolding newton_step_def
using f'a_closed f'a_nonzero fa_closed local.a_closed by blast
fun newton_seq :: "padic_int_seq" ("ns") where
"newton_seq 0 = a"|
"newton_seq (Suc n) = newton_step (newton_seq n)"
subsection‹Key Properties of the Newton Sequence›
lemma hensel_factor_id:
"(divide (f∙a) (f'∙a)) ⊗ ((f'∙a)) = (f∙a)"
using hensel_hypothesis hensel_axioms divide_formula f'a_closed
fa_closed hensel_hypothesis_weakened mult_comm
by auto
definition hensel_factor ("t") where
"hensel_factor = val_Zp (f∙a) - 2*(val_Zp (f'∙a))"
lemma t_pos[simp]:
"t > 0"
using hensel_factor_def hensel_hypothesis
by (simp add: eint_minus_le)
lemma t_neq_infty[simp]:
"t ≠ ∞"
by (simp add: hensel_factor_def val_Zp_def)
lemma t_times_pow_pos[simp]:
"(2^(n::nat))*t > 0"
apply(cases "n = 0")
using one_eint_def apply auto[1]
using eint_mult_mono'[of t 1 "2^n"] t_pos
by (smt (verit) eint_ord_simps(2) linorder_not_less mult_one_left neq0_conv one_eint_def order_less_le order_trans self_le_power t_neq_infty)
lemma newton_seq_props_induct:
shows "⋀k. k ≤ n ⟹ (ns k) ∈ carrier Zp
∧ val_Zp (f'∙(ns k)) = val_Zp ((f'∙a))
∧ val_Zp (f∙(ns k)) ≥ 2*(val_Zp (f'∙a)) + (2^k)*t"
proof(induction n)
case 0
then have kz: "k = 0"
by simp
have B0: "( ns k) ∈ carrier Zp"
using kz
by simp
have B1: "val_Zp (f' ∙ ns k) = (val_Zp (f'∙a))"
using kz newton_seq.simps(1)
by presburger
have B2: "val_Zp (f ∙ (ns k)) ≥ (2 * (val_Zp (f'∙a))) + 2 ^ k * t"
proof-
have B20: "(2 * (val_Zp (f'∙a))) + 2 ^ k * t = (2 * (val_Zp (f'∙a))) + t"
proof-
have "(2 * (val_Zp (f'∙a))) + 2 ^ k * t = (2 * (val_Zp (f'∙a))) + t"
using kz one_eint_def by auto
then show ?thesis
by blast
qed
then have "(2 * (val_Zp (f'∙a))) + 2 ^ k * t = (2 * (val_Zp (f'∙a))) + val_Zp (f∙a) - 2*(val_Zp (f'∙a))"
unfolding hensel_factor_def
by (simp add: val_Zp_def)
then have "(2 * (val_Zp (f'∙a))) + 2 ^ k * t = val_Zp (f∙a)"
by (metis add_diff_cancel_eint eint_ord_simps(6) hensel_hypothesis)
thus ?thesis by (simp add: kz)
qed
thus ?case
using B0 B1 by blast
next
case (Suc n)
show ?case
proof(cases "k ≤ n")
case True
then show ?thesis using Suc.IH
by blast
next
case False
have F1: "(ns n) ∈ carrier Zp"
using Suc.IH by blast
have F2: "val_Zp (f'∙(ns n)) = val_Zp ((f'∙a))"
using Suc.IH by blast
have F3: "val_Zp (f∙(ns n)) ≥ 2*(val_Zp (f'∙a)) + (2^n)*t"
using Suc.IH by blast
have kval: "k = Suc n"
using False Suc.prems le_Suc_eq by blast
have F6: "val_Zp (f∙(ns n)) ≥ val_Zp (f'∙(ns n))"
proof-
have "2*(val_Zp (f'∙a)) ≥ val_Zp (f'∙a)"
using f'a_closed val_pos eint_mult_mono'[of "val_Zp (f'∙a)" 1 2]
by (metis Groups.add_ac(2) add.right_neutral eSuc_eint eint_0_iff(2) eint_add_left_cancel_le
eint_ord_simps(2) f'a_nonneg_val f'a_not_infinite infinity_ne_i1 linorder_not_less
mult_one_left not_one_less_zero one_add_one one_eint_def order_less_le order_trans zero_one_eint_neq(1))
hence "2*(val_Zp (f'∙a)) + (2^n)*t ≥ val_Zp (f'∙a)"
using t_times_pow_pos[of n]
by (metis (no_types, lifting) add.right_neutral eint_add_left_cancel_le order_less_le order_trans)
then show ?thesis
using F2 F3 by auto
qed
have F5: " divide (f∙(ns n))(f'∙(ns n)) ∈ carrier Zp"
proof-
have 00: "f ∙ ns n ∈ carrier Zp"
by (simp add: F1 to_fun_closed)
have "val_Zp ((f'∙a)) ≠ val_Zp 𝟬"
by (simp add: val_Zp_def)
then have 01: "f' ∙ ns n ∈ nonzero Zp"
using F2 F1 Zp_x_is_UP_cring f'_closed nonzero_def
proof -
have "f' ∙ ns n ∈ carrier Zp"
using F1 Zp_continuous_is_Zp_closed f'_closed polynomial_is_Zp_continuous
by (simp add: to_fun_closed)
then show ?thesis
using F2 ‹val_Zp (f'∙a) ≠ val_Zp 𝟬› not_nonzero_Zp by fastforce
qed
then show ?thesis
using F6
by (metis "00" F2 ‹val_Zp (f'∙a) ≠ val_Zp 𝟬› divide_closed nonzero_closed)
qed
have F4: "(ns k) ⊖ (ns n) = (⊖ divide (f∙(ns n))(f'∙(ns n)))"
using F1 F5 newton_seq.simps(2)[of n] kval
unfolding newton_step_def
by (metis R.l_neg R.minus_closed R.minus_zero R.plus_diff_simp R.r_neg2 R.r_right_minus_eq
a_minus_def local.a_closed minus_a_inv)
have F7: "val_Zp (divide (f∙(ns n))(f'∙(ns n))) = val_Zp (f∙(ns n)) - val_Zp (f'∙(ns n))"
apply(rule val_of_divide)
apply (simp add: F1 to_fun_closed)
using F1 f'_closed to_fun_closed F2 not_nonzero_Zp val_Zp_def apply fastforce
by (simp add: F6)
show ?thesis
proof
show P0:"ns k ∈ carrier Zp"
proof-
have A0: "ns k = ns n ⊖ (divide (f∙ (ns n)) (f'∙(ns n)))"
by (simp add: kval newton_step_def)
have A1: "val_Zp (f'∙(ns n)) = val_Zp (f'∙a)"
using Suc.IH
by blast
have A2: "val_Zp (f∙(ns n)) ≥val_Zp (f'∙a)"
proof-
have A20: "(2 * val_Zp (f'∙a)) + 2 ^ n * (val_Zp (f∙a) - 2 * val_Zp (f'∙a)) ≥val_Zp (f'∙a)"
proof-
have "val_Zp (f∙a) - 2 * val_Zp (f'∙a) > 0"
using hensel_hypothesis eint_minus_le by blast
then have " (2 ^ n) * (val_Zp (f∙a) - 2 * val_Zp (f'∙a))
≥ (val_Zp (f∙a) - 2 * val_Zp (f'∙a))"
using eint_pos_int_times_ge by auto
then have " ((2 * val_Zp (f'∙a)) + 2 ^ n * (val_Zp (f∙a) - 2 * val_Zp (f'∙a)))
≥ (2 * val_Zp (f'∙a)) + (val_Zp (f∙a) - 2 * val_Zp (f'∙a))"
by (simp add: val_Zp_def)
then have " ((2 * val_Zp (f'∙a)) + 2 ^ n * (val_Zp (f∙a) - 2 * val_Zp (f'∙a)))
≥ (val_Zp (f∙a) )"
by simp
then show " ((2 * val_Zp (f'∙a)) + 2 ^ n * (val_Zp (f∙a) - 2 * val_Zp (f'∙a)))
≥ (val_Zp (f'∙a) )"
using hensel_hypothesis_weakened by auto
qed
have A21:"val_Zp (f∙(ns n)) ≥ (2 * val_Zp (f'∙a)) + 2 ^ n * (val_Zp (f∙a) - 2 * val_Zp (f'∙a))"
using Suc.IH unfolding hensel_factor_def
by blast
show ?thesis using A21 A20
by auto
qed
have A3: "ns n ∈ carrier Zp"
using Suc.IH by blast
have A4: "val_Zp (f∙(ns n)) ≥val_Zp (f'∙(ns n))"
using A1 A2
by presburger
have A5: "f∙(ns n) ∈ carrier Zp"
by (simp add: F1 UP_cring.to_fun_closed Zp_x_is_UP_cring)
have A6: "(f'∙(ns n)) ∈ nonzero Zp"
proof-
have "(f'∙(ns n)) ∈ carrier Zp"
by (simp add: F1 UP_cring.to_fun_closed Zp_x_is_UP_cring f'_closed)
have "val_Zp (f'∙(ns n)) ≠ ∞"
using A1
by (simp add: val_Zp_def)
then show ?thesis
using ‹f' ∙ ns n ∈ carrier Zp› not_nonzero_Zp val_Zp_def
by meson
qed
have A7: " (divide (f∙ (ns n)) (f'∙(ns n))) ∈ carrier Zp"
using A5 A6 A4 A3 F5 by linarith
then show ?thesis
using A0 A3 cring.cring_simprules(4)
by (simp add: F1 F5 cring.cring_simprules(4))
qed
have P1: "val_Zp (f' ∙ ns k) = val_Zp (f'∙a) "
proof(cases "(f' ∙ ns k) = (f' ∙ ns n)")
case True
then show ?thesis using Suc.IH
by (metis order_refl)
next
case False
have "val_Zp ((f' ∙ ns k) ⊖ (f' ∙ ns n)) ≥ val_Zp ((ns k) ⊖ (ns n))"
using False P0 f'_closed poly_diff_val Suc.IH
by blast
then have "val_Zp ((f' ∙ ns k) ⊖ (f' ∙ ns n)) ≥ val_Zp (⊖ divide (f∙(ns n))(f'∙(ns n)))"
using F4 by argo
then have "val_Zp ((f' ∙ ns k) ⊖ (f' ∙ ns n)) ≥ val_Zp (divide (f∙(ns n))(f'∙(ns n)))"
using F5 val_Zp_of_minus
by presburger
then have P10: "val_Zp ((f' ∙ ns k) ⊖ (f' ∙ ns n)) ≥ val_Zp (f∙(ns n)) - val_Zp (f'∙(ns n))"
using F7 by metis
have P11: "val_Zp (f'∙(ns n)) ≠ ∞"
by (simp add: F2)
then have "val_Zp ((f' ∙ ns k) ⊖ (f' ∙ ns n)) ≥ (2 * val_Zp (f'∙a)) + 2 ^ n * t - val_Zp (f'∙(ns n))"
using F3 P10
by (smt (verit) eint_add_cancel_fact eint_add_left_cancel_le order_trans)
then have P12: "val_Zp ((f' ∙ ns k) ⊖ (f' ∙ ns n)) ≥ (2 *(val_Zp (f'∙a))) + 2 ^ n * t - (val_Zp (f'∙a))"
by (simp add: F2)
have P13:"val_Zp ((f' ∙ ns k) ⊖ (f' ∙ ns n)) ≥ (val_Zp (f'∙a)) + 2 ^ n * t "
proof-
have "(2 *(val_Zp (f'∙a))) + (2 ^ n * t) - (val_Zp (f'∙a)) = (2 *(val_Zp (f'∙a))) - (val_Zp (f'∙a)) + (2 ^ n * t) "
using eint_minus_comm by blast
then show ?thesis using P12
using f'a_not_infinite by force
qed
then have P14: "val_Zp ((f' ∙ ns k) ⊖ (f' ∙ ns n)) > (val_Zp (f'∙a))"
using f'a_not_infinite ge_plus_pos_imp_gt t_times_pow_pos by blast
show ?thesis
by (meson F1 F2 P0 P14 equal_val_Zp f'_closed f'a_closed to_fun_closed)
qed
have P2: "val_Zp (f∙(ns k)) ≥ 2*(val_Zp (f'∙a)) + (2^k)*t"
proof-
have P23: "2 * (val_Zp (f'∙a)) + ((2 ^ k) * t) ≤ val_Zp (f ∙ ns k)"
proof-
have 0: "ns n ∈ carrier Zp"
by (simp add: F1)
have 1: "local.divide (f ∙ ns n) (f' ∙ ns n) ∈ carrier Zp"
using F5 by blast
have 2: "(poly_shift_iter 2 (taylor (ns n) f)) ∙ ⊖ local.divide (f ∙ ns n) (f' ∙ ns n) ∈ carrier Zp"
using F1 F5 shift_closed 1
by (simp add: taylor_closed to_fun_closed)
have 3: "divide (f ∙ ns n) (f' ∙ ns n) ⊗ deriv f (ns n) = f ∙ ns n"
by (metis F1 F2 F6 divide_formula f'_closed f'a_not_infinite f_closed mult_comm pderiv_eval_deriv to_fun_closed val_Zp_def)
have 4: "f ∈ carrier Zp_x"
by simp
obtain c where c_def: "c = poly_shift_iter (2::nat) (taylor (ns n) f) ∙ ⊖ local.divide (f ∙ ns n) (f' ∙ ns n)"
by blast
then have c_def': "c ∈ carrier Zp ∧ f ∙ (ns n ⊖ local.divide (f ∙ ns n) (f' ∙ ns n)) = c ⊗ local.divide (f ∙ ns n) (f' ∙ ns n) [^] (2::nat)"
using 0 1 2 3 4 UP_cring.taylor_deg_1_eval'''[of Zp f "ns n" "(divide (f∙(ns n)) (f'∙(ns n)))" c]
Zp_x_is_UP_cring
by blast
have P230: "f∙(ns k) = (c ⊗ (divide (f∙(ns n)) (f'∙(ns n)))[^](2::nat))"
using c_def'
by (simp add: kval newton_step_def)
have P231: "val_Zp (f∙(ns k)) = val_Zp c + 2*(val_Zp (f∙(ns n)) - val_Zp(f'∙(ns n)))"
proof-
have P2310: "val_Zp (f∙(ns k)) = val_Zp c + val_Zp ((divide (f∙(ns n)) (f'∙(ns n)))[^](2::nat))"
by (simp add: F5 P230 c_def' val_Zp_mult)
have P2311: "val_Zp ((divide (f∙(ns n)) (f'∙(ns n)))[^](2::nat))
= 2*(val_Zp (f∙(ns n)) - val_Zp(f'∙(ns n)))"
by (metis F5 F7 R.pow_zero mult.commute not_nonzero_Zp of_nat_numeral times_eint_simps(3) val_Zp_def val_Zp_pow' zero_less_numeral)
thus ?thesis
by (simp add: P2310)
qed
have P232: "val_Zp (f∙(ns k)) ≥ 2*(val_Zp (f∙(ns n)) - val_Zp(f'∙(ns n)))"
by (simp add: P231 c_def' val_pos)
have P236: "val_Zp (f∙(ns k)) ≥ 2*(2 *val_Zp (f'∙a) + 2 ^ n * t) - 2* val_Zp(f'∙(ns n))"
using P232 F3 eint_minus_ineq''[of "val_Zp(f'∙(ns n))" "(2 *val_Zp (f'∙a)) + 2 ^ n * t" "val_Zp (f∙(ns n))" 2 ]
F2 eint_pow_int_is_pos by auto
hence P237: "val_Zp (f∙(ns k)) ≥(4*val_Zp (f'∙a)) + (2*((2 ^ n)* t)) - 2* val_Zp(f'∙(ns n))"
proof-
have "2*(2*val_Zp (f'∙a) + 2 ^ n * t) = (4*val_Zp (f'∙a)) + 2*(2 ^ n)* t "
using distrib_left[of 2 "2*val_Zp (f'∙a)" "2 ^ n * t"] mult.assoc mult_one_right one_eint_def plus_eint_simps(1)
hensel_factor_def val_Zp_def by auto
then show ?thesis
using P236
by (metis mult.assoc)
qed
hence P237: "val_Zp (f∙(ns k)) ≥ 4*val_Zp (f'∙a) + 2*(2 ^ n)* t - 2* val_Zp((f'∙a))"
by (metis F2 mult.assoc)
hence P238: "val_Zp (f∙(ns k)) ≥ 2*val_Zp (f'∙a) + 2*(2 ^ n)* t"
using eint_minus_comm[of "4*val_Zp (f'∙a) " "2*(2 ^ n)* t" "2* val_Zp((f'∙a))"]
by (simp add: eint_int_minus_distr)
thus ?thesis
by (simp add: kval)
qed
thus ?thesis
by blast
qed
show "val_Zp (to_fun f' (ns k)) = val_Zp (f'∙a) ∧
2 * val_Zp (f'∙a) + eint (2 ^ k) * t ≤ val_Zp (to_fun f (ns k))"
using P1 P2 by blast
qed
qed
qed
lemma newton_seq_closed:
shows "ns m ∈ carrier Zp"
using newton_seq_props_induct
by blast
lemma f_of_newton_seq_closed:
shows "f ∙ ns m ∈ carrier Zp"
by (simp add: to_fun_closed newton_seq_closed)
lemma newton_seq_fact1[simp]:
" val_Zp (f'∙(ns k)) = val_Zp ((f'∙a))"
using newton_seq_props_induct by blast
lemma newton_seq_fact2:
"⋀k. val_Zp (f∙(ns k)) ≥ 2*(val_Zp (f'∙a)) + (2^k)*t"
by (meson le_iff_add newton_seq_props_induct)
lemma newton_seq_fact3:
"val_Zp (f∙(ns l)) ≥ val_Zp (f'∙(ns l))"
proof-
have "2*(val_Zp (f'∙a)) + (2^l)*t ≥ (val_Zp (f'∙a))"
using f'a_closed ord_pos t_pos
by (smt (verit) eint_pos_int_times_ge f'a_nonneg_val f'a_not_infinite ge_plus_pos_imp_gt linorder_not_less nat_mult_not_infty order_less_le t_times_pow_pos)
then show "val_Zp (f ∙ ns l) ≥ val_Zp (f' ∙ ns l) "
using f'a_closed f'a_nonzero newton_seq_fact1[of l] newton_seq_fact2[of l] val_Zp_def
proof -
show ?thesis
using ‹eint 2 * val_Zp (f'∙a) + eint (2 ^ l) * t ≤ val_Zp (to_fun f (ns l))› ‹val_Zp (f'∙a) ≤ eint 2 * val_Zp (f'∙a) + eint (2 ^ l) * t› by force
qed
qed
lemma newton_seq_fact4[simp]:
assumes "f∙(ns l) ≠𝟬"
shows "val_Zp (f∙(ns l)) ≥ val_Zp (f'∙(ns l))"
using newton_seq_fact3 by blast
lemma newton_seq_fact5:
"divide (f ∙ ns l) (f' ∙ ns l) ∈ carrier Zp"
apply(rule divide_closed)
apply (simp add: to_fun_closed newton_seq_closed)
apply (simp add: f'_closed to_fun_closed newton_seq_closed)
by (metis f'a_not_infinite newton_seq_fact1 val_Zp_def)
lemma newton_seq_fact6:
"(f'∙(ns l)) ∈ nonzero Zp"
apply(rule ccontr)
using nonzero_memI nonzero_memE
f'a_nonzero newton_seq_fact1 val_Zp_def
by (metis (no_types, lifting) divide_closed f'_closed f'a_closed fa_closed hensel_factor_id
hensel_hypothesis_weakened mult_zero_l newton_seq_closed order_less_le to_fun_closed val_Zp_mult)
lemma newton_seq_fact7:
"(ns (Suc n)) ⊖ (ns n) = ⊖divide (f∙(ns n)) (f'∙(ns n))"
using newton_seq.simps(2)[of n] newton_seq_fact5[of n]
newton_seq_closed[of "Suc n"] newton_seq_closed[of n]
R.ring_simprules
unfolding newton_step_def a_minus_def
by (smt (verit))
lemma newton_seq_fact8:
assumes "f∙(ns l) ≠𝟬"
shows "divide (f ∙ ns l) (f' ∙ ns l) ∈ nonzero Zp"
using assms divide_nonzero[of "f ∙ ns l" "f' ∙ ns l"]
nonzero_memI
using f_of_newton_seq_closed newton_seq_fact3 newton_seq_fact6 by blast
lemma newton_seq_fact9:
assumes "f∙(ns n) ≠𝟬"
shows "val_Zp((ns (Suc n)) ⊖ (ns n)) = val_Zp (f∙(ns n)) - val_Zp (f'∙(ns n))"
using newton_seq_fact7 val_of_divide newton_seq_fact6 assms nonzero_memI
f_of_newton_seq_closed newton_seq_fact4 newton_seq_fact5
by (metis val_Zp_of_minus)
text‹Assuming no element of the Newton sequence is a root of f, the Newton sequence is Cauchy.›
lemma newton_seq_is_Zp_cauchy_0:
assumes "⋀k. f∙(ns k) ≠𝟬"
shows "is_Zp_cauchy ns"
proof(rule is_Zp_cauchyI')
show P0: "ns ∈ closed_seqs Zp"
proof(rule closed_seqs_memI)
show "⋀k. ns k ∈ carrier Zp "
by (simp add: newton_seq_closed)
qed
show "∀n. ∃k. ∀m. k ≤ int m ⟶ int n ≤ val_Zp (ns (Suc m) ⊖ ns m)"
proof
fix n
show "∃k. ∀m. k ≤ int m ⟶ int n ≤ val_Zp (ns (Suc m) ⊖ ns m)"
proof(induction "n")
case 0
have B0: "∀n0 n1. 0 < n0 ∧ 0 < n1 ⟶ ns n0 0 = ns n1 0"
apply auto
proof-
fix n0 n1::nat
assume A: "0 < n0" "0 < n1"
show "ns n0 0 = ns n1 0"
proof-
have 0: "ns n0 ∈ carrier Zp"
using P0
by (simp add: newton_seq_closed)
have 1: "ns n1 ∈ carrier Zp"
using P0
by (simp add: newton_seq_closed)
show ?thesis
using 0 1 Zp_defs(3) prime
by (metis p_res_ring_0' residue_closed)
qed
qed
have "∀m. 1 ≤ int m ⟶ int 0 ≤ val_Zp_dist (newton_step (ns m)) (ns m)"
proof
fix m
show "1 ≤ int m ⟶ int 0 ≤ val_Zp_dist (newton_step (ns m)) (ns m)"
proof
assume "1 ≤ int m "
then have C0:"ns (Suc m) 0 = ns m 0"
using B0
by (metis int_one_le_iff_zero_less int_ops(1) less_Suc_eq_0_disj of_nat_less_iff)
then show "int 0 ≤ val_Zp_dist (newton_step (ns m)) (ns m)"
proof-
have "(newton_step (ns m)) ≠(ns m)"
proof-
have A0: "divide (f∙(ns m)) (f'∙(ns m)) ≠𝟬"
proof-
have 0: "(f∙(ns m)) ≠ 𝟬"
using assms by auto
have 1: " (f'∙(ns m)) ∈ carrier Zp"
by (simp add: UP_cring.to_fun_closed Zp_x_is_UP_cring f'_closed newton_seq_closed)
have 2: "(f'∙(ns m)) ≠ 𝟬"
using newton_seq_fact6 not_nonzero_memI by blast
show ?thesis using 0 1 2
by (metis R.r_null divide_formula f_closed to_fun_closed newton_seq_closed newton_seq_fact4)
qed
have A2: "local.divide (f ∙ ns m) (f' ∙ ns m) ∈ carrier Zp"
using newton_seq_fact5 by blast
have A3: "ns m ∈ carrier Zp"
by (simp add: newton_seq_closed)
have A4: "newton_step (ns m) ∈ carrier Zp"
by (metis newton_seq.simps(2) newton_seq_closed)
show ?thesis
apply(rule ccontr)
using A4 A3 A2 A0 newton_step_def[of "(ns m)"]
by (simp add: a_minus_def)
qed
then show ?thesis using C0
by (metis newton_seq.simps(2) newton_seq_closed val_Zp_dist_res_eq2)
qed
qed
qed
then show ?case
using val_Zp_def val_Zp_dist_def
by (metis int_ops(1) newton_seq.simps(2) zero_eint_def)
next
case (Suc n)
show "∃k. ∀m. k ≤ int m ⟶ int (Suc n) ≤ val_Zp (ns (Suc m) ⊖ ns m)"
proof-
obtain k0 where k0_def: "k0 ≥0 ∧ (∀m. k0 ≤ int m ⟶ int n ≤ val_Zp (ns (Suc m) ⊖ ns m))"
using Suc.IH
by (metis int_nat_eq le0 nat_le_iff of_nat_0_eq_iff )
have I0: "⋀l. val_Zp (ns (Suc l) ⊖ ns l) = val_Zp (f∙ (ns l)) - val_Zp (f'∙(ns l))"
proof-
fix l
have I00:"(ns (Suc l) ⊖ ns l) = (⊖ divide (f∙(ns l)) (f'∙(ns l)))"
proof-
have "local.divide (f ∙ ns l) (f' ∙ ns l) ∈ carrier Zp"
by (simp add: newton_seq_fact5)
then show ?thesis
using newton_seq.simps(2)[of l] newton_seq_closed R.ring_simprules
unfolding newton_step_def a_minus_def
by (metis add_comm)
qed
have I01: "val_Zp (ns (Suc l) ⊖ ns l) = val_Zp (divide (f∙(ns l)) (f'∙(ns l)))"
proof-
have I010: "(divide (f∙(ns l)) (f'∙(ns l))) ∈carrier Zp"
by (simp add: newton_seq_fact5)
have I011: "(divide (f∙(ns l)) (f'∙(ns l))) ≠ 𝟬"
proof-
have A: "(f∙(ns l)) ≠𝟬"
by (simp add: assms)
have B: " (f'∙(ns l)) ∈carrier Zp"
using nonzero_memE newton_seq_fact6 by auto
then have C: " (f'∙(ns l)) ∈nonzero Zp"
using f'a_closed fa_closed fa_nonzero hensel_factor_id hensel_hypothesis_weakened
newton_seq_fact1[of l] not_nonzero_Zp val_Zp_def
by fastforce
then show ?thesis using I010 A
by (metis B R.r_null divide_formula f_closed to_fun_closed newton_seq_closed newton_seq_fact4 nonzero_memE(2))
qed
then have "val_Zp (divide (f∙(ns l)) (f'∙(ns l)))
= val_Zp (⊖ divide (f∙(ns l)) (f'∙(ns l)))"
using I010 not_nonzero_Zp val_Zp_of_minus by blast
then show ?thesis using I00 by metis
qed
have I02: "val_Zp (f∙(ns l)) ≥ val_Zp (f'∙(ns l))"
using assms newton_seq_fact4
by blast
have I03: "(f∙(ns l)) ∈ nonzero Zp"
by (meson UP_cring.to_fun_closed Zp_x_is_UP_cring assms f_closed newton_seq_closed not_nonzero_Zp)
have I04: "f'∙(ns l) ∈ nonzero Zp"
by (simp add: newton_seq_fact6)
have I05 :" val_Zp (divide (f∙(ns l)) (f'∙(ns l))) = val_Zp (f∙ (ns l)) - val_Zp (f'∙(ns l))"
using I02 I03 I04 I01 assms newton_seq_fact9 by auto
then show " val_Zp (ns (Suc l) ⊖ ns l) = val_Zp (f∙ (ns l)) - val_Zp (f'∙(ns l))"
using I01 by simp
qed
have "∀m. int(Suc n) + k0 + 1 ≤ int m ⟶ int (Suc n) ≤ val_Zp_dist (newton_step (ns m)) (ns m)"
proof
fix m
show "int (Suc n) + k0 + 1 ≤ int m ⟶ int (Suc n) ≤ val_Zp_dist (newton_step (ns m)) (ns m)"
proof
assume A: "int (Suc n) + k0 + 1 ≤ int m "
show " int (Suc n) ≤ val_Zp_dist (newton_step (ns m)) (ns m)"
proof-
have 0: " val_Zp_dist (newton_step (ns m)) (ns m) = val_Zp (f∙ (ns m)) - val_Zp (f'∙(ns m))"
using I0 val_Zp_dist_def by auto
have 1: "val_Zp (f∙ (ns m)) - val_Zp (f'∙(ns m)) > int n"
proof-
have "val_Zp (f∙ (ns m)) ≥ 2*(val_Zp (f'∙a)) + (2^m)*t"
by (simp add: newton_seq_fact2)
then have 10:"val_Zp (f∙ (ns m)) - val_Zp (f'∙(ns m)) ≥ 2*(val_Zp (f'∙a)) + (2^m)*t - val_Zp (f'∙(ns m))"
by (simp add: eint_minus_ineq)
have "2^m * t > m"
apply(induction m)
using one_eint_def zero_eint_def apply auto[1]
proof- fix m
assume IH : "int m < 2 ^ m * t "
then have "((2 ^ (Suc m)) * t) = 2* ((2 ^ m) * t)"
by (metis mult.assoc power_Suc times_eint_simps(1))
then show "int (Suc m) < 2 ^ Suc m * t"
using IH t_neq_infty by force
qed
then have 100: "2^m * t > int m"
by blast
have "int m ≥2 + (int n + k0)"
using A by simp
hence 1000: "2^m * t > 2 + (int n + k0)"
using 100
by (meson eint_ord_simps(2) less_le_trans linorder_not_less)
have "2 + (int n + k0) > 1 + int n"
using k0_def by linarith
then have "2^m * t > 1 + int n"
using 1000 eint_ord_simps(2) k0_def less_le_trans linorder_not_less
proof -
have "eint (2 + (int n + k0)) < t * eint (int (2 ^ m))"
by (metis "1000" mult.commute numeral_power_eq_of_nat_cancel_iff)
then have "eint (int (Suc n)) < t * eint (int (2 ^ m))"
by (metis ‹1 + int n < 2 + (int n + k0)› eint_ord_simps(2) less_trans of_nat_Suc)
then show ?thesis
by (simp add: mult.commute)
qed
hence "2*val_Zp (f'∙a) + eint (2 ^ m) * t ≥ 2*(val_Zp (f'∙a)) + 1 + int n"
by (smt (verit) eSuc_eint eint_add_left_cancel_le iadd_Suc iadd_Suc_right order_less_le)
then have 11: "val_Zp (f∙ (ns m)) - val_Zp (f'∙(ns m))
≥ 2*(val_Zp (f'∙a)) + 1 + int n - val_Zp (f'∙(ns m))"
using "10"
by (smt (verit) ‹eint 2 * val_Zp (f'∙a) + eint (2 ^ m) * t ≤ val_Zp (to_fun f (ns m))›
f'a_not_infinite eint_minus_ineq hensel_axioms newton_seq_fact1 order_trans)
have 12: "val_Zp (f'∙(ns m)) = val_Zp (f'∙a) "
using nonzero_memE newton_seq_fact1 newton_seq_fact6 val_Zp_def val_Zp_def
by auto
then have 13: "val_Zp (f∙ (ns m)) - val_Zp (f'∙(ns m))
≥ 2*(val_Zp (f'∙a)) + (1 + int n) - val_Zp ((f'∙a))"
using 11
by (metis eint_1_iff(1) group_cancel.add1 plus_eint_simps(1))
then have 14:"val_Zp (f∙ (ns m)) - val_Zp (f'∙(ns m))
≥ 1 + int n + val_Zp ((f'∙a))"
using eint_minus_comm[of "2*(val_Zp (f'∙a))" "1 + int n" "val_Zp ((f'∙a))"]
by (simp add: Groups.add_ac(2))
then show ?thesis
by (smt (verit) Suc_ile_eq add.right_neutral eint.distinct(2) f'a_nonneg_val ge_plus_pos_imp_gt order_less_le)
qed
then show ?thesis
by (smt (verit) "0" Suc_ile_eq of_nat_Suc)
qed
qed
qed
then show ?thesis
using val_Zp_def val_Zp_dist_def
by (metis newton_seq.simps(2))
qed
qed
qed
qed
lemma eventually_zero:
"f ∙ ns (k + m) = 𝟬 ⟹ f ∙ ns (k + Suc m) = 𝟬"
proof-
assume A: "f ∙ ns (k + m) = 𝟬"
have 0: "ns (k + Suc m) = ns (k + m) ⊖ (divide (f ∙ ns (k + m)) (f' ∙ ns (k + m)))"
by (simp add: newton_step_def)
have 1: "(divide (f ∙ ns (k + m)) (f' ∙ ns (k + m))) = 𝟬"
by (simp add: A divide_def)
show "f ∙ ns (k + Suc m) = 𝟬"
using A 0 1
by (simp add: a_minus_def newton_seq_closed)
qed
text‹The Newton Sequence is Cauchy:›
lemma newton_seq_is_Zp_cauchy:
"is_Zp_cauchy ns"
proof(cases "∀k. f∙(ns k) ≠𝟬")
case True
then show ?thesis using newton_seq_is_Zp_cauchy_0
by blast
next
case False
obtain k where k_def:"f∙(ns k) = 𝟬"
using False by blast
have 0: "⋀m. (ns (m + k)) = (ns k)"
proof-
fix m
show "(ns (m + k)) = (ns k)"
proof(induction m)
case 0
then show ?case
by simp
next
case (Suc m)
show "(ns (Suc m + k)) = (ns k)"
proof-
have "f ∙ ns (m + k) = 𝟬"
by (simp add: Suc.IH k_def)
then have "divide ( f ∙ ns (m + k)) (f' ∙ ns (m + k)) = 𝟬"
by (simp add: divide_def)
then show ?thesis using newton_step_def
by (simp add: Suc.IH a_minus_def newton_seq_closed)
qed
qed
qed
show "is_Zp_cauchy ns"
apply(rule is_Zp_cauchyI)
apply (simp add: closed_seqs_memI newton_seq_closed)
proof-
show "⋀n.⋀n. ∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ ns n0 n = ns n1 n"
proof-
fix n
show "∃N. ∀n0 n1. N < n0 ∧ N < n1 ⟶ ns n0 n = ns n1 n"
proof-
have "∀n0 n1. k < n0 ∧ k < n1 ⟶ ns n0 n = ns n1 n"
apply auto
proof-
fix n0 n1
assume A0: "k < n0"
assume A1: "k < n1"
obtain m0 where m0_def: "n0 = k + m0"
using A0 less_imp_add_positive by blast
obtain m1 where m1_def: "n1 = k + m1"
using A1 less_imp_add_positive by auto
show "ns n0 n = ns n1 n"
using 0 m0_def m1_def
by (metis add.commute)
qed
then show ?thesis by blast
qed
qed
qed
qed
subsection‹The Proof of Hensel's Lemma›
lemma pre_hensel:
"val_Zp (a ⊖ (ns n)) > val_Zp (f'∙a)"
"∃N. ∀n. n> N ⟶ (val_Zp (a ⊖ (ns n)) = val_Zp (divide (f∙a) (f'∙a)))"
"val_Zp (f'∙(ns n)) = val_Zp (f'∙a)"
proof-
show "val_Zp (a ⊖ (ns n)) > val_Zp (f'∙a)"
proof(induction n)
case 0
then show ?case
by (simp add: val_Zp_def)
next
case (Suc n)
show "val_Zp (a ⊖ (ns (Suc n))) > val_Zp (f'∙a)"
proof-
have I0: "val_Zp ((ns (Suc n)) ⊖ (ns n)) > val_Zp (f'∙a)"
proof(cases "(ns (Suc n)) = (ns n)")
case True
then show ?thesis
by (simp add: newton_seq_closed val_Zp_def)
next
case False
have 00:"(ns (Suc n)) ⊖ (ns n) = ⊖divide (f∙(ns n)) (f'∙(ns n))"
using newton_seq_fact7 by blast
then have 0: "val_Zp((ns (Suc n)) ⊖ (ns n)) = val_Zp (divide (f∙(ns n)) (f'∙(ns n)))"
using newton_seq_fact5 val_Zp_of_minus by presburger
have 1: "(f∙(ns n)) ∈ nonzero Zp"
by (metis False R.minus_zero R.r_right_minus_eq 00 divide_def f_closed to_fun_closed
newton_seq_closed not_nonzero_Zp)
have 2: "f'∙(ns n) ∈ nonzero Zp"
by (simp add: newton_seq_fact6)
have "val_Zp (f∙(ns n)) ≥ val_Zp (f'∙(ns n))"
using nonzero_memE ‹f ∙ ns n ∈ nonzero Zp› newton_seq_fact4 by blast
then have 3:"val_Zp((ns (Suc n)) ⊖ (ns n)) = val_Zp (f∙(ns n)) - val_Zp (f'∙(ns n))"
using 0 1 2 newton_seq_fact9 nonzero_memE(2) by blast
have 4: "val_Zp (f ∙ ns n) ≥ (2 * val_Zp (f'∙a)) + 2 ^ n * t"
using newton_seq_fact2[of n] by metis
then have 5: "val_Zp((ns (Suc n)) ⊖ (ns n)) ≥ ((2 * val_Zp (f'∙a)) + 2 ^ n * t) - val_Zp (f'∙(ns n))"
using "3" eint_minus_ineq f'a_not_infinite newton_seq_fact1 by presburger
have 6: "((ns (Suc n)) ⊖ (ns n)) ∈ nonzero Zp"
using False not_eq_diff_nonzero newton_seq_closed by blast
then have "val_Zp((ns (Suc n)) ⊖ (ns n)) ≥ (2 * val_Zp (f'∙a)) + 2 ^ n * t - val_Zp ((f'∙a))"
using "5" by auto
then have 7: "val_Zp((ns (Suc n)) ⊖ (ns n)) ≥ (val_Zp (f'∙a)) + 2 ^ n * t"
by (simp add: eint_minus_comm)
then show "val_Zp((ns (Suc n)) ⊖ (ns n)) > (val_Zp (f'∙a))"
using f'a_not_infinite ge_plus_pos_imp_gt t_times_pow_pos by blast
qed
have "val_Zp ((ns (Suc n)) ⊖ (ns n)) = val_Zp ((ns n) ⊖ (ns (Suc n)))"
using newton_seq_closed[of "n"] newton_seq_closed[of "Suc n"]
val_Zp_def val_Zp_dist_def val_Zp_dist_sym val_Zp_def
by auto
then have I1: "val_Zp ((ns n) ⊖ (ns (Suc n))) > val_Zp (f'∙a)"
using I0
by presburger
have I2: " (a ⊖ (ns n)) ⊕ ((ns n) ⊖ (ns (Suc n))) = (a ⊖ (ns (Suc n)))"
by (metis R.plus_diff_simp add_comm local.a_closed newton_seq_closed)
then have "val_Zp (a ⊖ (ns (Suc n))) ≥ min (val_Zp (a ⊖ ns n)) (val_Zp (ns n ⊖ ns (Suc n)))"
by (metis R.minus_closed local.a_closed newton_seq_closed val_Zp_ultrametric)
thus ?thesis
using I1 Suc.IH eint_min_ineq by blast
qed
qed
show "val_Zp (f'∙(ns n)) = val_Zp (f'∙a)"
using newton_seq_fact1 by blast
show "∃N.∀n. n> N ⟶ (val_Zp (a ⊖ (ns n)) = val_Zp (divide (f∙a) (f'∙a)))"
proof-
have P: "⋀m. m > 1 ⟹ (val_Zp (a ⊖ (ns m)) = val_Zp (divide (f∙a) (f'∙a)))"
proof-
fix n::nat
assume AA: "n >1"
show " (val_Zp (a ⊖ (ns n)) = val_Zp (divide (f∙a) (f'∙a)))"
proof(cases "(ns 1) = a")
case True
have T0: "⋀k. ∀n. n ≤ k ⟶ ns n = a"
proof-
fix k
show " ∀n. n ≤ k ⟶ ns n = a"
proof(induction k)
case 0
then show ?case
by simp
next
case (Suc k)
show "∀n≤Suc k. ns n = a" apply auto
proof-
fix n
assume A: "n ≤Suc k"
show "ns n = a"
proof(cases "n < Suc k")
case True
then show ?thesis using Suc.IH by auto
next
case False thus ?thesis
using A Suc.IH True by auto
qed
qed
qed
qed
show "val_Zp (a ⊖ ns n) = val_Zp (local.divide (f∙a) (f'∙a))"
by (metis T0 Zp_def Zp_defs(3) f'a_closed f'a_nonzero fa_nonzero
hensel.fa_closed hensel_axioms hensel_hypothesis_weakened le_eq_less_or_eq
newton_seq_fact9 not_nonzero_Qp order_less_le val_of_divide)
next
case False
have F0: "(1::nat) ≤ n"
using AA by simp
have "(f∙a) ≠ 𝟬"
by simp
have "⋀k. val_Zp (a ⊖ ns (Suc k)) = val_Zp (local.divide (f∙a) (f'∙a))"
proof-
fix k
show " val_Zp (a ⊖ ns (Suc k)) = val_Zp (local.divide (f∙a) (f'∙a))"
proof(induction k)
case 0
have "(a ⊖ ns (Suc 0)) = (local.divide (f∙a) (f'∙a))"
by (metis R.minus_minus Zp_def hensel.newton_seq_fact7 hensel_axioms
local.a_closed minus_a_inv newton_seq.simps(1) newton_seq.simps(2) newton_seq_fact5 newton_step_closed)
then show ?case by simp
next
case (Suc k)
have I0: "ns (Suc (Suc k)) = ns (Suc k) ⊖ (divide (f∙(ns (Suc k))) (f'∙(ns (Suc k))))"
by (simp add: newton_step_def)
have I1: "val_Zp (f∙(ns (Suc k))) ≥ val_Zp(f'∙(ns (Suc k)))"
using newton_seq_fact3 by blast
have I2: "(divide (f∙(ns (Suc k))) (f'∙(ns (Suc k)))) ∈ carrier Zp"
using newton_seq_fact5 by blast
have I3: "ns (Suc (Suc k)) ⊖ ns (Suc k) = ⊖(divide (f∙(ns (Suc k))) (f'∙(ns (Suc k))))"
using I0 I2 newton_seq_fact7 by blast
then have "val_Zp (ns (Suc (Suc k)) ⊖ ns (Suc k)) = val_Zp (divide (f∙(ns (Suc k))) (f'∙(ns (Suc k))))"
using I2 val_Zp_of_minus
by presburger
then have "val_Zp (ns (Suc (Suc k)) ⊖ ns (Suc k)) = val_Zp (f∙(ns (Suc k))) - val_Zp (f'∙(ns (Suc k)))"
by (metis I1 R.zero_closed Zp_def newton_seq_fact6 newton_seq_fact9 padic_integers.val_of_divide padic_integers_axioms)
then have I4: "val_Zp (ns (Suc (Suc k)) ⊖ ns (Suc k)) = val_Zp (f∙(ns (Suc k))) - val_Zp ((f'∙a))"
using newton_seq_fact1 by presburger
have F3: "val_Zp (a ⊖ ns (Suc k)) = val_Zp (local.divide (f∙a) (f'∙a))"
using Suc.IH by blast
have F4: "a ⊖ ns (Suc (Suc k)) = (a ⊖ ( ns (Suc k))) ⊕ (ns (Suc k)) ⊖ ns (Suc (Suc k))"
by (metis R.ring_simprules(17) a_minus_def add_comm local.a_closed newton_seq_closed)
have F5: "val_Zp ((ns (Suc k)) ⊖ ns (Suc (Suc k))) > val_Zp (a ⊖ ( ns (Suc k)))"
proof-
have F50: "val_Zp ((ns (Suc k)) ⊖ ns (Suc (Suc k))) = val_Zp (f∙(ns (Suc k))) - val_Zp ((f'∙a))"
by (metis I4 R.minus_closed minus_a_inv newton_seq_closed val_Zp_of_minus)
have F51: "val_Zp (f∙(ns (Suc k))) > val_Zp ((f∙a))"
proof-
have F510: "val_Zp (f∙(ns (Suc k))) ≥ 2*val_Zp (f'∙a) + 2^(Suc k)*t "
using newton_seq_fact2 by blast
hence F511: "val_Zp (f∙(ns (Suc k))) ≥ 2*val_Zp (f'∙a) + 2*t "
using eint_plus_times[of t "2*val_Zp (f'∙a)" "2^(Suc k)" "val_Zp (f∙(ns (Suc k)))" 2] t_pos
by (simp add: order_less_le)
have F512: "2*val_Zp (f'∙a) + 2*t = 2 *val_Zp (f∙a) - 2* val_Zp (f'∙a)"
unfolding hensel_factor_def
using eint_minus_distr[of "val_Zp (f∙a)" "2 * val_Zp (f'∙a)" 2]
eint_minus_comm[of _ _ "eint 2 * (eint 2 * val_Zp (f'∙a))"]
by (smt (verit) eint_2_minus_1_mult eint_add_cancel_fact eint_minus_comm f'a_not_infinite hensel_hypothesis nat_mult_not_infty order_less_le)
hence "2*val_Zp (f'∙a) + 2*t > val_Zp (f∙a)"
using hensel_hypothesis
by (smt (verit) add_diff_cancel_eint eint_add_cancel_fact eint_add_left_cancel_le
eint_pos_int_times_gt f'a_not_infinite hensel_factor_def nat_mult_not_infty order_less_le t_neq_infty t_pos)
thus ?thesis using F512
using F511 less_le_trans by blast
qed
thus ?thesis
by (metis F3 F50 Zp_def divide_closed eint_add_cancel_fact eint_minus_ineq
f'a_closed f'a_nonzero f'a_not_infinite fa_closed fa_nonzero hensel.newton_seq_fact7
hensel_axioms newton_seq.simps(1) newton_seq_fact9 order_less_le val_Zp_of_minus)
qed
have "a ⊖ ns (Suc k) ⊕ (ns (Suc k) ⊖ ns (Suc (Suc k))) = a ⊖ ns (Suc (Suc k))"
by (metis F4 a_minus_def add_assoc)
then show F6: "val_Zp (a ⊖ ns (Suc (Suc k))) = val_Zp (local.divide (f∙a) (f'∙a))"
using F5 F4 F3
by (metis R.minus_closed local.a_closed newton_seq_closed order_less_le val_Zp_not_equal_ord_plus_minus val_Zp_ultrametric_eq'')
qed
qed
thus ?thesis
by (metis AA less_imp_add_positive plus_1_eq_Suc)
qed
qed
thus ?thesis
by blast
qed
qed
lemma hensel_seq_comp_f:
"res_lim ((to_fun f) ∘ ns) = 𝟬"
proof-
have A: "is_Zp_cauchy ((to_fun f) ∘ ns)"
using f_closed is_Zp_continuous_def newton_seq_is_Zp_cauchy polynomial_is_Zp_continuous
by blast
have "Zp_converges_to ((to_fun f) ∘ ns) 𝟬"
apply(rule Zp_converges_toI)
using A is_Zp_cauchy_def apply blast
apply simp
proof-
fix n
show " ∃N. ∀k>N. (((to_fun f) ∘ ns) k) n = 𝟬 n"
proof-
have 0: "⋀k. (k::nat)>3 ⟶ val_Zp (f∙(ns k)) > k"
proof
fix k::nat
assume A: "k >3"
show "val_Zp (f∙(ns k)) > k "
proof-
have 0: " val_Zp (f∙(ns k)) ≥ 2*(val_Zp (f'∙a)) + (2^k)*t"
using newton_seq_fact2 by blast
have 1: "2*(val_Zp (f'∙a)) + (2^k)*t > k "
proof-
have "(2^k)*t ≥ (2^k) "
apply(cases "t = ∞")
apply simp
using t_pos eint_mult_mono'
proof -
obtain ii :: "eint ⇒ int" where
f1: "∀e. (∞ ≠ e ∨ (∀i. eint i ≠ e)) ∧ (eint (ii e) = e ∨ ∞ = e)"
by (metis not_infinity_eq)
then have "0 < ii t"
by (metis (no_types) eint_ord_simps(2) t_neq_infty t_pos zero_eint_def)
then show ?thesis
using f1 by (metis eint_pos_int_times_ge eint_mult_mono linorder_not_less
mult.commute order_less_le t_neq_infty t_pos t_times_pow_pos)
qed
hence " 2*(val_Zp (f'∙a)) + (2^k)*t ≥ (2^k) "
by (smt (verit) Groups.add_ac(2) add.right_neutral eint_2_minus_1_mult eint_pos_times_is_pos
eint_pow_int_is_pos f'a_nonneg_val ge_plus_pos_imp_gt idiff_0_right linorder_not_less
nat_mult_not_infty order_less_le t_neq_infty)
then have " 2*(val_Zp (f'∙a)) + (2^k)*t > k"
using A of_nat_1 of_nat_add of_nat_less_two_power
by (smt (verit) eint_ord_simps(1) linorder_not_less order_trans)
then show ?thesis
by metis
qed
thus ?thesis
using 0 less_le_trans by blast
qed
qed
have 1: "⋀k. (k::nat)>3 ⟶ (f∙(ns k)) k = 0"
proof
fix k::nat
assume B: "3<k"
show " (f∙(ns k)) k = 0"
proof-
have B0: " val_Zp (f∙(ns k)) > k"
using 0 B
by blast
then show ?thesis
by (simp add: f_of_newton_seq_closed zero_below_val_Zp)
qed
qed
have "∀k>(max 3 n). (((to_fun f) ∘ ns) k) n = 𝟬 n"
apply auto
proof-
fix k::nat
assume A: "3< k"
assume A': "n < k"
have A0: "(f∙(ns k)) k = 0"
using 1[of k] A by auto
then have "(f∙(ns k)) n = 0"
using A A'
using above_ord_nonzero[of "(f∙(ns k))"]
by (smt (verit) UP_cring.to_fun_closed Zp_x_is_UP_cring f_closed le_eq_less_or_eq
newton_seq_closed of_nat_mono residue_of_zero(2) zero_below_ord)
then show A1: "to_fun f (ns k) n = 𝟬 n"
by (simp add: residue_of_zero(2))
qed
then show ?thesis by blast
qed
qed
then show ?thesis
by (metis Zp_converges_to_def unique_limit')
qed
lemma full_hensels_lemma:
obtains α where
"f∙α = 𝟬" and "α ∈ carrier Zp"
"val_Zp (a ⊖ α) > val_Zp (f'∙a)"
"(val_Zp (a ⊖ α) = val_Zp (divide (f∙a) (f'∙a)))"
"val_Zp (f'∙α) = val_Zp (f'∙a)"
proof(cases "∃k. f∙(ns k) =𝟬")
case True
obtain k where k_def: "f∙(ns k) =𝟬"
using True by blast
obtain N where N_def: "∀n. n> N ⟶ (val_Zp (a ⊖ (ns n)) = val_Zp (divide (f∙a) (f'∙a)))"
using pre_hensel(2) by blast
have Z: "⋀n. n ≥k ⟹ f∙(ns n) =𝟬"
proof-
fix n
assume A: "n ≥k"
obtain l where l_def:"n = k + l"
using A le_Suc_ex
by blast
have "⋀m. f∙(ns (k+m)) =𝟬"
proof-
fix m
show "f∙(ns (k+m)) =𝟬"
apply(induction m)
apply (simp add: k_def)
using eventually_zero
by simp
qed
then show "f∙(ns n) =𝟬"
by (simp add: l_def)
qed
obtain M where M_def: "M = N + k"
by simp
then have M_root: "f∙(ns M) =𝟬"
by (simp add: Z)
obtain α where alpha_def: "α= ns M"
by simp
have T0: "f∙α = 𝟬"
using alpha_def M_root
by auto
have T1: "val_Zp (a ⊖ α) > val_Zp (f'∙a)"
using alpha_def pre_hensel(1) by blast
have T2: "(val_Zp (a ⊖ α) = val_Zp (divide (f∙a) (f'∙a)))"
by (metis M_def N_def alpha_def fa_nonzero k_def
less_add_same_cancel1 newton_seq.elims zero_less_Suc)
have T3: "val_Zp (f'∙α) = val_Zp (f'∙a)"
using alpha_def newton_seq_fact1 by blast
show ?thesis using T0 T1 T2 T3
using that alpha_def newton_seq_closed
by blast
next
case False
then have Nz: "⋀k. f∙(ns k) ≠𝟬"
by blast
have ns_cauchy: "is_Zp_cauchy ns"
by (simp add: newton_seq_is_Zp_cauchy)
have fns_cauchy: "is_Zp_cauchy ((to_fun f) ∘ ns)"
using f_closed is_Zp_continuous_def ns_cauchy polynomial_is_Zp_continuous by blast
have F0: "res_lim ((to_fun f) ∘ ns) = 𝟬"
proof-
show ?thesis
using hensel_seq_comp_f by auto
qed
obtain α where alpha_def: "α = res_lim ns"
by simp
have F1: "(f∙α)= 𝟬"
using F0 alpha_def alt_seq_limit
ns_cauchy polynomial_is_Zp_continuous res_lim_pushforward
res_lim_pushforward' by auto
have F2: "val_Zp (a ⊖ α) > val_Zp (f'∙a) ∧ val_Zp (a ⊖ α) = val_Zp (local.divide (f∙a) (f'∙a))"
proof-
have 0: "Zp_converges_to ns α"
by (simp add: alpha_def is_Zp_cauchy_imp_has_limit ns_cauchy)
have "val_Zp (a ⊖ α) < ∞"
using "0" F1 R.r_right_minus_eq Zp_converges_to_def Zp_def hensel.fa_nonzero hensel_axioms local.a_closed val_Zp_def
by auto
hence "1 + max (eint 2 + val_Zp (f'∙a)) (val_Zp (α ⊖ a)) < ∞"
by (metis "0" R.minus_closed Zp_converges_to_def eint.distinct(2) eint_ord_simps(4)
f'a_not_infinite infinity_ne_i1 local.a_closed max_def minus_a_inv
sum_infinity_imp_summand_infinity val_Zp_of_minus)
then obtain l where l_def: "eint l = 1 + max (eint 2 + val_Zp (f'∙a)) (val_Zp (α ⊖ a))"
by auto
then obtain N where N_def: "(∀m>N. 1 + max (2 + val_Zp (f'∙a)) (val_Zp (α ⊖ a)) < val_Zp_dist (ns m) α)"
using 0 l_def Zp_converges_to_def[of ns α] unfolding val_Zp_dist_def
by metis
obtain N' where N'_def: "∀n>N'. val_Zp (a ⊖ ns n) = val_Zp (local.divide (f∙a) (f'∙a))"
using pre_hensel(2) by blast
obtain K where K_def: "K = Suc (max N N')"
by simp
then have F21: "(1+ (max (2 + val_Zp (f'∙a)) (val_Zp (α ⊖ a)))) < val_Zp_dist (ns K) α"
by (metis N_def lessI linorder_not_less max_def order_trans)
have F22: "a ≠ ns K"
by (smt (verit, del_insts) F21 Nz alpha_def eint_1_iff(1) eint_pow_int_is_pos less_le
local.a_closed max_less_iff_conj newton_seq_is_Zp_cauchy_0 not_less pos_add_strict
res_lim_in_Zp val_Zp_dist_def val_Zp_dist_sym)
show ?thesis
proof(cases "ns K = α")
case True
then show ?thesis
using pre_hensel F1 False by blast
next
case False
assume "ns K ≠ α"
show ?thesis
proof-
have P0: " (a ⊖ α) ∈ nonzero Zp"
by (metis (mono_tags, opaque_lifting) F1 not_eq_diff_nonzero
‹Zp_converges_to ns α› a_closed Zp_converges_to_def fa_nonzero)
have P1: "(α ⊖ (ns K)) ∈ nonzero Zp"
using False not_eq_diff_nonzero ‹Zp_converges_to ns α›
Zp_converges_to_def newton_seq_closed
by (metis (mono_tags, opaque_lifting))
have P2: "a ⊖ (ns K) ∈ nonzero Zp"
using F22 not_eq_diff_nonzero
a_closed newton_seq_closed
by blast
have P3: "(a ⊖ α) = a ⊖ (ns K) ⊕ ((ns K) ⊖ α)"
by (metis R.plus_diff_simp ‹Zp_converges_to ns α› add_comm Zp_converges_to_def local.a_closed newton_seq_closed)
have P4: "val_Zp (a ⊖ α) ≥ min (val_Zp (a ⊖ (ns K))) (val_Zp ((ns K) ⊖ α))"
using "0" P3 Zp_converges_to_def newton_seq_closed val_Zp_ultrametric
by auto
have P5: "val_Zp (a ⊖ (ns K)) > val_Zp (f'∙a)"
using pre_hensel(1)[of "K"]
by metis
have "1 + max (eint 2 + val_Zp (f'∙a)) (val_Zp (α ⊖ a)) > val_Zp (f'∙a)"
proof-
have "1 + max (eint 2 + val_Zp (f'∙a)) (val_Zp (α ⊖ a)) > (eint 2 + val_Zp (f'∙a))"
proof -
obtain ii :: int where
f1: "eint ii = 1 + max (eint 2 + val_Zp (f'∙a)) (val_Zp (α ⊖ a))"
by (meson l_def)
then have "1 + (eint 2 + val_Zp (f'∙a)) ≤ eint ii"
by simp
then show ?thesis
using f1 by (metis Groups.add_ac(2) iless_Suc_eq linorder_not_less)
qed
thus ?thesis
by (smt (verit) Groups.add_ac(2) eint_pow_int_is_pos f'a_not_infinite ge_plus_pos_imp_gt order_less_le)
qed
hence P6: "val_Zp ((ns K) ⊖ α) > val_Zp (f'∙a)"
using F21 unfolding val_Zp_dist_def
by auto
have P7: "val_Zp (a ⊖ α) > val_Zp (f'∙a)"
using P4 P5 P6 eint_min_ineq by blast
have P8: "val_Zp (a ⊖ α) = val_Zp (local.divide (f∙a) (f'∙a))"
proof-
have " 1 + max (2 + val_Zp (f'∙a)) (val_Zp_dist α a) ≤ val_Zp_dist (ns K) α"
using False F21
by (simp add: val_Zp_dist_def)
then have "val_Zp(α ⊖ (ns K)) > max (2 + val_Zp (f'∙a)) (val_Zp_dist α a)"
by (metis "0" Groups.add_ac(2) P1 Zp_converges_to_def eSuc_mono iless_Suc_eq l_def
minus_a_inv newton_seq_closed nonzero_closed val_Zp_dist_def val_Zp_of_minus)
then have "val_Zp(α ⊖ (ns K)) > val_Zp (a ⊖ α) "
using ‹Zp_converges_to ns α› Zp_converges_to_def val_Zp_dist_def val_Zp_dist_sym
by auto
then have P80: "val_Zp (a ⊖ α) = val_Zp (a ⊖ (ns K))"
using P0 P1 Zp_def val_Zp_ultrametric_eq[of "α ⊖ ns K" "a ⊖ α"] 0 R.plus_diff_simp
Zp_converges_to_def local.a_closed newton_seq_closed nonzero_closed by auto
have P81: "val_Zp (a ⊖ ns K) = val_Zp (local.divide (f∙a) (f'∙a))"
using K_def N'_def
by (metis (no_types, lifting) lessI linorder_not_less max_def order_less_le order_trans)
then show ?thesis
by (simp add: P80)
qed
thus ?thesis
using P7 by blast
qed
qed
qed
have F3: "val_Zp (f' ∙ α) = val_Zp (f'∙a)"
proof-
have F31: " (f' ∙ α) = res_lim ((to_fun f') ∘ ns)"
using alpha_def alt_seq_limit ns_cauchy polynomial_is_Zp_continuous res_lim_pushforward
res_lim_pushforward' f'_closed
by auto
obtain N where N_def: "val_Zp (f'∙α ⊖ f'∙(ns N)) > val_Zp ((f'∙a))"
by (smt (verit) F2 False R.minus_closed Suc_ile_eq Zp_def alpha_def f'_closed f'a_nonzero
local.a_closed minus_a_inv newton_seq.simps(1) newton_seq_is_Zp_cauchy_0 order_trans
padic_integers.poly_diff_val padic_integers_axioms res_lim_in_Zp val_Zp_def val_Zp_of_minus)
show ?thesis
by (metis False N_def alpha_def equal_val_Zp f'_closed newton_seq_closed newton_seq_is_Zp_cauchy_0 newton_seq_fact1 res_lim_in_Zp to_fun_closed)
qed
show ?thesis
using F1 F2 F3 that alpha_def ns_cauchy res_lim_in_Zp
by blast
qed
end
section‹Removing Hensel's Lemma from the Hensel Locale›
context padic_integers
begin
lemma hensels_lemma:
assumes "f ∈ carrier Zp_x"
assumes "a ∈ carrier Zp"
assumes "(pderiv f)∙a ≠ 𝟬"
assumes "f∙a ≠𝟬"
assumes "val_Zp (f∙a) > 2* val_Zp ((pderiv f)∙a)"
obtains α where
"f∙α = 𝟬" and "α ∈ carrier Zp"
"val_Zp (a ⊖ α) > val_Zp ((pderiv f)∙a)"
"val_Zp (a ⊖ α) = val_Zp (divide (f∙a) ((pderiv f)∙a))"
"val_Zp ((pderiv f)∙α) = val_Zp ((pderiv f)∙a)"
proof-
have "hensel p f a"
using assms
by (simp add: Zp_def hensel.intro hensel_axioms.intro padic_integers_axioms)
then show ?thesis
using hensel.full_hensels_lemma Zp_def that
by blast
qed
text‹Uniqueness of the root found in Hensel's lemma ›
lemma hensels_lemma_unique_root:
assumes "f ∈ carrier Zp_x"
assumes "a ∈ carrier Zp"
assumes "(pderiv f)∙a ≠ 𝟬"
assumes "f∙a ≠𝟬"
assumes "(val_Zp (f∙a) > 2* val_Zp ((pderiv f)∙a))"
assumes "f∙α = 𝟬"
assumes "α ∈ carrier Zp"
assumes "val_Zp (a ⊖ α) > val_Zp ((pderiv f)∙a)"
assumes "f∙β = 𝟬"
assumes "β ∈ carrier Zp"
assumes "val_Zp (a ⊖ β) > val_Zp ((pderiv f)∙a)"
assumes "val_Zp ((pderiv f)∙α) = val_Zp ((pderiv f)∙a)"
shows "α = β"
proof-
have "α ≠ a"
using assms(4) assms(6) by auto
have "β ≠ a"
using assms(4) assms(9) by auto
have 0: "val_Zp (β ⊖ α) > val_Zp ((pderiv f)∙a)"
proof-
have "β ⊖ α = ⊖ ((a ⊖ β) ⊖ (a ⊖ α))"
by (metis R.minus_eq R.plus_diff_simp assms(10) assms(2) assms(7) minus_a_inv)
hence "val_Zp (β ⊖ α) = val_Zp ((a ⊖ β) ⊖ (a ⊖ α))"
using R.minus_closed assms(10) assms(2) assms(7) val_Zp_of_minus by presburger
thus ?thesis using val_Zp_ultrametric_diff[of "a ⊖ β" "a ⊖ α"]
by (smt (verit) R.minus_closed assms(10) assms(11) assms(2) assms(7) assms(8) min.absorb2 min_less_iff_conj)
qed
obtain h where h_def: "h = β ⊖ α"
by blast
then have h_fact: "h ∈ carrier Zp ∧ β = α ⊕ h"
by (metis R.l_neg R.minus_closed R.minus_eq R.r_zero add_assoc add_comm assms(10) assms(7))
then have 1: "f∙(α ⊕ h) = 𝟬"
using assms
by blast
obtain c where c_def: "c ∈ carrier Zp ∧ f∙(α ⊕ h) = (f ∙ α) ⊕ (deriv f α)⊗h ⊕ c ⊗(h[^](2::nat))"
using taylor_deg_1_eval'[of f α h _ "f ∙ α" "deriv f α" ]
by (meson taylor_closed assms(1) assms(7) to_fun_closed h_fact shift_closed)
then have "(f ∙ α) ⊕ (deriv f α)⊗h ⊕ c ⊗(h[^](2::nat)) = 𝟬"
by (simp add: "1")
then have 2: "(deriv f α)⊗h ⊕ c ⊗(h[^](2::nat)) = 𝟬"
by (simp add: assms(1) assms(6) assms(7) deriv_closed h_fact)
have 3: "((deriv f α) ⊕ c ⊗h)⊗h = 𝟬"
proof-
have "((deriv f α) ⊕ c ⊗h)⊗h = ((deriv f α)⊗h ⊕ (c ⊗h)⊗h)"
by (simp add: R.r_distr UP_cring.deriv_closed Zp_x_is_UP_cring assms(1) assms(7) c_def h_fact mult_comm)
then have "((deriv f α) ⊕ c ⊗h)⊗h = (deriv f α)⊗h ⊕ (c ⊗(h⊗h))"
by (simp add: mult_assoc)
then have "((deriv f α) ⊕ c ⊗h)⊗h = (deriv f α)⊗h ⊕ (c ⊗(h[^](2::nat)))"
using nat_pow_def[of Zp h "2"]
by (simp add: h_fact)
then show ?thesis
using 2
by simp
qed
have "h = 𝟬"
proof(rule ccontr)
assume "h ≠ 𝟬"
then have "(deriv f α) ⊕ c ⊗h = 𝟬"
using 2 3
by (meson R.m_closed assms(1) assms(7) c_def deriv_closed h_fact local.integral sum_closed)
then have "(deriv f α) = ⊖ c ⊗h"
by (simp add: R.l_minus R.sum_zero_eq_neg UP_cring.deriv_closed Zp_x_is_UP_cring assms(1) assms(7) c_def h_fact)
then have "val_Zp (deriv f α) = val_Zp (c ⊗ h)"
by (meson R.m_closed ‹deriv f α ⊕ c ⊗ h = 𝟬› assms(1) assms(7) c_def deriv_closed h_fact val_Zp_not_equal_imp_notequal(3))
then have P: "val_Zp (deriv f α) = val_Zp h + val_Zp c"
using val_Zp_mult c_def h_fact by force
hence "val_Zp (deriv f α) ≥ val_Zp h "
using val_pos[of c]
by (simp add: c_def)
then have "val_Zp (deriv f α) ≥ val_Zp (β ⊖ α) "
using h_def by blast
then have "val_Zp (deriv f α) > val_Zp ((pderiv f)∙a)"
using "0" by auto
then show False using pderiv_eval_deriv[of f α]
using assms(1) assms(12) assms(7) by auto
qed
then show "α = β"
using assms(10) assms(7) h_def
by auto
qed
lemma hensels_lemma':
assumes "f ∈ carrier Zp_x"
assumes "a ∈ carrier Zp"
assumes "val_Zp (f∙a) > 2*val_Zp ((pderiv f)∙a)"
shows "∃!α ∈ carrier Zp. f∙α = 𝟬 ∧ val_Zp (a ⊖ α) > val_Zp ((pderiv f)∙a)"
proof(cases "f∙a = 𝟬")
case True
have T0: "pderiv f ∙ a ≠ 𝟬"
apply(rule ccontr) using assms(3)
unfolding val_Zp_def by simp
then have T1: "a ∈ carrier Zp ∧ f∙a = 𝟬 ∧ val_Zp (a ⊖ a) > val_Zp ((pderiv f)∙a)"
using assms True
by(simp add: val_Zp_def)
have T2: "⋀b. b ∈ carrier Zp ∧ f∙b = 𝟬 ∧ val_Zp (a ⊖ b) > val_Zp ((pderiv f)∙a) ⟹ a = b"
proof- fix b assume A: "b ∈ carrier Zp ∧ f∙b = 𝟬 ∧ val_Zp (a ⊖ b) > val_Zp ((pderiv f)∙a)"
obtain h where h_def: "h = b ⊖ a"
by blast
then have h_fact: "h ∈ carrier Zp ∧ b = a ⊕ h"
by (metis A R.l_neg R.minus_closed R.minus_eq R.r_zero add_assoc add_comm assms(2))
then have 1: "f∙(a ⊕ h) = 𝟬"
using assms A by blast
obtain c where c_def: "c ∈ carrier Zp ∧ f∙(a ⊕ h) = (f ∙ a) ⊕ (deriv f a)⊗h ⊕ c ⊗(h[^](2::nat))"
using taylor_deg_1_eval'[of f a h _ "f ∙ a" "deriv f a" ]
by (meson taylor_closed assms(1) assms(2) to_fun_closed h_fact shift_closed)
then have "(f ∙ a) ⊕ (deriv f a)⊗h ⊕ c ⊗(h[^](2::nat)) = 𝟬"
by (simp add: "1")
then have 2: "(deriv f a)⊗h ⊕ c ⊗(h[^](2::nat)) = 𝟬"
by (simp add: True assms(1) assms(2) deriv_closed h_fact)
hence 3: "((deriv f a) ⊕ c ⊗h)⊗h = 𝟬"
proof-
have "((deriv f a) ⊕ c ⊗h)⊗h = ((deriv f a)⊗h ⊕ (c ⊗h)⊗h)"
by (simp add: R.l_distr assms(1) assms(2) c_def deriv_closed h_fact)
then have "((deriv f a) ⊕ c ⊗h)⊗h = (deriv f a)⊗h ⊕ (c ⊗(h⊗h))"
by (simp add: mult_assoc)
then have "((deriv f a) ⊕ c ⊗h)⊗h = (deriv f a)⊗h ⊕ (c ⊗(h[^](2::nat)))"
using nat_pow_def[of Zp h "2"]
by (simp add: h_fact)
then show ?thesis
using 2
by simp
qed
have "h = 𝟬"
proof(rule ccontr)
assume "h ≠ 𝟬"
then have "(deriv f a) ⊕ c ⊗h = 𝟬"
using 2 3
by (meson R.m_closed UP_cring.deriv_closed Zp_x_is_UP_cring assms(1) assms(2) c_def h_fact local.integral sum_closed)
then have "(deriv f a) = ⊖ c ⊗h"
using R.l_minus R.minus_equality assms(1) assms(2) c_def deriv_closed h_fact by auto
then have "val_Zp (deriv f a) = val_Zp (c ⊗ h)"
by (meson R.m_closed ‹deriv f a ⊕ c ⊗ h = 𝟬› assms(1) assms(2) c_def deriv_closed h_fact val_Zp_not_equal_imp_notequal(3))
then have P: "val_Zp (deriv f a) = val_Zp h + val_Zp c"
by (simp add: c_def h_fact val_Zp_mult)
have "val_Zp (deriv f a) ≥ val_Zp h "
using P val_pos[of c] c_def
by simp
then have "val_Zp (deriv f a) ≥ val_Zp (b ⊖ a) "
using h_def by blast
then have "val_Zp (deriv f a) > val_Zp ((pderiv f)∙a)"
by (metis (no_types, lifting) A assms(2) h_def h_fact minus_a_inv not_less order_trans val_Zp_of_minus)
then have P0:"val_Zp (deriv f a) > val_Zp (deriv f a)"
by (metis UP_cring.pderiv_eval_deriv Zp_x_is_UP_cring assms(1) assms(2))
thus False by auto
qed
then show "a = b"
by (simp add: assms(2) h_fact)
qed
show ?thesis
using T1 T2
by blast
next
case False
have F0: "pderiv f ∙ a ≠ 𝟬"
apply(rule ccontr) using assms(3)
unfolding val_Zp_def by simp
obtain α where alpha_def:
"f∙α = 𝟬" "α ∈ carrier Zp"
"val_Zp (a ⊖ α) > val_Zp ((pderiv f)∙a)"
"(val_Zp (a ⊖ α) = val_Zp (divide (f∙a) ((pderiv f)∙a)))"
"val_Zp ((pderiv f)∙α) = val_Zp ((pderiv f)∙a)"
using assms hensels_lemma F0 False by blast
have 0: "⋀x. x ∈ carrier Zp ∧ f ∙ x = 𝟬 ∧ val_Zp (a ⊖ x) > val_Zp (pderiv f ∙ a) ∧ val_Zp (pderiv f ∙ a) ≠ val_Zp (a ⊖ x) ⟹ x= α"
using alpha_def assms hensels_lemma_unique_root[of f a α] F0 False by blast
have 1: "α ∈ carrier Zp ∧ f ∙ α = 𝟬 ∧ val_Zp (a ⊖ α) > val_Zp (pderiv f ∙ a) ∧ val_Zp (pderiv f ∙ a) ≠ val_Zp (a ⊖ α)"
using alpha_def order_less_le by blast
thus ?thesis
using 0
by (metis (no_types, opaque_lifting) R.minus_closed alpha_def(1-3) assms(2) equal_val_Zp val_Zp_ultrametric_eq')
qed
section‹Some Applications of Hensel's Lemma to Root Finding for Polynomials over $\mathbb{Z}_p$›
lemma Zp_square_root_criterion:
assumes "p ≠ 2"
assumes "a ∈ carrier Zp"
assumes "b ∈ carrier Zp"
assumes "val_Zp b ≥ val_Zp a"
assumes "a ≠ 𝟬"
assumes "b ≠ 𝟬"
shows "∃y ∈ carrier Zp. a[^](2::nat) ⊕ 𝗉⊗b[^](2::nat) = (y [^]⇘Zp⇙ (2::nat))"
proof-
have bounds: "val_Zp a < ∞" "val_Zp a ≥ 0" "val_Zp b < ∞" "val_Zp b ≥ 0"
using assms(2) assms(3) assms(6) assms(5) val_Zp_def val_pos[of b] val_pos[of a]
by auto
obtain f where f_def: "f = monom Zp_x 𝟭 2 ⊕⇘Zp_x⇙ to_polynomial Zp (⊖ (a[^](2::nat)⊕ 𝗉⊗b[^](2::nat)))"
by simp
have "∃ α. f∙α = 𝟬 ∧ α ∈ carrier Zp"
proof-
have 0: "f ∈ carrier Zp_x"
using f_def
by (simp add: X_closed assms(2) assms(3) to_poly_closed)
have 1: "(pderiv f)∙a = [(2::nat)] ⋅ 𝟭 ⊗ a"
proof-
have "pderiv f = pderiv (monom Zp_x 𝟭 2)"
using assms f_def pderiv_add[of "monom Zp_x 𝟭 2"] to_poly_closed R.nat_pow_closed
pderiv_deg_0
unfolding to_polynomial_def
using P.nat_pow_closed P.r_zero R.add.inv_closed X_closed Zp_int_inc_closed deg_const monom_term_car pderiv_closed sum_closed
by (metis (no_types, lifting) R.one_closed monom_closed)
then have 20: "pderiv f = monom (Zp_x) ([(2::nat) ] ⋅ 𝟭) (1::nat)"
using pderiv_monom[of 𝟭 2]
by simp
have 21: "[(2::nat)] ⋅ 𝟭 ≠ 𝟬"
using Zp_char_0'[of 2] by simp
have 22: "(pderiv f)∙a = [(2::nat)] ⋅ 𝟭 ⊗ (a[^]((1::nat)))"
using 20
by (simp add: Zp_nat_inc_closed assms(2) to_fun_monom)
then show ?thesis
using assms(2)
by (simp add: cring.cring_simprules(12))
qed
have 2: "(pderiv f)∙a ≠ 𝟬"
using 1 assms
by (metis Zp_char_0' Zp_nat_inc_closed local.integral zero_less_numeral)
have 3: "f∙a = ⊖ (𝗉⊗b[^](2::nat))"
proof-
have 3: "f∙a =
monom (UP Zp) 𝟭 2 ∙ a ⊕
to_polynomial Zp (⊖ (a [^] (2::nat) ⊕ [p] ⋅ 𝟭 ⊗ b [^] (2::nat)))∙a"
unfolding f_def apply(rule to_fun_plus)
apply (simp add: assms(2) assms(3) to_poly_closed)
apply simp
by (simp add: assms(2))
have 30: "f∙a = a[^](2::nat) ⊖ (a[^](2::nat) ⊕ 𝗉⊗b[^](2::nat))"
unfolding 3 by (simp add: R.minus_eq assms(2) assms(3) to_fun_monic_monom to_fun_to_poly)
have 31: "f∙a = a[^](2::nat) ⊖ a[^](2::nat) ⊖ (𝗉⊗b[^](2::nat))"
proof-
have 310: "a[^](2::nat) ∈ carrier Zp"
using assms(2) pow_closed
by blast
have 311: "𝗉⊗(b[^](2::nat)) ∈ carrier Zp"
by (simp add: assms(3) monom_term_car)
have "⊖ (a [^] (2::nat)⊕(𝗉 ⊗ b [^] (2::nat))) = ⊖ (a [^] (2::nat)) ⊕ ⊖ (𝗉 ⊗ (b [^] (2::nat)))"
using 310 311 R.minus_add by blast
then show ?thesis
by (simp add: "30" R.minus_eq add_assoc)
qed
have 32: "f∙a = (a[^](2::nat) ⊖ a[^](2::nat)) ⊖ (𝗉⊗b[^](2::nat))"
using 31 unfolding a_minus_def
by blast
have 33: "𝗉⊗b[^](2::nat) ∈ carrier Zp"
by (simp add: Zp_nat_inc_closed assms(3) monom_term_car)
have 34: "a[^](2::nat) ∈ carrier Zp"
using assms(2) pow_closed by blast
then have 34: "(a[^](2::nat) ⊖ a[^](2::nat)) = 𝟬 "
by simp
have 35: "f∙a = 𝟬 ⊖ (𝗉⊗b[^](2::nat))"
by (simp add: "32" "34")
then show ?thesis
using 33 unfolding a_minus_def
by (simp add: cring.cring_simprules(3))
qed
have 4: "f∙a ≠𝟬"
using 3 assms
by (metis R.add.inv_eq_1_iff R.m_closed R.nat_pow_closed Zp.integral Zp_int_inc_closed
mult_zero_r nonzero_pow_nonzero p_natpow_prod_Suc(1) p_pow_nonzero(2))
have 5: "val_Zp (f∙a) = 1 + 2*val_Zp b"
proof-
have "val_Zp (f∙a) = val_Zp (𝗉⊗b[^](2::nat))"
using 3 Zp_int_inc_closed assms(3) monom_term_car val_Zp_of_minus by presburger
then have "val_Zp (𝗉⊗b[^](2::nat)) = 1 + val_Zp (b[^](2::nat))"
by (simp add: assms(3) val_Zp_mult val_Zp_p)
then show ?thesis
using assms(3) assms(6)
using Zp_def ‹val_Zp (to_fun f a) = val_Zp ([p] ⋅ 𝟭 ⊗ b [^] 2)› not_nonzero_Zp
padic_integers_axioms val_Zp_pow' by fastforce
qed
have 6: "val_Zp ((pderiv f)∙a) = val_Zp a"
proof-
have 60: "val_Zp ([(2::nat)] ⋅ 𝟭 ⊗ a) = val_Zp ([(2::nat)] ⋅ 𝟭) + val_Zp a"
by (simp add: Zp_char_0' assms(2) assms(5) val_Zp_mult ord_of_nonzero(2) ord_pos)
have "val_Zp ([(2::nat)] ⋅ 𝟭) = 0"
proof-
have "(2::nat) < p"
using prime assms prime_ge_2_int by auto
then have "(2::nat) mod p = (2::nat)"
by simp
then show ?thesis
by (simp add: val_Zp_p_nat_unit)
qed
then show ?thesis
by (simp add: "1" "60")
qed
then have 7: "val_Zp (f∙a) > 2* val_Zp ((pderiv f)∙a)"
using bounds 5 assms(4)
by (simp add: assms(5) assms(6) one_eint_def val_Zp_def)
obtain α where
A0: "f∙α = 𝟬" "α ∈ carrier Zp"
using hensels_lemma[of f a] "0" "2" "4" "7" assms(2)
by blast
show ?thesis
using A0 by blast
qed
then obtain α where α_def: "f∙α = 𝟬 ∧ α ∈ carrier Zp"
by blast
have "f∙α = α [^](2::nat) ⊖ (a[^](2::nat)⊕ 𝗉⊗b[^](2::nat))"
proof-
have 0: "f∙α =
monom (UP Zp) 𝟭 2 ∙ α ⊕
to_polynomial Zp (⊖ (a [^] (2::nat) ⊕ [p] ⋅ 𝟭 ⊗ b [^] (2::nat)))∙α"
unfolding f_def apply(rule to_fun_plus)
apply (simp add: assms(2) assms(3) to_poly_closed)
apply simp
by (simp add: α_def)
thus ?thesis
by (simp add: R.minus_eq α_def assms(2) assms(3) to_fun_monic_monom to_fun_to_poly)
qed
then show ?thesis
by (metis R.r_right_minus_eq Zp_int_inc_closed α_def assms(2) assms(3) monom_term_car pow_closed sum_closed)
qed
lemma Zp_semialg_eq:
assumes "a ∈ nonzero Zp"
shows "∃y ∈ carrier Zp. 𝟭 ⊕ (𝗉 [^] (3::nat))⊗ (a [^] (4::nat)) = (y [^] (2::nat))"
proof-
obtain f where f_def: "f = monom Zp_x 𝟭 2 ⊕⇘Zp_x⇙ to_poly (⊖ (𝟭 ⊕ (𝗉 [^] (3::nat))⊗ (a [^] (4::nat))))"
by simp
have a_car: "a ∈ carrier Zp"
by (simp add: nonzero_memE assms)
have "f ∈ carrier Zp_x"
using f_def
by (simp add: a_car to_poly_closed)
hence 0:"f∙𝟭 = 𝟭 ⊖ (𝟭 ⊕ (𝗉 [^] (3::nat))⊗ (a [^] (4::nat)))"
using f_def
by (simp add: R.minus_eq assms nat_pow_nonzero nonzero_mult_in_car p_pow_nonzero' to_fun_monom_plus to_fun_to_poly to_poly_closed)
then have 1: "f∙𝟭 = ⊖ (𝗉 [^] (3::nat))⊗ (a [^] (4::nat))"
unfolding a_minus_def
by (smt (verit) R.add.inv_closed R.l_minus R.minus_add R.minus_minus R.nat_pow_closed R.one_closed R.r_neg1 a_car monom_term_car p_pow_nonzero(1))
then have "val_Zp (f∙𝟭) = 3 + val_Zp (a [^] (4::nat))"
using assms val_Zp_mult[of "𝗉 [^] (3::nat)" "(a [^] (4::nat))" ]
val_Zp_p_pow p_pow_nonzero[of "3::nat"] val_Zp_of_minus
by (metis R.l_minus R.nat_pow_closed a_car monom_term_car of_nat_numeral)
then have 2: "val_Zp (f∙𝟭) = 3 + 4* val_Zp a"
using assms val_Zp_pow' by auto
have "pderiv f = pderiv (monom Zp_x 𝟭 2)"
using assms f_def pderiv_add[of "monom Zp_x 𝟭 2"] to_poly_closed R.nat_pow_closed pderiv_deg_0
unfolding to_polynomial_def
by (metis (no_types, lifting) P.r_zero R.add.inv_closed R.add.m_closed R.one_closed
UP_zero_closed a_car deg_const deg_nzero_nzero monom_closed monom_term_car p_pow_nonzero(1))
then have 3: "pderiv f = [(2::nat)] ⋅ 𝟭 ⊙⇘Zp_x⇙ X "
by (metis P.nat_pow_eone R.one_closed Suc_1 X_closed diff_Suc_1 monom_rep_X_pow pderiv_monom')
hence 4: "val_Zp ((pderiv f)∙𝟭) = val_Zp ([(2::nat)] ⋅ 𝟭 )"
by (metis R.add.nat_pow_eone R.nat_inc_prod R.nat_inc_prod' R.nat_pow_one R.one_closed
Zp_nat_inc_closed ‹pderiv f = pderiv (monom Zp_x 𝟭 2)› pderiv_monom to_fun_monom)
have "(2::int) = (int (2::nat))"
by simp
then have 5: "[(2::nat)] ⋅ 𝟭 = ([(int (2::nat))] ⋅ 𝟭 )"
using add_pow_def int_pow_int
by metis
have 6: "val_Zp ((pderiv f)∙𝟭) ≤ 1"
apply(cases "p = 2")
using "4" "5" val_Zp_p apply auto[1]
proof-
assume "p ≠ 2"
then have 60: "coprime 2 p"
using prime prime_int_numeral_eq primes_coprime two_is_prime_nat by blast
have 61: "2 < p"
using 60 prime
by (smt (verit) ‹p ≠ 2› prime_gt_1_int)
then show ?thesis
by (smt (verit) "4" "5" ‹2 = int 2› mod_pos_pos_trivial nonzero_closed p_nonzero val_Zp_p val_Zp_p_int_unit val_pos)
qed
have 7: "val_Zp (f∙𝟭) ≥ 3"
proof-
have "eint 4 * val_Zp a ≥ 0"
using 2 val_pos[of a]
by (metis R.nat_pow_closed a_car assms of_nat_numeral val_Zp_pow' val_pos)
thus ?thesis
using "2" by auto
qed
have "2*val_Zp ((pderiv f)∙𝟭) ≤ 2*1"
using 6 one_eint_def eint_mult_mono'
by (smt (verit) ‹2 = int 2› eint.distinct(2) eint_ile eint_ord_simps(1) eint_ord_simps(2) mult.commute
ord_Zp_p ord_Zp_p_pow ord_Zp_pow p_nonzero p_pow_nonzero(1) times_eint_simps(1) val_Zp_p val_Zp_pow' val_pos)
hence 8: "2 * val_Zp ((pderiv f)∙ 𝟭) < val_Zp (f∙𝟭)"
using 7 le_less_trans[of "2 * val_Zp ((pderiv f)∙ 𝟭)" "2::eint" 3]
less_le_trans[of "2 * val_Zp ((pderiv f)∙ 𝟭)" 3 "val_Zp (f∙𝟭)"] one_eint_def
by auto
obtain α where α_def: "f∙α = 𝟬" and α_def' :"α ∈ carrier Zp"
using 2 6 7 hensels_lemma' 8 ‹f ∈ carrier Zp_x› by blast
have 0: "(monom Zp_x 𝟭 2) ∙ α = α [^] (2::nat)"
by (simp add: α_def' to_fun_monic_monom)
have 1: "to_poly (⊖ (𝟭 ⊕ (𝗉 [^] (3::nat))⊗ (a [^] (4::nat)))) ∙ α =⊖( 𝟭 ⊕ (𝗉 [^] (3::nat))⊗ (a [^] (4::nat)))"
by (simp add: α_def' a_car to_fun_to_poly)
then have "α [^] (2::nat) ⊖ (𝟭 ⊕ (𝗉 [^] (3::nat))⊗ (a [^] (4::nat))) = 𝟬"
using α_def α_def'
by (simp add: R.minus_eq a_car f_def to_fun_monom_plus to_poly_closed)
then show ?thesis
by (metis R.add.m_closed R.nat_pow_closed R.one_closed R.r_right_minus_eq α_def' a_car monom_term_car p_pow_nonzero(1))
qed
lemma Zp_nth_root_lemma:
assumes "a ∈ carrier Zp"
assumes "a ≠ 𝟭"
assumes "n > 1"
assumes "val_Zp (𝟭 ⊖ a) > 2*val_Zp ([(n::nat)]⋅ 𝟭)"
shows "∃ b ∈ carrier Zp. b[^]n = a"
proof-
obtain f where f_def: "f = monom Zp_x 𝟭 n ⊕⇘Zp_x⇙ monom Zp_x (⊖a) 0"
by simp
have "f ∈ carrier Zp_x"
using f_def monom_closed assms
by simp
have 0: "pderiv f = monom Zp_x ([n]⋅ 𝟭) (n-1)"
by (simp add: assms(1) f_def pderiv_add pderiv_monom)
have 1: "f ∙ 𝟭 = 𝟭 ⊖ a"
using f_def
by (metis R.add.inv_closed R.minus_eq R.nat_pow_one R.one_closed assms(1) to_fun_const to_fun_monom to_fun_monom_plus monom_closed)
have 2: "(pderiv f) ∙ 𝟭 = ([n]⋅ 𝟭)"
using 0 to_fun_monom assms
by simp
have 3: "val_Zp (f ∙ 𝟭) > 2* val_Zp ((pderiv f) ∙ 𝟭)"
using 1 2 assms
by (simp add: val_Zp_def)
have 4: "f ∙ 𝟭 ≠ 𝟬"
using 1 assms(1) assms(2) by auto
have 5: "(pderiv f) ∙ 𝟭 ≠ 𝟬"
using "2" Zp_char_0' assms(3) by auto
obtain β where beta_def: "β ∈ carrier Zp ∧ f ∙ β = 𝟬"
using hensels_lemma[of f 𝟭]
by (metis "3" "5" R.one_closed ‹f ∈ carrier Zp_x›)
then have "(β [^] n) ⊖ a = 𝟬"
using f_def R.add.inv_closed assms(1) to_fun_const[of "⊖ a"] to_fun_monic_monom[of β n] to_fun_plus monom_closed
unfolding a_minus_def
by (simp add: beta_def)
then have "β ∈ carrier Zp ∧ β [^] n = a"
using beta_def nonzero_memE not_eq_diff_nonzero assms(1) pow_closed
by blast
then show ?thesis by blast
qed
end
end