Theory Nine_Unknowns_N_Z_Definitions

theory Nine_Unknowns_N_Z_Definitions
  imports "../Coding_Theorem/Coding_Theorem_Definitions" "../Bridge_Theorem/Bridge_Theorem_Imp"
    "M3_Polynomial" "../Coding/Suitable_For_Coding" "../MPoly_Utils/Poly_Degree"
    "HOL-Eisbach.Eisbach"
begin

section ‹Nine Unknowns over $\mathbb{N}$ and $\mathbb{Z}$›

subsection ‹Combining all previous constructions›

text ‹For any appropriately typed function F, we introduce the syntax 
  ‹fn τ ≡ fn a f g h k l w x y n›, as well as ‹(λτ. e) ≡ (λf a f g h k l w x y n. e)›.›

syntax "tau" :: "(int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int) ⇒ int" ("_ τ" [1000] 1000)
syntax "tau_fn" :: "(int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int) ⇒ int" ("λτ. _" [0] 0)

parse_translation ‹
  [
    (
      \<^syntax_const>‹tau›,
      fn ctxt => fn args =>
        list_comb (
          args |> hd,
          ["a", "f", "g", "h", "k", "l", "w", "x", "y", "n"] |> map (fn name => Free (name, @{typ int}))
        )
    ),
    (
      \<^syntax_const>‹tau_fn›,
      fn ctxt => fn args =>
        ["a", "f", "g", "h", "k", "l", "w", "x", "y", "n"]
          |> List.foldr (fn (name, r) => Abs (name, @{typ int}, r)) (args |> hd)
    )
  ]
›


locale combined_variables =
  fixes P :: "int mpoly"
begin

text ‹Copy of the polynomials from Theorem I›


definition P⇩1 :: "int mpoly" where 
  "P⇩1 ≡ suitable_for_coding P"

abbreviation "δ ≡ coding_variables.δ P⇩1"
abbreviation "ν ≡ coding_variables.ν P⇩1"

definition b :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "b τ = coding_variables.b a f"
definition X :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "X τ = coding_variables.X P⇩1 a f g"
definition Y :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "Y τ = coding_variables.Y P⇩1 a f"

poly_extract b

(* The following is the manual equivalent of poly_extract Y *)
definition Y_poly :: "int mpoly" where 
  "Y_poly ≡ coding_variables.Y_poly P⇩1"
lemma Y_correct: "insertion f Y_poly =  Y (f 0) (f 1) (f 2) (f 3) (f 4) (f 5) (f 6) (f 7) (f 8) (f 9)"
  unfolding Y_def coding_variables.Y_correct Y_poly_def by simp


(* The following is the manual equivalent of poly_extract X *)
definition X_poly :: "int mpoly" where 
  "X_poly ≡ coding_variables.X_poly P⇩1"
lemma X_correct: "insertion f X_poly =  X (f 0) (f 1) (f 2) (f 3) (f 4) (f 5) (f 6) (f 7) (f 8) (f 9)"
  unfolding X_def coding_variables.X_correct X_poly_def by simp


(* The following lemma uses an abbreviation, which does not work for use in literal facts. *) 
lemma δ_gt0: "δ > 0"
  unfolding coding_variables.δ_def P⇩1_def
  by (simp add: suitable_for_coding_total_degree)


text ‹Polynomials from Theorem II›

definition L :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "L τ = bridge_variables.L l (Y τ)"
definition U :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "U τ = bridge_variables.U l (X τ) (Y τ)"
definition V :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "V τ = bridge_variables.V w g (Y τ)"
definition A :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "A τ = bridge_variables.A l w g (Y τ) (X τ)"
definition C :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "C τ = bridge_variables.C l w h g (Y τ) (X τ)"
definition D :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "D τ = bridge_variables.D l w h g (Y τ) (X τ)"
definition F :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "F τ = bridge_variables.F l w h x g (Y τ) (X τ)"
definition I :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "I τ = bridge_variables.I l w h x y g (Y τ) (X τ)"
definition W :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "W τ = bridge_variables.W w (coding_variables.b a f)"
definition K :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "K τ = bridge_variables.K k l w g (Y τ) (X τ)"

poly_extract L
poly_extract U
poly_extract V
poly_extract A
poly_extract C
poly_extract D
poly_extract F
poly_extract I
poly_extract W
poly_extract K

text ‹Variables in the proof of Theorem III›

definition M3 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "M3 A⇩1 A⇩2 A⇩3 S T Q' m = insertion_list [A⇩1, A⇩2, A⇩3, S, T, Q', m] section5.M3_poly"

(* This poly_extract just recovers M3_poly as section5.M3_poly, up to an
   identity substitution. *)
(* This construction does simplify the lemma on the maximum variable index just afterwards. *)
poly_extract M3

lemma max_vars_M3: "max_vars M3_poly ≤ 6"
  unfolding M3_poly_def
  using max_vars_id[of 6, unfolded upt_def]
  by auto

definition μ :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "μ τ = (coding_variables.γ P⇩1) * (b τ) ^ (coding_variables.α P⇩1)"

poly_extract μ

definition A⇩1 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "A⇩1 τ = b τ"
definition A⇩2 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "A⇩2 τ = (D τ) * (F τ) * (I τ)"
definition A⇩3 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "A⇩3 τ = ((U τ) ^ 4 * (V τ)⇧2 - 4) * (K τ)⇧2 + 4"
definition S :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "S τ = bridge_variables.S l w g (Y τ) (X τ)"
definition T :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "T τ = bridge_variables.T l w h g (Y τ) (X τ) (b τ)"
definition R :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "R τ = f⇧2 * l⇧2 * x⇧2 * (8 * (μ τ)^3 * g * (K τ)⇧2 - g⇧2 * (32 * ((C τ) - (K τ) * (L τ))^2 * (μ τ)^3 + g⇧2 * (K τ)⇧2))"
definition m :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "m τ = n"

poly_extract A⇩1
poly_extract A⇩2
poly_extract A⇩3
poly_extract S
poly_extract T
poly_extract R
poly_extract m


definition σ :: "(int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int) ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "(σ fn) τ = fn (A⇩1 τ) (A⇩2 τ) (A⇩3 τ) (S τ) (T τ) (R τ) (m τ)"

definition Q :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "Q τ = M3 (A⇩1 τ) (A⇩2 τ) (A⇩3 τ) (S τ) (T τ) (R τ) (m τ)"

lemma M_poly_degree_correct: "total_degree (coding_variables.M_poly P⇩1) ≤ (1+(δ+1)^ν) * 2*δ"
  using δ_gt0 coding_variables.M_poly_degree_correct by blast 

lemma D_poly_degree_correct: "total_degree (coding_variables.D_poly P⇩1) ≤ (δ+1)^(ν+1) * (2*δ)"
  using δ_gt0 coding_variables.D_poly_degree_correct by blast 

lemma K_poly_degree_correct: "total_degree (coding_variables.K_poly P⇩1)
  ≤ max (δ*(1+2*δ) + (δ+1)^(ν+1) * 2*δ) ((1 + (2*δ+1)*(δ+1)^ν) * 2*δ)"
  using δ_gt0 coding_variables.K_poly_degree_correct by blast 


(* Because the polynomial Q is too complicated, we introduced these fixed degree_correct lemmas. *)
poly_degree X_poly
poly_degree Y_poly

lemma X_poly_degree_alt: "X_poly_degree = 12 * δ + 12 * δ * Suc δ ^ ν + 12 * δ⇧2 * Suc δ ^ ν" 
    if "δ > 0"
proof - 
  have step0: "X_poly_degree 
    = δ + δ + Suc δ ^ ν * (δ + δ) + (δ + δ + (Suc δ ^ ν + 2 * δ * Suc δ ^ ν) * (δ + δ)) +
    max (max (max (Suc 0)
               (max (δ + δ * (2 * δ) + (Suc δ ^ ν * 2 + δ * Suc δ ^ ν * 2) * δ)
                 (δ + (δ + (Suc δ ^ ν * 2 + 4 * (δ * Suc δ ^ ν)) * δ)) +
                (δ + δ + Suc δ ^ ν * (δ + δ))))
          (max (2 * δ + Suc δ ^ ν * 2 * δ)
            (δ + δ + (Suc δ ^ ν + δ * Suc δ ^ ν) * (δ + δ) +
             (δ + δ + Suc δ ^ ν * (δ + δ)))) +
         (δ + δ + Suc δ ^ ν * (δ + δ) +
          (δ + δ + (Suc δ ^ ν + 2 * δ * Suc δ ^ ν) * (δ + δ))))
     (max (2 * δ + Suc δ ^ ν * 2 * δ)
       (δ + δ + (Suc δ ^ ν + δ * Suc δ ^ ν) * (δ + δ) + (δ + δ + Suc δ ^ ν * (δ + δ))))"
    by (simp add: X_poly_degree_def) (* takes long! *)
    
  have step1: "max (2 * δ + Suc δ ^ ν * 2 * δ) 
               (δ + δ + (Suc δ ^ ν + δ * Suc δ ^ ν) * (δ + δ) + (δ + δ + Suc δ ^ ν * (δ + δ))) 
        = 4 * δ + 2 * (δ^2 + 2*δ) * Suc δ ^ ν" 
    using that apply (simp add: ab_semigroup_mult_class.mult_ac(1) mult_2)
    by (smt (verit, del_insts) ab_semigroup_mult_class.mult_ac(1) add.commute add.left_commute 
        mult.commute mult_2_right mult_Suc power2_eq_square)

  have step2: "max (δ + δ * (2 * δ) + (Suc δ ^ ν * 2 + δ * Suc δ ^ ν * 2) * δ)
               (δ + (δ + (Suc δ ^ ν * 2 + 4 * (δ * Suc δ ^ ν)) * δ))
        = 2 * δ  + 2 * δ * Suc δ ^ ν + 4 * δ⇧2 * Suc δ ^ ν"
  proof - 
    have aux1: "max (δ + (δ * (δ * 2) + (δ * (2 * Suc δ ^ ν) + δ * (δ * (2 * Suc δ ^ ν)))))
     (δ * 2 + (δ * (2 * Suc δ ^ ν) + δ * (δ * (4 * Suc δ ^ ν))))
    = δ + δ * (2 * Suc δ ^ ν) + 
      max (δ * (δ * 2) + δ * (δ * (2 * Suc δ ^ ν))) (δ + δ * (δ * (4 * Suc δ ^ ν)))"
      using nat_add_max_right by presburger
    have aux2: "max (δ * (δ * 2) + δ * (δ * (2 * Suc δ ^ ν))) (δ + δ * (δ * (4 * Suc δ ^ ν))) = 
          2 * δ^2 * Suc δ ^ ν + max (2 * δ^2) (δ + 2 * δ^2 * Suc δ ^ ν)" 
      by (simp add: mult.commute mult.left_commute power2_eq_square)
    have aux3: "max (2 * δ⇧2) (δ + 2 * δ⇧2 * Suc δ ^ ν) = δ + 2 * δ⇧2 * Suc δ ^ ν"
      apply (rule linorder_class.max.absorb2)
      by (simp add: trans_le_add2)
    show ?thesis 
      apply (simp add: algebra_simps)
      unfolding aux1 aux2 aux3
      by (simp add: algebra_simps)
  qed

  have step3: "max (Suc 0) (2 * δ + 2 * δ * Suc δ ^ ν + 4 * δ⇧2 * Suc δ ^ ν + (δ + δ + Suc δ ^ ν * (δ + δ)))
            = δ * 4 + δ * 4 * Suc δ ^ ν + 4 * δ⇧2 * Suc δ ^ ν"
  proof - 
    have "max (Suc 0) (2 * δ + 2 * δ * Suc δ ^ ν + 4 * δ⇧2 * Suc δ ^ ν + (δ + δ + Suc δ ^ ν * (δ + δ)))
        = (2 * δ + 2 * δ * Suc δ ^ ν + 4 * δ⇧2 * Suc δ ^ ν + (δ + δ + Suc δ ^ ν * (δ + δ)))"
    apply (rule linorder_class.max.absorb2)
    using Suc_leI add_gr_0 that by presburger
    thus ?thesis 
      by (simp add: algebra_simps)
  qed

  show ?thesis
    unfolding step0
    unfolding step1
    unfolding step2
    unfolding step3
    apply (simp add: algebra_simps)
    by algebra
qed

poly_degree A⇩1_poly
poly_degree A⇩2_poly
poly_degree A⇩3_poly
poly_degree S_poly
poly_degree T_poly
poly_degree R_poly

lemma A⇩1_vars: "max_vars A⇩1_poly ≤ 8"
  unfolding A⇩1_poly_def b_poly_def coding_variables.b_poly_def
  apply (rule le_trans[OF max_vars_poly_subst_list_bounded])
  by (rule le_trans[OF max_vars_poly_subst_list_general], auto)

lemma h0: "max_vars (4::int mpoly) ≤ 8"
  by (metis Const_numeral max_vars_Const zero_le)

lemma h1: "max_vars (8::int mpoly) ≤ 8"
  by (metis Const_numeral max_vars_Const zero_le)

lemma h2: "max_vars (32::int mpoly) ≤ 8"
  by (metis Const_numeral max_vars_Const zero_le)

lemma A⇩2_vars: "max_vars A⇩2_poly ≤ 8"
  unfolding A⇩2_poly_def apply (rule le_trans[OF max_vars_mult], auto)+
  unfolding D_poly_def F_poly_def I_poly_def
  unfolding X_poly_def coding_variables.X_poly_def Y_poly_def coding_variables.Y_poly_def
  unfolding power2_eq_square
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_general]›, simp_all, all ‹intro conjI›)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  by (rule le_trans[OF max_vars_poly_subst_list_general]
              le_trans[OF max_vars_pow]
              le_trans[OF max_vars_mult]
              le_trans[OF max_vars_add]
              le_trans[OF max_vars_diff], auto)+

lemma A⇩3_vars: "max_vars A⇩3_poly ≤ 8"
  unfolding A⇩3_poly_def power2_eq_square
  apply (rule le_trans[OF max_vars_pow]
              le_trans[OF max_vars_mult]
              le_trans[OF max_vars_add]
              le_trans[OF max_vars_diff]; auto simp: h0)+
  apply (all ‹rule le_trans[OF max_vars_pow] le_trans[OF max_vars_mult]›, auto)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  unfolding U_poly_def V_poly_def K_poly_def
  unfolding X_poly_def coding_variables.X_poly_def Y_poly_def coding_variables.Y_poly_def
  unfolding power2_eq_square
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_general]›, auto)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  by (rule le_trans[OF max_vars_poly_subst_list_general]
              le_trans[OF max_vars_pow]
              le_trans[OF max_vars_mult]
              le_trans[OF max_vars_add]
              le_trans[OF max_vars_diff], auto)+

lemma S_vars: "max_vars S_poly ≤ 8"
  unfolding S_poly_def
  unfolding X_poly_def coding_variables.X_poly_def Y_poly_def coding_variables.Y_poly_def
  unfolding power2_eq_square
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_general]›, auto)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  by (rule le_trans[OF max_vars_poly_subst_list_general]
              le_trans[OF max_vars_pow]
              le_trans[OF max_vars_mult]
              le_trans[OF max_vars_add]
              le_trans[OF max_vars_diff], auto)+

lemma T_vars: "max_vars T_poly ≤ 8"
  unfolding T_poly_def b_poly_def coding_variables.b_poly_def
  unfolding X_poly_def coding_variables.X_poly_def Y_poly_def coding_variables.Y_poly_def
  unfolding power2_eq_square
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_general]›, auto)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  by (rule le_trans[OF max_vars_poly_subst_list_general]
              le_trans[OF max_vars_pow]
              le_trans[OF max_vars_mult]
              le_trans[OF max_vars_add]
              le_trans[OF max_vars_diff], auto)+

lemma K_vars: "max_vars K_poly ≤ 8"
  unfolding K_poly_def
  unfolding X_poly_def coding_variables.X_poly_def Y_poly_def coding_variables.Y_poly_def power2_eq_square
  apply ((rule le_trans[OF max_vars_pow]
               le_trans[OF max_vars_mult max.boundedI] 
               le_trans[OF max_vars_add max.boundedI]
               le_trans[OF max_vars_diff' max.boundedI])
             | simp_all add: h1)+
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_general]›, auto)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  by (rule le_trans[OF max_vars_poly_subst_list_general]
              le_trans[OF max_vars_pow]
              le_trans[OF max_vars_mult]
              le_trans[OF max_vars_add]
              le_trans[OF max_vars_diff], auto)+

lemma L_vars: "max_vars L_poly ≤ 8"
  unfolding L_poly_def
  unfolding X_poly_def coding_variables.X_poly_def Y_poly_def coding_variables.Y_poly_def power2_eq_square
  apply ((rule le_trans[OF max_vars_pow]
               le_trans[OF max_vars_mult max.boundedI] 
               le_trans[OF max_vars_add max.boundedI]
               le_trans[OF max_vars_diff' max.boundedI])
             | simp_all add: h1)+
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_general]›, auto)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  by (rule le_trans[OF max_vars_poly_subst_list_general]
              le_trans[OF max_vars_pow]
              le_trans[OF max_vars_mult]
              le_trans[OF max_vars_add]
              le_trans[OF max_vars_diff], auto)+

lemma C_vars: "max_vars C_poly ≤ 8"
  unfolding C_poly_def
  unfolding X_poly_def coding_variables.X_poly_def Y_poly_def coding_variables.Y_poly_def power2_eq_square
  apply ((rule le_trans[OF max_vars_pow]
               le_trans[OF max_vars_mult max.boundedI] 
               le_trans[OF max_vars_add max.boundedI]
               le_trans[OF max_vars_diff' max.boundedI])
             | simp_all add: h1)+
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_general]›, auto)
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  by (rule le_trans[OF max_vars_poly_subst_list_general]
              le_trans[OF max_vars_pow]
              le_trans[OF max_vars_mult]
              le_trans[OF max_vars_add]
              le_trans[OF max_vars_diff], auto)+

lemma μ_vars:
  "max_vars (poly_subst_list [Var 0, Var (Suc 0), Var 2, Var 3, Var 4, Var 5, Var 6, Var 7, Var 8, Var 9] μ_poly) ≤ 8"
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  unfolding μ_poly_def
  unfolding X_poly_def coding_variables.X_poly_def Y_poly_def coding_variables.Y_poly_def 
            b_poly_def power2_eq_square
  apply ((rule le_trans[OF max_vars_pow]
               le_trans[OF max_vars_mult max.boundedI] 
               le_trans[OF max_vars_add max.boundedI]
               le_trans[OF max_vars_diff' max.boundedI])
             | simp_all add: h1)+
  apply (all ‹rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]]›, auto)
  by (all ‹rule le_trans[OF max_vars_poly_subst_list_general]›, auto)

lemma R_vars: "max_vars R_poly ≤ 8"
  unfolding R_poly_def
  unfolding power2_eq_square
  by ((rule le_trans[OF max_vars_pow]
               le_trans[OF max_vars_mult max.boundedI] 
               le_trans[OF max_vars_add max.boundedI]
               le_trans[OF max_vars_diff' max.boundedI])
             | simp_all add: h1 h2 μ_vars
             | rule le_trans[OF max_vars_poly_subst_list_bounded[of _ 8]], simp add: K_vars C_vars L_vars)+


lemma list_vars: "i ≤ 8 ⟹ max_vars
          ([Var 0::int mpoly, Var (Suc 0), Var (Suc (Suc 0)), Var (Suc (Suc (Suc 0))),
            Var (Suc (Suc (Suc (Suc 0)))), Var (Suc (Suc (Suc (Suc (Suc 0))))),
            Var (Suc (Suc (Suc (Suc (Suc (Suc 0)))))),
            Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))),
            Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))),
            Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))] !⇩0
           i)
         ≤ 8"
  apply (simp add: nth0_def)
  by (smt (z3) add.right_neutral add_Suc_right le_Suc_eq less_eq_nat.simps(1) max_vars_Var nle_le
      nth_Cons_0 nth_Cons_Suc numeral_1_eq_Suc_0 numeral_Bit0)


lemmas aux_vars = A⇩1_vars A⇩2_vars A⇩3_vars S_vars T_vars R_vars


lemma total_degree_three_squares_rw:
  fixes Pextra :: "'a::comm_semiring_1 mpoly"
  shows "ia ≤ 8 ⟹
        total_degree_env env
         ([Var 0, Var (Suc 0), Var (Suc (Suc 0)),
           Var (Suc (Suc (Suc 0))), Var (Suc (Suc (Suc (Suc 0)))),
           Var (Suc (Suc (Suc (Suc (Suc 0))))),
           Var (Suc (Suc (Suc (Suc (Suc (Suc 0)))))),
           Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))),
           Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))),
           Pextra] !⇩0
          ia)
        = total_degree_env env
         ([Var 0 :: 'a mpoly , Var (Suc 0), Var (Suc (Suc 0)), Var (Suc (Suc (Suc 0))),
           Var (Suc (Suc (Suc (Suc 0)))), Var (Suc (Suc (Suc (Suc (Suc 0))))),
           Var (Suc (Suc (Suc (Suc (Suc (Suc 0)))))),
           Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))),
           Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))]  !⇩0
          ia)"
  unfolding total_degree_env_id[symmetric]
  apply (drule le_imp_less_Suc)
  using total_degree_env_reduce[of ia "map Var [0::nat, 1, 2, 3, 4, 5, 6, 7, 8]", simplified]
  by (metis One_nat_def Suc_1 Suc_numeral semiring_norm(2,5,8))

lemma final: "⋀ia. ia ≤ 8 ⟹
          total_degree_env (λ_. Suc 0)
           ([Var 0::int mpoly, Var (Suc 0), Var (Suc (Suc 0)), Var (Suc (Suc (Suc 0))),
             Var (Suc (Suc (Suc (Suc 0)))), Var (Suc (Suc (Suc (Suc (Suc 0))))),
             Var (Suc (Suc (Suc (Suc (Suc (Suc 0)))))),
             Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))),
             Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))),
             Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) +
             (Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) *
              Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) +
              (Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) *
               Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) +
               Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) *
               Var (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))] !⇩0
            ia)
          ≤ Suc 0"
  apply (simp add: total_degree_three_squares_rw)
  by (metis (no_types, lifting) Nil_is_map_conv One_nat_def le_add1 list.simps(9) plus_1_eq_Suc
      total_degree_env_mono3_map_Var)
(* End auxiliary lemmas *)

poly_extract Q


lemma Q_alt: "Q = σ M3"
  unfolding Q_def σ_def ..

lemma R_gt_0_consequences:
  fixes a :: nat and f g h k l w n :: int
  assumes "R τ > 0" and "b τ ≥ 0" and "f > 0"
  shows "g ≥ 1" and "g < 2 * μ τ" and "K τ ≠ 0" 
    and "bridge_variables.d2f k l w h g (Y τ) (X τ)"
proof -
  have helper: "0 < int α * β ^ γ" if "α > 0" and "β > 0" for α β γ 
    by (simp add: that(1-2))

  have "b τ > 0"
  proof - 
    have "b τ ≠ 0"
    unfolding b_def coding_variables.b_def
    using ‹f > 0› apply simp
    by (smt (verit, best) mult_pos_pos of_nat_less_0_iff)
    
    thus "b τ > 0" using ‹b τ ≥ 0› by auto
  qed

  have "μ τ > 0" 
    unfolding μ_def
    using helper[of "coding_variables.γ P⇩1" "b τ", 
                 OF coding_variables.γ_gt_0 ‹b τ > 0›]
    unfolding b_def by auto
  hence "real_of_int (8*(μ τ)^3) > 0"
    by auto

  let ?R' = "8 * (μ τ)^3 * g * (K τ)^2 - g^2 * (32 * ((C τ) - (K τ)*(L τ))^2 * (μ τ)^3 + g^2 * (K τ)^2)"
  have R_gt_0_condition: "real_of_int ?R' > 0"
  proof - 
    have rewrite: "f^2 * l^2 * x^2 = (f * l * x) ^2" 
      by (simp add: power_mult_distrib)

    have helper: "0 < α^2 * β ⟹ 0 < β" for α β :: int 
      by (smt (verit) mult_nonneg_nonpos power2_less_0)
      
    have "?R' > 0"
      using ‹R τ > 0›
      unfolding R_def μ_def K_def L_def C_def 
      unfolding rewrite using helper[of "f * l * x"]
      by metis

    thus ?thesis
      using of_int_pos by blast
  qed

  hence "g ≠ 0"
    by (auto)
  hence "real_of_int (g^2) > 0"
    by auto

  have inequality_divided: 
    "(K τ)^2 / g > 4 * ((C τ) - (K τ)*(L τ))^2 + (g^2 * (K τ)^2) / (8*(μ τ)^3)"
    (is "?A / g > ?B + ?C / (8*(μ τ)^3)")
  proof -
    have "0 < (8*(μ τ)^3) * g * (K τ)^2 / (8*(μ τ)^3) - g^2 * (32 * ((C τ) - (K τ)*(L τ))^2 * (μ τ)^3 + g^2 * (K τ)^2) / (8*(μ τ)^3)"
      using divide_strict_right_mono[of 0 "real_of_int ?R'" "8*(μ τ)^3", OF R_gt_0_condition ‹real_of_int (8*(μ τ)^3) > 0›]
        by (simp add: diff_divide_distrib)
    hence aux1: "g * (K τ)^2 > g^2 * (32 * ((C τ) - (K τ)*(L τ))^2 * (μ τ)^3 + g^2 * (K τ)^2) / (8*(μ τ)^3)"
      using ‹0 < μ τ› by auto
    
    have "(g * (K τ)^2) / g^2 > (32 * ((C τ) - (K τ)*(L τ))^2 * (μ τ)^3 + g^2 * (K τ)^2) / (8*(μ τ)^3)"
      using divide_strict_right_mono[OF aux1 ‹real_of_int (g^2) > 0›]
      by (auto simp: ‹g ≠ 0›)
    hence "(K τ)^2 / g > 4 * ((C τ) - (K τ)*(L τ))^2 + (g^2 * (K τ)^2) / (8*(μ τ)^3)"
      using ‹μ τ > 0›
      by (auto simp add: add_divide_distrib) (metis power2_eq_square real_divide_square_eq)
    then show ?thesis
      by auto
  qed

  have 1: "4 * ((C τ) - (K τ)*(L τ))^2 + (g^2 * (K τ)^2) / (8*(μ τ)^3)
            ≥ (g^2 * (K τ)^2) / (8*(μ τ)^3)"
      by simp

  have "(K τ)^2 / g > 0"
  proof - 
    have 2: "(g^2 * (K τ)^2) / (8*(μ τ)^3) ≥ 0"
      using ‹(μ τ) > 0› by (simp add: pos_imp_zdiv_nonneg_iff)

    show ?thesis using 1 2 inequality_divided
      by linarith
  qed

  show "(K τ) ≠ 0" 
    using ‹(K τ)^2 / g > 0› by fastforce


  have "g > 0"
    using ‹(K τ)^2 / g > 0› ‹(K τ) ≠ 0›
    by (simp add: zero_less_divide_iff)
  then show "g ≥ 1"
    using ‹g ≠ 0› by auto
  from ‹g > 0› have "real_of_int g > 0"
    by auto

  show "g < 2 * μ τ"
  proof -
    from inequality_divided have "(K τ)^2 / g > (g^2 * (K τ)^2) / (8*(μ τ)^3)"
      by auto (smt (verit) power2_less_0)
    hence "(8*(μ τ)^3) * (K τ)^2 > real_of_int g^3 * (K τ)^2"
      using ‹real_of_int (8*(μ τ)^3) > 0› using ‹real_of_int g > 0›
      by (auto simp: divide_simps algebra_simps power2_eq_square power3_eq_cube)
    hence "real_of_int g < 2 * μ τ"
      apply (simp add: ‹(K τ) ≠ 0›)
      apply (rule power_less_imp_less_base[of _ 3])
      using ‹μ τ > 0› by auto
    then show ?thesis
      by auto
  qed

  from inequality_divided have "4 * ((C τ) - (K τ)*(L τ))^2 < (K τ)^2 / g"
    using ‹g > 0› ‹μ τ > 0› ‹(K τ) ≠ 0› apply simp
    by (smt (verit, ccfv_SIG) diff_divide_distrib mult_sign_intros(1)
            of_int_1_le_iff power2_less_0 zero_le_power_eq_numeral zero_less_divide_iff)
  also have "... ≤ (K τ)^2"
    using ‹g ≥ 1›
    by (auto simp: algebra_simps divide_simps mult_le_cancel_right1)
  finally have "4 * ((C τ) - (K τ)*(L τ))^2 < (K τ)^2"
    by linarith
  then have "(2 * (C τ) - 2 * (K τ)*(L τ))^2 < (K τ)^2"
    by (auto simp: algebra_simps power2_eq_square)
  then show "bridge_variables.d2f k l w h g (Y τ) (X τ)" 
    unfolding bridge_variables.d2f_def C_def L_def K_def
    by (auto simp: algebra_simps)
qed

lemma R_gt_0_necessary_condition: 
  fixes a :: nat and f g h k l w x y :: int
  assumes "f > 0" and "x > 0" and "l > 0" and "g > 0" and "g < μ τ" and
          "bridge_variables.d2e k l w h g (Y τ) (X τ)"
  shows "R τ > 0"
proof - 
  from assms have "μ τ > 0"
    by auto

  have "(K τ)^2 ≥ 0"
    by auto

  have 0: "(4 * g * (C τ - K τ * L τ))^2 < (K τ)^2"
    using assms(6)
    unfolding bridge_variables.d2e_def C_def K_def L_def
    by (auto simp: algebra_simps)
  hence "(K τ)^2 > 0"
    by auto

  from 0 have "2 * 4^2 * g^2 * (C τ - K τ * L τ)^2 < 2 * (K τ)^2"
    by (auto simp: algebra_simps power2_eq_square)

  moreover have "8*g^4 / (8*(μ τ)^3) * (K τ)^2 ≤ g * (K τ)^2"
  proof -
    have "8*g^4 / (8*(μ τ)^3) < g"
      apply (simp add: power2_eq_square ‹g < μ τ›)
      using ‹g < μ τ› ‹g > 0› ‹μ τ > 0›
      apply (simp add: algebra_simps divide_simps power2_eq_square power4_eq_xxxx)
      using ‹g < μ τ› apply simp
      unfolding real_of_int_strict_inequality power3_eq_cube
      apply (simp add:  mult.commute mult.assoc mult_strict_right_mono)
      by (smt (verit, best) mult_le_less_imp_less mult_nonneg_nonneg of_int_le_0_iff real_of_int_inequality)
    thus ?thesis
      using ‹(K τ)^2 ≥ 0›
      apply simp
      by (metis less_eq_real_def mult_right_mono times_divide_eq_left zero_le_power2)
  qed

  ultimately have "2 * 4^2 * g^2 * (C τ - K τ * L τ)^2 + 8*g^4 / (8*(μ τ) ^ 3) * (K τ)^2 < 2 * (K τ)^2 + g * (K τ)^2"
    unfolding real_of_int_strict_inequality by auto

  also have "... < 8 * g * (K τ)^2"
    using ‹g > 0› ‹(K τ)^2 > 0› by (auto simp: algebra_simps)

  finally have "4 * g^2 * (C τ - K τ * L τ)^2 + g^4 / (8*(μ τ) ^ 3) * (K τ)^2 < g * (K τ)^2"
    by (auto simp: algebra_simps)

  hence "8 * (μ τ)^3 * 4 * g^2 * (C τ - K τ * L τ)^2 + g^4 * (K τ)^2 < 8 * (μ τ)^3 * g * (K τ)^2"
    using ‹μ τ > 0› unfolding real_of_int_strict_inequality 
    by (auto simp: divide_simps algebra_simps power2_eq_square)

  hence "8 * (μ τ)^3 * g * (K τ)⇧2 - g⇧2 * (32 * (C τ - K τ * L τ)^2 * (μ τ)^3 + g⇧2 * (K τ)⇧2) > 0"
    by (auto simp: divide_simps power2_eq_square power4_eq_xxxx algebra_simps)

  thus ?thesis unfolding R_def using assms by auto
qed

end

end