Theory Pi_Relations

theory Pi_Relations
  imports J3_Relations
begin

subsection ‹The $\Pi$ polynomial›

(* Auxiliary lemma *)
lemma finite_when: "finite {x. (f x when x = c) ≠ 0}"
  by auto

locale section5_variables
begin

definition 𝒮 :: "int mpoly" where "𝒮 ≡ Var 4"
definition 𝒯 :: "int mpoly" where "𝒯 ≡ Var 5"
definition ℛ :: "int mpoly" where "ℛ ≡ Var 6"
definition ℐ :: "int mpoly" where "ℐ ≡ Var 7"
definition 𝒴 :: "int mpoly" where "𝒴 ≡ Var 8"
definition ℨ :: "int mpoly" where "ℨ ≡ Var 9"
definition 𝒥 :: "int mpoly" where "𝒥 ≡ Var 10"
definition 𝗇 :: "int mpoly" where "𝗇 ≡ Var 11"

definition 𝒰 ::"int mpoly" where "𝒰 = 𝒮^2 * (2*ℛ-1)"
definition 𝒱 ::"int mpoly" where "𝒱 = 𝒯^2 + 𝒮^2 * 𝗇"

lemmas defs = 𝒮_def 𝒯_def ℛ_def ℐ_def 𝒴_def ℨ_def 𝒥_def 𝗇_def 𝒰_def 𝒱_def

end 

locale pi_relations = section5_variables + 
  fixes ℱ :: "int mpoly"
    and v :: nat
  assumes F_monom_over_v: "vars ℱ ⊆ {v}"
      and F_one: "coeff ℱ (Abs_poly_mapping (λk. (degree ℱ v when k = v))) = 1"
begin

definition coeff_F where 
  "coeff_F d = coeff ℱ (Abs_poly_mapping (λk. (d when k = v)))"
definition q :: nat where 
  "q = degree ℱ v"
definition G :: "int mpoly" where 
  "G = (∑i=0..q. of_int (coeff_F i) * (𝒴-ℐ-𝒯^2)^i)"
definition G_sub :: "nat⇒int mpoly" where
  "G_sub j = (∑i=j..q. of_int (coeff_F i) * of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j))"
definition H :: "int mpoly" where 
  "H = (∑j=0..q. G_sub j * ℨ^j * 𝒥^(q-j))"
definition Π :: "int mpoly" where 
  "Π = (∑j=0..q. G_sub j * (𝒮^2*𝗇 + 𝒯^2)^j * (𝒮^2*(2*ℛ-1))^(q-j))"

lemma eval_F:
  "insertion f ℱ = (∑d = 0..q. coeff_F d * (f v ^ d))"
proof -
  have aux1: " {a. lookup (mapping_of ℱ) a * (∏v. f v ^ lookup a v) ≠ 0}
    ⊆ {a ∈ range (λd. Abs_poly_mapping (λk. d when k = v)).
        lookup (mapping_of ℱ) a * (∏v. f v ^ lookup a v) ≠ 0}"
  proof -
    have "lookup (mapping_of ℱ) a ≠ 0 ⟹
         (∏v. f v ^ lookup a v) ≠ 0 ⟹
         a ∈ range (λd. Abs_poly_mapping (λk. d when k = v))" for a 
    proof -
      assume "lookup (mapping_of ℱ) a ≠ 0"
      hence "a ∈ keys (mapping_of ℱ)"
        unfolding keys.rep_eq
        by simp
      hence "⋀v'. v ≠ v' ⟹ lookup a v' = 0"
        subgoal for v'
        proof (cases "lookup a v' = 0")
          case True
          then show ?thesis by simp
        next
          case False
          assume "lookup a v' ≠ 0"
          hence "v' ∈ ⋃ (keys ` keys (mapping_of ℱ))"
            using `a ∈ keys (mapping_of ℱ)`
            unfolding keys.rep_eq
            apply simp
            apply (rule exI[where ?x=a])
            by simp
          hence 0: "v' = v"
            using F_monom_over_v vars_def
            by auto
          assume 1: "v ≠ v'"
          from 0 and 1 show ?thesis by simp
        qed
        done
      hence "a = Abs_poly_mapping (λk. (lookup a v) when k = v)"
        apply (subst lookup_inverse[symmetric])
        apply (rule arg_cong[where ?f=Abs_poly_mapping])
        by (metis (mono_tags, opaque_lifting) "when"(1) "when"(2))
      thus "a ∈ range (λd. Abs_poly_mapping (λk. d when k = v))"
        by simp
    qed
    thus ?thesis by auto
  qed

  have aux2: "lookup (mapping_of ℱ) (Abs_poly_mapping (λk. d when k = v)) ≠ 0 ⟹
    (∏va. f va ^ lookup (Abs_poly_mapping (λk. d when k = v)) va) ≠ 0 ⟹ d ∈ {0..q}" for d
  proof - 
    assume "lookup (mapping_of ℱ) (Abs_poly_mapping (λk. d when k = v)) ≠ 0"
    thus "d ∈ {0..q}"
      unfolding q_def degree.rep_eq keys.rep_eq
      apply (subst atLeastAtMost_iff)
      apply simp
      apply (rule Max_ge)
      subgoal by simp
      apply (rule insertI2)
      apply (rule image_eqI[where ?x="Abs_poly_mapping (λk. d when k = v)"])
      subgoal
        apply (subst lookup_Abs_poly_mapping)
        subgoal using finite_when[where ?f="λ_. d"] by simp
        by auto
      by simp
  qed

  have aux3: "x ≤ q ⟹ y ≤ q ⟹
    Abs_poly_mapping (λk. x when k = v) = Abs_poly_mapping (λk. y when k = v) ⟹ x = y" for x y
    proof -
      assume "Abs_poly_mapping (λk. x when k = v) = Abs_poly_mapping (λk. y when k = v)"
      hence 0: "(λk. x when k = v) = (λk. y when k = v)"
        apply (subst Abs_poly_mapping_inject[symmetric])
        subgoal
          apply (rule CollectI)
          using finite_when[where ?f="λ_. x"] by simp
        subgoal
          apply (rule CollectI)
          using finite_when[where ?f="λ_. y"] by simp
        by simp
      have "(x when v = v) = (y when v = v)"
        by (rule fun_cong[OF 0, where ?x=v])
      thus ?thesis
        by simp
    qed

  have aux4: "lookup (mapping_of ℱ) (Abs_poly_mapping (λk. d when k = v)) ≠ 0 ⟹
    (∏va. f va ^ lookup (Abs_poly_mapping (λk. d when k = v)) va) ≠ 0 ⟹
    Abs_poly_mapping (λk. d when k = v) ∈ (λd. Abs_poly_mapping (λk. d when k = v)) ` {0..q}" for d
    apply (rule image_eqI[where ?x=d, OF refl])
    using aux2 by simp

  have "insertion f ℱ = (∑m∈{a. lookup (mapping_of ℱ) a * (∏v. f v ^ lookup a v) ≠ 0}.
       lookup (mapping_of ℱ) m * (∏v. f v ^ lookup m v))"
    unfolding insertion.rep_eq insertion_aux.rep_eq insertion_fun_def
    unfolding Sum_any.expand_set
    by simp
  also have "... =
    (∑m∈{a ∈ range (λd. Abs_poly_mapping (λk. d when k = v)).
          lookup (mapping_of ℱ) a * (∏v. f v ^ lookup a v) ≠ 0}.
      lookup (mapping_of ℱ) m * (∏v. f v ^ lookup m v))"
    apply (rule sum.mono_neutral_right[symmetric])
    subgoal by auto
    subgoal using aux1 by auto
    subgoal by auto
    done
  also have "... =
    (∑m∈{a ∈ (λd. Abs_poly_mapping (λk. d when k = v)) ` {0..q}.
          lookup (mapping_of ℱ) a * (∏v. f v ^ lookup a v) ≠ 0}.
      lookup (mapping_of ℱ) m * (∏v. f v ^ lookup m v))"
    apply (rule arg_cong[where ?f="sum _"])
    apply standard
    subgoal using aux4 by auto
    subgoal by auto
    done
  also have "... =
    (∑m∈(λd. Abs_poly_mapping (λk. d when k = v)) ` {0..q}.
      lookup (mapping_of ℱ) m * (∏v. f v ^ lookup m v))"
    apply (rule sum.mono_neutral_right[symmetric])
    by auto
  also have "... =
    sum
      ((λm. lookup (mapping_of ℱ) m *
       (∏v. f v ^ lookup m v)) ∘ (λd. Abs_poly_mapping (λk. d when k = v)))
      {0..q}"
    apply (rule sum.reindex) unfolding inj_on_def using aux3 by auto
  also have "... =
    (∑d∈{0..q}. lookup (mapping_of ℱ) (Abs_poly_mapping (λk. d when k = v)) *
      (∏va. f va ^ lookup (Abs_poly_mapping (λk. d when k = v)) va))"
    by simp
  finally show ?thesis
    unfolding coeff_F_def coeff_def
    apply simp
    apply (rule arg_cong[where ?f="λf. (∑d = 0..q. _ d * f d)"])
    apply (rule ext)
    subgoal for d
      apply (subst lookup_Abs_poly_mapping)
      subgoal using finite_when[where ?f="λ_. d"] by simp
    proof (cases d)
      case 0
      then show "(∏va. f va ^ (d when va = v)) = f v ^ d"
        apply (subst `d = 0`)
        by simp
    next
      case (Suc nat)
      then show "(∏va. f va ^ (d when va = v)) = f v ^ d"
        apply (subst pow_when)
        by simp_all
    qed
    done
qed

(* Auxiliary lemma *)
lemma triangular_sum: "(∑k=0..(n::nat). (∑j=0..k. f j k)) = (∑j=0..(n::nat). (∑k=j..n. f j k))"
proof -
  have 0: "k∈{0..n} ⟹ (∑j=0..k. f j k) = (∑j=0..n. (if j≤k then f j k else 0))" for k
  proof -
    assume k_prop: "k∈{0..n}"
    hence "(∑j=0..k. f j k) = (∑j=0..k. f j k) + (∑j=(k+1)..n. 0)" by simp
    also have "... = (∑j=0..k. (if j≤k then f j k else 0)) + (∑j=(k+1)..n. (if j≤k then f j k else 0))"
      by simp
    also have "... = (∑j=0..n. (if j≤k then f j k else 0))"
      using sum.union_disjoint[of "{0..k}" "{(k+1)..n}"]
      by (smt (verit) atLeastAtMost_iff k_prop le_iff_add sum.ub_add_nat zero_order(1))
    finally show ?thesis by blast
  qed
  have 1: "j∈{0..n} ⟹ (∑k=j..n. f j k) = (∑k=0..n. (if j≤k then f j k else 0))" for j
  proof -
    assume j_prop: "j∈{0..n}"
    hence "(∑k=j..n. f j k) = (∑k<j. 0) + (∑k=j..n. f j k)" by simp
    also have "... = (∑k<j. (if j≤k then f j k else 0)) + (∑k=j..n. (if j≤k then f j k else 0))"
      by simp
    also have "... = (∑k=0..n. (if j≤k then f j k else 0))"
      using sum.union_disjoint[of "{0..<j}" "{j..n}"]
      by (smt (verit, best) atLeast0LessThan atLeastAtMost_iff finite_atLeastAtMost finite_atLeastLessThan ivl_disj_int_two(7) ivl_disj_un_two(7) j_prop)
    finally show ?thesis by blast
  qed
  hence "(∑k=0..(n::nat). (∑j=0..k. f j k)) = (∑k=0..n. (∑j=0..n. (if j≤k then f j k else 0)))"
    using 0 by simp
  also have "... = (∑j=0..n. (∑k=0..n. (if j≤k then f j k else 0)))" using sum.swap by fast
  finally show ?thesis using 1 by simp
qed


lemma G_expr:
  "G = (∑j=0..q. 𝒴^j * (∑i=j..q. of_int (coeff_F i) * of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j)))"
proof -
  have "𝒴-ℐ-𝒯^2 = 𝒴 + (-ℐ-𝒯^2)" by simp
  hence "(𝒴-ℐ-𝒯^2)^i = (∑j≤i. of_nat (i choose j) * 𝒴^j * (-ℐ-𝒯^2)^(i-j))" for i
    using binomial_ring[of 𝒴 "-ℐ-𝒯^2" i] by presburger
  hence "G = (∑i=0..q. of_int (coeff_F i) * (∑j≤i. of_nat (i choose j) * 𝒴^j * (-ℐ-𝒯^2)^(i-j)))"
    using G_def by presburger
  also have "... = (∑i=0..q. (∑j=0..i. of_int (coeff_F i) * of_nat (i choose j) * 𝒴^j * (-ℐ-𝒯^2)^(i-j) ))"
    (is "(∑i=_.._. ?f i) = (∑i=_.._. ?g i)")
  proof (rule sum.cong[OF refl])
    fix i
    have "?f i = of_int (coeff_F i) * (∑j=0..i. of_nat (i choose j) * 𝒴^j * (-ℐ-𝒯^2)^(i-j) )"
      using atMost_atLeast0 by simp
    thus "?f i = ?g i"
      unfolding mult.assoc
      by (simp add: sum_distrib_left)
  qed
  also have "... = (∑j=0..q. (∑i=j..q. of_int (coeff_F i) * of_nat (i choose j) * 𝒴^j * (-ℐ-𝒯^2)^(i-j) ))"
    using triangular_sum[of "(λj. (λi. of_int (coeff_F i) * of_nat (i choose j) * 𝒴^j * (-ℐ-𝒯^2)^(i-j)))" q]
    by blast
  also have "... = (∑j=0..q. (∑i=j..q. 𝒴^j * of_int (coeff_F i) * of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j) ))"
    apply (rule sum.cong[OF refl])
    apply (rule sum.cong[OF refl])
    by simp
  also have "... = (∑j=0..q. 𝒴^j * (∑i=j..q. of_int (coeff_F i) * of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j) ))"
    (is "(∑j=_.._. ?f j) = (∑j=_.._. ?g j)")
    apply (rule sum.cong[OF refl])
    unfolding mult.assoc
    by (simp add: sum_distrib_left)
  finally show ?thesis by simp
qed


lemma G_in_Y: "G = (∑j=0..q. 𝒴^j * G_sub j)" 
  unfolding G_sub_def using G_expr by blast

lemma Gq_eq_1: "G_sub q = 1"
proof -
  have "coeff_F q = 1" using q_def F_one unfolding coeff_F_def by simp
  have "G_sub q = of_int (coeff_F q)" unfolding G_sub_def by simp
  also have "... = of_int 1" using q_def using ‹coeff_F q = 1› by presburger
  finally show ?thesis using Const⇩0_one one_mpoly_def by simp
qed

lemma lemma_J_div_Z :
  "(∑j'=0..q. insertion f (G_sub j') * z^j' * j^(q-j')) = 0 ⟹ j dvd z" for f z j
proof (cases "j=0 ∧ z=0")
  case True
  then show ?thesis by blast
next
  case False
  assume assm: "(∑j'=0..q. insertion f (G_sub j') * z^j' * j^(q-j')) = 0"
  define d where "d = gcd j z"
  have "d dvd j" using d_def by blast
  then obtain j0 where j0_def: "j = d * j0" by blast
  have "d dvd z" using d_def by blast
  then obtain z0 where z0_def: "z = d * z0" by blast
  have "gcd j z = d * gcd j0 z0" using d_def j0_def z0_def
    by (metis abs_gcd_int gcd_mult_distrib_int)
  hence coprime: "gcd j0 z0 = 1" using d_def using False by simp

  have dn0: "d≠0" using False d_def by simp

  have "j'≤q ⟹ j' + (q-j') =q" for j' by simp
  hence nat_pow: "j'≤q ⟹ d^j' * d^(q-j') = d^q" for j' using power_add by metis
  have "z^j' * j^(q-j') = d^j' * z0^j' * d^(q-j') * j0^(q-j')" for j'
    using j0_def z0_def by (simp add: power_mult_distrib)
  hence "j'≤q ⟹ z^j' * j^(q-j') =  d^q * z0^j' * j0^(q-j')" for j'
    using power_add nat_pow by simp
  hence "0 = (∑j'=0..q. insertion f (G_sub j') * d^q * z0^j' * j0^(q-j'))"
    using assm
    by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) atLeastAtMost_iff sum.cong)
  also have "... = (∑j'=0..q. d^q * insertion f (G_sub j') * z0^j' * j0^(q-j'))"
    using mult.commute by (metis (no_types, opaque_lifting))
  also have "... = d^q * (∑j'=0..q. insertion f (G_sub j') * z0^j' * j0^(q-j'))"
    using sum_distrib_left[of "d^q" "(λj'. insertion f (G_sub j') * z0^j' * j0^(q-j'))" "{0..q}"]
    by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) sum.cong)
  finally have pol_red_0: "(∑j'=0..q. insertion f (G_sub j') * z0^j' * j0^(q-j')) = 0"
    using dn0 by simp

  have inser_Gq_1: "insertion f (G_sub q) = 1" using Gq_eq_1 by simp
  have j0_pow: "j'<q ⟹ j0^(q-j') = j0^(q-j'-1) * j0" for j'
    by (metis power_minus_mult zero_less_diff)
  have "(∑j'=0..q. insertion f (G_sub j') * z0^j' * j0^(q-j'))
        = (∑j'=0..<q. insertion f (G_sub j') * z0^j' * j0^(q-j')) + insertion f (G_sub q) * z0^q * j0^(q-q)"
    by (simp add: sum.last_plus)
  also have "... = (∑j'=0..<q. insertion f (G_sub j') * z0^j' * j0^(q-j')) + z0^q"
    using inser_Gq_1 by simp
  also have "... = (∑j'=0..<q. insertion f (G_sub j') * z0^j' * j0^(q-j'-1)*j0) + z0^q"
    using j0_pow sum.cong by (simp add: ab_semigroup_mult_class.mult_ac(1))
  also have "... = (∑j'=0..<q. insertion f (G_sub j') * z0^j' * j0^(q-j'-1)) * j0 + z0^q"
    using sum_distrib_right[of _ _ "j0"] by metis
  finally have "z0^q = -(∑j'=0..<q. insertion f (G_sub j') * z0^j' * j0^(q-j'-1)) * j0"
    using pol_red_0 by simp
  hence "j0 dvd z0^q" by simp
  hence "j0 dvd z0" using coprime
    by (metis coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff coprime_power_right_iff is_unit_gcd one_dvd)
  thus "j dvd z" using j0_def z0_def by simp
qed

lemma lemma_pos: 
  assumes "(∑j'=0..q. insertion f (G_sub j') * z^j' * j^(q-j')) = 0"
          "j≠0" "z = z' * j"
  shows "insertion (λ_. z' - f 7 - (f 5)^2) ℱ = 0"
proof -
  have "z^j' = z'^j' * j^j'" for j' using power_mult_distrib[of "z'" "j" "j'"] assms by blast
  hence 0: "0 = (∑j'=0..q. insertion f (G_sub j') * z'^j' * j^j' * j^(q-j'))" using assms
    by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) sum.cong)
  also have "... = (∑j'=0..q. insertion f (G_sub j') * z'^j' * j^(j'+(q-j')))"
    using power_add[of "j"] by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1))
  also have "... = (∑j'=0..q. insertion f (G_sub j') * z'^j' * j^q)" by simp
  also have "... = (∑j'=0..q. insertion f (G_sub j') * z'^j') * j^q"
    using sum_distrib_right[of _ _ "j^q"] by metis
  finally have G_is_0: "(∑j'=0..q. insertion f (G_sub j') * z'^j') = 0" using assms by simp

  define f' where "f' = (λx. f x)(8:=z')" (* variable 8 is Y *)
  hence "insertion f' 𝒴 = z'"
    by (simp add: 𝒴_def)
  hence ins_f'_Y: "insertion f' (𝒴^j') = z'^j'" for j'::nat using insertion_pow by blast
  have ins_f'_Gsub: "insertion f' (G_sub j') = insertion f (G_sub j')" for j'
  (* Basically f and f' only differ on Y, and G_sub doesn't contain Y *)
  (* A better proof could be done with lemma insertion_irrelevant_vars *)
  proof (rule insertion_irrelevant_vars)
    fix v
    assume H: "v ∈ vars (G_sub j')"
    have "vars (G_sub j') ⊆ vars ℐ ∪ vars 𝒯"
      unfolding G_sub_def
      apply (rule subset_trans[OF vars_setsum])
      subgoal by simp
      apply (rule union_subset)
      subgoal for x
        apply (rule subset_trans[OF vars_mult])
        apply (rule Un_least)
         apply (rule subset_trans[OF vars_mult])
         apply (subst of_int_Const)
         apply (subst of_nat_Const)
        using vars_Const
        subgoal by simp
        apply (rule subset_trans[OF vars_pow])
        apply (subst diff_conv_add_uminus)
        apply (rule subset_trans[OF vars_add])
        apply (rule Un_mono)
        using vars_neg
        subgoal by auto
        apply (subst vars_neg)
        apply (subst power2_eq_square)
        apply (rule subset_trans[OF vars_mult])
        by simp
      done
    also have "... ⊆ {5, 7}"
      unfolding defs
      unfolding MPoly_Type.Var.abs_eq[symmetric]
      by simp
    finally have "v ≠ 8"
      using H
      by auto
    thus "f' v = f v"
      unfolding f'_def
      by auto
  qed

  have "(∑j'=0..q. insertion f' (G_sub j') * insertion f' (𝒴^j')) = 0"
    using ins_f'_Y ins_f'_Gsub G_is_0 by presburger
  hence "(∑j'=0..q. insertion f' (G_sub j' * 𝒴^j')) = 0"
    using insertion_mult by (metis (no_types, lifting) sum.cong)
  hence "insertion f' (∑j'=0..q. G_sub j' * 𝒴^j') = 0" using insertion_sum[of "{0..q}" "f'"] by simp
  hence "insertion f' G = 0" using G_in_Y mult.commute
    by (metis (no_types, lifting) sum.cong)

  hence "(∑i = 0..q. insertion f' (of_int (coeff_F i) * (𝒴 - ℐ - 𝒯⇧2) ^ i)) = 0"
    unfolding G_def using insertion_sum[of "{0..q}" "f'"] by simp 
  hence "(∑i = 0..q. coeff_F i * insertion f' ((𝒴 - ℐ - 𝒯⇧2) ^ i)) = 0"
    by simp
  hence 1: "(∑i = 0..q. coeff_F i * (insertion f' (𝒴 - ℐ - 𝒯⇧2)) ^ i) = 0"
    using insertion_pow[of "f'"] by simp
  
  have "insertion f' (𝒴 - ℐ - 𝒯⇧2) = z' - f 7 - (f 5)^2"
  proof -
    have "insertion f' (𝒴 - ℐ - 𝒯⇧2) = insertion f' 𝒴 + insertion f' (-ℐ-𝒯*𝒯)"
      using insertion_add[of "f'" 𝒴 "-ℐ-𝒯*𝒯"] power2_eq_square[of 𝒯] add.assoc
      by (metis ab_group_add_class.ab_diff_conv_add_uminus)
    also have "... = insertion f' 𝒴 - insertion f' ℐ - insertion f' (𝒯*𝒯)"
      by simp
    also have "... = insertion f' 𝒴 - insertion f' ℐ - (insertion f' 𝒯)^2"
      using insertion_mult[of "f'" 𝒯 𝒯] power2_eq_square by metis
    also have "... = f' 8 - f' 7 - (f' 5)^2"
      unfolding 𝒴_def ℐ_def 𝒯_def by simp
    finally show ?thesis using f'_def by simp
  qed

  hence "(∑i = 0..q. coeff_F i * (z' - f 7 - (f 5)^2) ^ i) = 0" using 1 by simp
  thus "insertion (λ_. z' - f 7 - (f 5)^2) ℱ = 0"
    using q_def eval_F
    by simp
qed

lemma Π_encodes_correctly:
  fixes S T R I :: int
  assumes "S ≠ 0" 
          "(∀x. insertion (λ_. x) ℱ = 0 ⟶ x > -I)"
      and "S dvd T"
          "R > 0"
          "insertion (λ_. y) ℱ = 0"
  defines "φ n ≡ (λ_. 0)(4:= S, 5:=T, 6:=R, 7:=I, 11:=int n)"
  shows "∃n :: nat. insertion (φ n) Π = 0 ∧ n = (2*R-1)*(y + I + T^2) - (T div S) ^ 2"
proof -
  obtain TdS where TdS_def: "T = TdS * S" using ‹S dvd T› by force
  define n⇩i where "n⇩i = (2*R-1)*(y+I+T^2) - TdS^2"
  have nBe0: "n⇩i≥0"
  proof -
    have 0: "(2*R-1) ≥ 1" using assms by simp
    have "y > -I" using assms by blast
    hence 1: "y+I+T^2 > T^2" by linarith
    have "T^2 ≥0" by simp
    hence "y+I+T^2 > 0" using 1 by linarith
    hence "(2*R-1)*(y+I+T^2) ≥ y+I+T^2" using 0 by simp
    hence 2: "(2*R-1)*(y+I+T^2) ≥ T^2" using 1 by simp

    have 3: "T^2 = TdS^2 * S^2" unfolding TdS_def using power_mult_distrib by blast
    have "S^2 > 0" using assms by simp
    hence 4: "S^2 ≥ 1" by linarith
    have "TdS^2 ≥ 0" by simp
    hence "TdS^2 * S^2 ≥ TdS^2" using 4 by (metis mult_cancel_left1 mult_left_mono)
    hence "T^2 ≥ TdS^2" using 3 by simp

    thus ?thesis unfolding n⇩i_def using 2 by simp
  qed
  then obtain n where n_def: "int n = n⇩i" using nonneg_int_cases by metis

  define f::"nat⇒int" where "f = (λ_. 0) (4 := S, 5 := T, 6 := R, 7 := I, 11 := int n)"
  have 0: "insertion f Π
  = (∑j = 0..q. insertion f (G_sub j * (𝒮⇧2 * 𝗇 + 𝒯⇧2) ^ j * (𝒮⇧2 * (2 * ℛ - 1)) ^ (q - j)))"
    unfolding Π_def using insertion_sum by blast
  have 1: "insertion f (G_sub j * (𝒮⇧2 * 𝗇 + 𝒯⇧2) ^ j * (𝒮⇧2 * (2 * ℛ - 1)) ^ (q - j))
       = insertion f (G_sub j) * (S^2 * n + T^2)^j * (S^2 * (2*R- 1)) ^ (q - j)" for j
  proof -
    have 0: "insertion f (G_sub j * (𝒮⇧2 * 𝗇 + 𝒯⇧2) ^ j * (𝒮⇧2 * (2 * ℛ - 1)) ^ (q - j))
       = insertion f (G_sub j) * insertion f ((𝒮⇧2 * 𝗇 + 𝒯⇧2) ^ j) * insertion f ((𝒮⇧2 * (2 * ℛ - 1)) ^ (q - j))"
      using insertion_mult[of f] by simp
    have 1: "insertion f ((𝒮⇧2 * 𝗇 + 𝒯⇧2) ^ j) * insertion f ((𝒮⇧2 * (2 * ℛ - 1)) ^ (q - j))
        = (insertion f (𝒮⇧2 * 𝗇 + 𝒯⇧2)) ^ j * (insertion f (𝒮⇧2 * (2 * ℛ - 1))) ^ (q - j)"
      using insertion_pow by metis
    have "insertion f (𝒮⇧2 * 𝗇 + 𝒯⇧2) = insertion f (𝒮*𝒮) * insertion f 𝗇 + insertion f (𝒯*𝒯)"
      using insertion_add[of f] insertion_mult[of f] power2_eq_square by metis
    also have "... = (insertion f 𝒮)^2 * insertion f 𝗇 + (insertion f 𝒯)^2"
      using insertion_mult[of f] power2_eq_square by metis
    also have "... = S^2 * n + T^2"
      unfolding 𝒮_def 𝗇_def 𝒯_def using f_def by simp
    finally have 2: "insertion f (𝒮⇧2 * 𝗇 + 𝒯⇧2) = S^2 * n + T^2" by simp
    have "insertion f (𝒮⇧2 * (2 * ℛ - 1)) = (insertion f 𝒮)^2 * insertion f (2 * ℛ - 1)"
      using insertion_mult[of f] power2_eq_square by metis
    also have "... = (insertion f 𝒮)^2 * (insertion f (2*ℛ) - insertion f 1)"
      by simp
    also have "... = (insertion f 𝒮)^2 * (2 * insertion f ℛ - 1)"
      by (simp add: insertion_mult[of f])
    also have "... = S^2 * (2*R-1)"
      unfolding 𝒮_def ℛ_def using f_def by simp
    finally have 3: "insertion f (𝒮⇧2 * (2 * ℛ - 1)) = S^2 * (2*R-1)" by simp
    show ?thesis using 0 1 2 3 by simp
  qed
  have 2: "j≤q ⟹ (S^2 * n + T^2)^j * (S^2 * (2*R- 1)) ^ (q - j)
      = (y+I+T^2)^j * (S^2 * (2*R- 1)) ^ q" for j
  proof -
    assume jLeq: "j≤q"
    have "S^2 * n + T^2 = S^2*(2*R-1)*(y+I+T^2) - S^2 * TdS^2 + T^2" unfolding n_def n⇩i_def
      by (simp add: right_diff_distrib)
    also have "... = S^2*(2*R-1)*(y+I+T^2) - (S* TdS)^2 + T^2" using power_mult_distrib by metis
    also have "... = S^2*(2*R-1)*(y+I+T^2)" using TdS_def by (simp add: mult.commute)
    finally have "(S^2 * n + T^2)^j * (S^2 * (2*R- 1)) ^ (q - j)
      = (S^2*(2*R-1)*(y+I+T^2))^j * (S^2 * (2*R- 1)) ^ (q - j)" by simp
    also have "... = (y+I+T^2)^j * (S^2*(2*R-1))^j * (S^2 * (2*R- 1)) ^ (q - j)"
      using power_mult_distrib mult.commute by metis
    also have "... = (y+I+T^2)^j * (S^2 * (2*R- 1))^q" using power_add jLeq
      by (metis (no_types, lifting) add_diff_cancel_left' mult.assoc nat_le_iff_add)
    finally show ?thesis by simp
  qed           
  hence "insertion f Π
       = (∑j = 0..q. insertion f (G_sub j) * (S^2 * n + T^2)^j * (S^2 * (2*R- 1)) ^ (q - j))"
    using 0 1 by presburger
  also have "... = (∑j = 0..q. insertion f (G_sub j) * (y+I+T^2)^j * (S^2 * (2*R- 1)) ^ q)"
    using 2 by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) atLeastAtMost_iff sum.cong)
  finally have inser_expr_1: "insertion f Π =
              (∑j = 0..q. insertion f (G_sub j) * (y+I+T^2)^j) * (S^2 * (2*R- 1)) ^ q"
    using sum_distrib_right[of _ _ "(S^2 * (2*R- 1)) ^ q"] by metis

  have inser_G_sub:  "insertion f (G_sub j) = (∑i=j..q. coeff_F i * of_nat (i choose j) * (-I-T^2)^(i-j))"
    for j
  proof -
    have "insertion f (G_sub j)
        = insertion f (∑i=j..q. of_int (coeff_F i) * of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j))"
      unfolding G_sub_def by blast 
    also have "... = (∑i=j..q. insertion f (of_int (coeff_F i) * of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j)))"
      using insertion_sum by blast
    also have "... = (∑i=j..q. (coeff_F i) * of_nat (i choose j) * insertion f ((-ℐ-𝒯^2)^(i-j)))"
    proof -
      have 1: "insertion f (of_int (coeff_F i) * of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j))
         = (coeff_F i) * insertion f (of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j))" for i
        using mult.assoc insertion_of_int_times by metis
      moreover have "(coeff_F i) * insertion f (of_nat (i choose j) * (-ℐ-𝒯^2)^(i-j))
         = (coeff_F i) * (i choose j) * insertion f ((-ℐ-𝒯^2)^(i-j))" for i
          using insertion_mult 
          by (smt (verit) ab_semigroup_mult_class.mult_ac(1) insertion_of_int_times mult.commute 
              of_int_of_nat_eq) 
      ultimately show ?thesis by presburger
    qed
    also have "... = (∑i=j..q. (coeff_F i) * of_nat (i choose j) * (insertion f (-ℐ-𝒯^2))^(i-j))"
    proof -
      have "insertion f ((-ℐ-𝒯^2)^(i-j)) = (insertion f (-ℐ-𝒯^2))^(i-j)" for i
        using insertion_pow by blast
      thus ?thesis by simp
    qed
    also have "... = (∑i=j..q. (coeff_F i) * of_nat (i choose j) * (-insertion f ℐ - (insertion f 𝒯) ^2 )^(i-j))"
    proof -
      have "insertion f (-ℐ-𝒯^2) = -insertion f (ℐ + 𝒯^2)" by simp
      also have "... = -insertion f ℐ - (insertion f (𝒯^2))" by simp
      finally have "insertion f (-ℐ-𝒯^2) = -insertion f ℐ - (insertion f 𝒯) ^2"
        using insertion_mult[of "f" 𝒯 𝒯] power2_eq_square by metis
      thus ?thesis by simp
    qed
    also have "... = (∑i=j..q. coeff_F i * of_nat (i choose j) * (-I-T^2)^(i-j))"
      unfolding defs using f_def by simp
    finally show ?thesis by blast
  qed

  hence "(∑j = 0..q. insertion f (G_sub j) * (y+I+T^2)^j)
      = (∑j = 0..q. (∑i=j..q. coeff_F i * of_nat (i choose j) * (-I-T^2)^(i-j)) * (y+I+T^2)^j)"
    using inser_G_sub by presburger
  also have "... = (∑j = 0..q. (∑i=j..q. coeff_F i * of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j))"
  proof -
    have "(∑i=j..q. coeff_F i * of_nat (i choose j) * (-I-T^2)^(i-j)) * (y+I+T^2)^j
         = (∑i=j..q. coeff_F i * of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j)" for j
      using sum_distrib_right by blast
    thus ?thesis by presburger
  qed
  also have "... = (∑i = 0..q. (∑j=0..i. coeff_F i * of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j))"
    using triangular_sum[of "(λj. (λi. coeff_F i * of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j))" q]
    by argo
  also have "... = (∑i = 0..q. coeff_F i * (∑j=0..i. of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j))"
  proof -
    have "(∑j=0..i. coeff_F i *  of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j)
         = coeff_F i * (∑j=0..i. of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j)" for i
      using sum_distrib_left[of "coeff_F i" "(λj. of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j)" "{0..i}"]
      by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) sum.cong)
    thus ?thesis by presburger
  qed
  also have "... = (∑i = 0..q. coeff_F i * y^i)"
  proof -
    have "(∑j=0..i. of_nat (i choose j) * (-I-T^2)^(i-j) * (y+I+T^2)^j) = y^i" for i
      using binomial_ring[of "y+I+T^2" "-I-T^2" i]
      by (smt (verit, best) ab_semigroup_mult_class.mult_ac(1) atLeast0AtMost mult.commute sum.cong)
    thus ?thesis by simp
  qed
  also have "... = insertion (λ_. y) ℱ" using q_def eval_F by metis
  also have "... = 0" using assms by blast
  finally have "insertion f Π = 0" using inser_expr_1 by presburger

  hence "insertion (φ n) Π = 0" 
    unfolding f_def φ_def by auto

  moreover have "n = (2*R-1)*(y + I + T^2) - (T div S) ^ 2" 
    unfolding n_def n⇩i_def TdS_def using ‹S ≠ 0› by auto

  ultimately show "?thesis" by auto
qed



lemma Π_encodes_correctly_2:
  fixes S T R I :: int
  assumes "S ≠ 0" 
          "(∀x. insertion (λ_. x) ℱ = 0 ⟶ x > -I)"
  defines "φ n ≡ (λ_. 0)(4:= S, 5:=T, 6:=R, 7:=I, 11:=int n)"
  assumes "∃n :: nat. insertion (φ n) Π = 0"
  shows "S dvd T ∧ R > 0 ∧ (∃x::int. (insertion (λ_. x) ℱ) = 0)"
proof - 
  from assms obtain n where 
    prop_2_n: "insertion ((λ_. 0) (4 := S, 5:=T, 6:=R, 7:= I, 11:= int n)) Π = 0"
    unfolding φ_def by auto
  define subst::"nat⇒int" where "subst = ((λ_. 0) (4 := S, 5 := T, 6 := R, 7 := I, 11 := n))"
  define J::int where "J = S^2 * (2*R-1)"
  have "2*R-1 ≠ 0" by presburger
  hence Jnot0: "J≠0" unfolding J_def using assms by simp

  have "0 = insertion subst (∑j=0..q. G_sub j * (𝒮^2 * 𝗇 + 𝒯^2)^j * (𝒮^2*(2*ℛ-1))^(q-j))"
    using prop_2_n unfolding Π_def[symmetric] subst_def by argo
  also have "... = (∑j=0..q. insertion subst (G_sub j * (𝒮^2 * 𝗇 + 𝒯^2)^j * (𝒮^2*(2*ℛ-1))^(q-j)))"
    using insertion_sum by blast
  also have "... = (∑j=0..q. insertion subst (G_sub j) * insertion subst ((𝒮^2 * 𝗇 + 𝒯^2)^j * (𝒮^2*(2*ℛ-1))^(q-j)))"
  proof -
    have "insertion subst (G_sub j * (𝒮^2 * 𝗇 + 𝒯^2)^j * (𝒮^2*(2*ℛ-1))^(q-j))
          = insertion subst (G_sub j) * insertion subst ((𝒮^2 * 𝗇 + 𝒯^2)^j * (𝒮^2*(2*ℛ-1))^(q-j))" for j
      using insertion_mult[of subst] by simp
    thus ?thesis by presburger
  qed
  also have "... = (∑j=0..q. insertion subst (G_sub j) * (S^2 * n + T^2)^j * (S^2*(2*R-1))^(q-j))"
  proof -
    have "insertion subst ((𝒮^2 * 𝗇 + 𝒯^2)^j * (𝒮^2*(2*ℛ-1))^(q-j)) = (S^2 * n + T^2)^j * (S^2*(2*R-1))^(q-j)" for j
    proof -
    have 0: "insertion subst ((𝒮⇧2 * 𝗇 + 𝒯⇧2) ^ j * (𝒮⇧2 * (2 * ℛ - 1)) ^ (q - j))
       = insertion subst ((𝒮⇧2 * 𝗇 + 𝒯⇧2) ^ j) * insertion subst ((𝒮⇧2 * (2 * ℛ - 1)) ^ (q - j))"
      using insertion_mult[of subst] by simp
    have 1: "insertion subst ((𝒮⇧2 * 𝗇 + 𝒯⇧2) ^ j) * insertion subst ((𝒮⇧2 * (2 * ℛ - 1)) ^ (q - j))
        = (insertion subst (𝒮⇧2 * 𝗇 + 𝒯⇧2)) ^ j * (insertion subst (𝒮⇧2 * (2 * ℛ - 1))) ^ (q - j)"
      using insertion_pow by metis
    have "insertion subst (𝒮⇧2 * 𝗇 + 𝒯⇧2) = insertion subst (𝒮*𝒮) * insertion subst 𝗇 + insertion subst (𝒯*𝒯)"
      using insertion_add[of subst] insertion_mult[of subst] power2_eq_square by metis
    also have "... = (insertion subst 𝒮)^2 * insertion subst 𝗇 + (insertion subst 𝒯)^2"
      using insertion_mult[of subst] power2_eq_square by metis
    also have "... = S^2 * n + T^2"
      unfolding 𝒮_def 𝗇_def 𝒯_def using subst_def by simp
    finally have 2: "insertion subst (𝒮⇧2 * 𝗇 + 𝒯⇧2) = S^2 * n + T^2" by simp
    have "insertion subst (𝒮⇧2 * (2 * ℛ - 1)) = (insertion subst 𝒮)^2 * insertion subst (2 * ℛ - 1)"
      using insertion_mult[of subst] power2_eq_square by metis
    also have "... = (insertion subst 𝒮)^2 * (insertion subst (2*ℛ) - insertion subst 1)"
      by simp
    also have "... = (insertion subst 𝒮)^2 * (2 * insertion subst ℛ - 1)"
      using insertion_of_int_times[of subst 2] by simp
    also have "... = S^2 * (2*R-1)"
      unfolding 𝒮_def ℛ_def using subst_def by simp
    finally have 3: "insertion subst (𝒮⇧2 * (2 * ℛ - 1)) = S^2 * (2*R-1)" by simp
      show ?thesis using 0 1 2 3 by argo
    qed
    thus ?thesis using sum.cong by (simp add: ab_semigroup_mult_class.mult_ac(1))
  qed
  finally have Π_eq_0: "(∑j=0..q. insertion subst (G_sub j) * (S^2 * n + T^2)^j * (S^2*(2*R-1))^(q-j)) = 0"
    by simp
  hence J_div_ST: "J dvd S^2 * n + T^2" using lemma_J_div_Z unfolding J_def by blast
  hence "S^2 dvd S^2 * n + T^2" unfolding J_def by fastforce
  hence "S^2 dvd (S^2*n + T^2) - S^2*n" by fastforce
  hence "S^2 dvd T^2" by simp
  hence S_dvd_T: "S dvd T" by simp

  obtain Z::int where Z_prop: "S^2 * n + T^2 = Z * J" using J_div_ST by fastforce
  hence "insertion (λ_. Z - subst 7 - (subst 5)^2) ℱ = 0"
    using Π_eq_0 Jnot0 lemma_pos[of subst "S^2*n+T^2" "J" "Z"]
    unfolding J_def by blast
  hence F_cancels: "insertion (λ_. Z - I - T^2) ℱ = 0"
    unfolding subst_def by simp
  hence "Z - I - T^2 > -I"
    using assms by blast           
  hence "Z > T^2" by simp
  hence "Z ≠ 0" by fastforce
  hence SnT_not_0: "S^2 * n + T^2 ≠ 0" using Z_prop Jnot0 by simp
  have Snt: "S^2 * n + T^2 ≥ 0" using prop_2_n by simp
  hence SnT_B_0: "S^2 * n + T^2 > 0" using SnT_not_0 by linarith
  have "T^2 ≥0" by simp
  hence ZB0:"Z > 0" using ‹Z > T^2› by linarith
  hence "J≤0 ⟹ False"
  proof -
    assume "J≤0"
    hence "J<0" using Jnot0 by simp
    hence "S^2 * n + T^2 < 0" using Z_prop ZB0 
      by (metis SnT_B_0 one_dvd plus_int_code(2) zdvd_not_zless zero_less_mult_pos zless_add1_eq)
    thus "False" using Snt by simp
  qed
  hence JB0:"J>0" by fastforce
  hence "S^2 * (2 * R- 1) > 0" unfolding J_def by blast
  hence "2 * R- 1 > 0"
    by (metis mult_eq_0_iff zero_eq_power2 zero_less_mult_pos zero_less_power2)
  hence "2*R > 0" by simp
  hence RB0: "R > 0" by simp
  thus "?thesis" using S_dvd_T RB0 F_cancels by blast
qed

end

end