Theory Eleven_Unknowns_Z

theory Eleven_Unknowns_Z
  imports "Nine_Unknowns_N_Z/Nine_Unknowns_N_Z" "Three_Squares.Three_Squares"
begin

section ‹Eleven Unknowns over $\mathbb{Z}$›

context
  fixes P :: "int mpoly"
begin

definition Q_tilde :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int"
  where "Q_tilde a z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 = 
  (combined_variables.Q P) a z1 z2 z3 z4 z5 z6 z7 z8 (z9^2 + z10^2 + z11^2 + z11)"


poly_extract Q_tilde
poly_degree Q_tilde_poly | combined_variables.aux_vars combined_variables.final combined_variables.list_vars
     
lemma Q_tilde_degree_in_X_Y: 
  "Q_tilde_poly_degree = 8352 * combined_variables.Y_poly_degree P 
  + (15568 + (4176 * combined_variables.X_poly_degree P 
              + 48 * coding_variables.α (combined_variables.P1 P)))"
proof -
  note Q_tilde_degree_presimplified = Q_tilde_poly_degree_def[simplified Nat.max_nat.right_neutral 
      Nat.max_nat.left_neutral Nat.plus_nat.add_0]
  note A2_poly_degree_alt = combined_variables.A2_poly_degree_def[simplified, simplified 
      Nat.Suc_eq_plus1, simplified Groups.ac_simps(1), unfolded one_add_one, 
      simplified one_plus_numeral, simplified]

  show ?thesis unfolding Q_tilde_degree_presimplified
    combined_variables.S_poly_degree_def[simplified] 
    combined_variables.T_poly_degree_def[simplified]
    combined_variables.R_poly_degree_def[simplified]
    combined_variables.A1_poly_degree_def[simplified]
    combined_variables.A3_poly_degree_def[simplified]
    A2_poly_degree_alt
    by simp
qed

definition delta_P_suitable ("δs") where 
  "delta_P_suitable ≡ total_degree (suitable_for_coding P)"

definition nu_P_suitable ("νs") where 
  "nu_P_suitable ≡ max_vars (suitable_for_coding P)"

definition etas where
  "etas ≡ 15616 + 116928 * δs + 116976 * δs * Suc δs ^ νs + 116928 * δs^2 * Suc δs ^ νs"

lemma Q_tilde_degree_etas: "Q_tilde_poly_degree = etas"
proof - 
  note X_degree = combined_variables.X_poly_degree_alt[unfolded combined_variables.P1_def 
      coding_variables.δ_def, OF suitable_for_coding_total_degree, 
      folded coding_variables.δ_def, folded combined_variables.P1_def]
  have degree_bound: "coding_variables.δ (combined_variables.P1 P) = delta_P_suitable" 
    unfolding coding_variables.δ_def combined_variables.P1_def delta_P_suitable_def by simp
  have vars: "coding_variables.ν (combined_variables.P1 P) = nu_P_suitable" 
    unfolding coding_variables.ν_def combined_variables.P1_def nu_P_suitable_def by simp
  show ?thesis
  unfolding Q_tilde_degree_in_X_Y combined_variables.Y_poly_degree_def[simplified] X_degree
  unfolding coding_variables.α_def coding_variables.n_def
  apply simp
  unfolding vars degree_bound etas_def
  apply (simp add: algebra_simps)
  using Semiring_Normalization.comm_semiring_1_class.semiring_normalization_rules(29) by metis
qed


definition η where
  "η ν δ ≡ 15616 + 233856 * δ + 233952 * δ * (2 * δ + 1) ^ (ν + 1)
            + 467712 * δ^2 * (2 * δ + 1) ^ (ν + 1)"

lemma Q_tilde_degree:
  assumes "0 < total_degree P"
  assumes "total_degree P ≤ δ"
  assumes "max_vars P ≤ ν"
  shows "Q_tilde_poly_degree ≤ η ν δ"
proof -
  have ν: "νs ≤ ν + 1"
    apply (cases "vars P = {}")
    subgoal 
      by (simp add: fresh_var_def max_vars_of_nonempty nu_P_suitable_def
          suitable_for_coding_degree_vars(2))
    subgoal
      unfolding nu_P_suitable_def
      using suitable_for_coding_max_vars
      by (simp add: assms(3))
    done
  have δ: "δs ≤ 2 * δ"
    unfolding delta_P_suitable_def
    using suitable_for_coding_total_degree_bound[OF assms(1)] assms(2) by auto
  have δ_power: "Suc δs ^ ν ≤ Suc (2 * δ) ^ ν"
    by (simp add: δ power_mono)
  hence δ_power2: "Suc δs ^ νs ≤ Suc (2 * δ) ^ (ν + 1)"
    using ν power_mono le_trans
    by (smt (verit) Suc_eq_plus1 δ le_SucE mult_Suc mult_le_mono not_less_eq_eq power_Suc
        power_increasing trans_le_add1 trans_le_add2)
  hence δ_power3: "Suc δs ^ νs ≤ Suc (2 * δ) ^ ν + 2 * δ * Suc (2 * δ) ^ ν"
    using δ_power2 by (algebra, simp)
  have aux: "δs * Suc δs ^ νs ≤ 2 * (δ * (Suc (2 * δ) ^ ν + 2 * δ * Suc (2 * δ) ^ ν))"
    using δ_power3 mult_le_mono by (metis δ more_arith_simps(11))
  have bound: "Q_tilde_poly_degree ≤ 15616 + 116928 * 2 * δ + 116976 * 2 * δ * Suc (2 * δ) ^ (ν + 1) 
                                    + 116928 * 4 * δ^2 * Suc (2 * δ) ^ (ν + 1)"
    unfolding Q_tilde_degree_etas etas_def 
    apply simp
    apply (rule add_mono mult_le_mono, simp add: δ ν)+
    subgoal by (simp add: aux)
    subgoal 
      apply (rule add_mono mult_le_mono power_mono, simp_all add: δ ν δ_power3)
      by (metis δ numeral_Bit0_eq_double power2_eq_square power2_nat_le_eq_le power_mult_distrib)
    done
  thus ?thesis unfolding η_def by auto
qed

lemma max_vars_Q_tilde: "max_vars Q_tilde_poly ≤ 11"
proof -
  have aux_three_squares: "vars ((Var 9)2 + (Var 10)2 + (Var 11)2 + Var 11) ⊆ {9, 10, 11}"
  unfolding power2_eq_square
  by (rule subset_trans[OF vars_add Un_least]
        | rule subset_trans[OF vars_mult Un_least]
        | subst vars_Var; simp)+
  
  show ?thesis
    unfolding Q_tilde_poly_def
    apply (rule le_trans[OF max_vars_poly_subst_list_general])
    apply (simp add: max_vars_def aux_three_squares)
    apply (rule Max.boundedI, auto simp: vars_finite)
    using in_mono[OF aux_three_squares] by fastforce
qed

lemma eleven_unknowns_over_Z:
  fixes A :: "nat set"
  assumes "is_diophantine_over_N_with A P"
  shows "a ∈ A = (∃z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11. 
    Q_tilde (int a) z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 = 0)"
proof -

  have "(∃w1 w2 w3 w4 w5 w6 w7 w8 w9. 
            w9 ≥ 0 ∧ (combined_variables.Q P) (int a) w1 w2 w3 w4 w5 w6 w7 w8 w9 = 0) 
      = (∃z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11. 
            Q_tilde (int a) z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 = 0)"
  proof (intro iffI)
    assume asm1:"(∃w1 w2 w3 w4 w5 w6 w7 w8 w9. w9 ≥ 0 ∧
               (combined_variables.Q P) (int a) w1 w2 w3 w4 w5 w6 w7 w8 w9 = 0)"
    obtain w1 w2 w3 w4 w5 w6 w7 w8 w9 where w_prop:"w9 ≥ 0 ∧
               (combined_variables.Q P) (int a) w1 w2 w3 w4 w5 w6 w7 w8 w9 = 0"
      using asm1 by auto
    have w9decomp:"∃u9 u10 u11. w9 = u9^2+u10^2+u11^2+u11" 
      using four_decomposition_int w_prop by presburger
    obtain u9 u10 u11 where u_prop:"w9 = u9^2+u10^2+u11^2+u11" 
      using w9decomp by auto
    have cs1:"Q_tilde (int a) w1 w2 w3 w4 w5 w6 w7 w8 u9 u10 u11 = 0"
      using u_prop Q_tilde_def asm1 w_prop by presburger
    thus "∃z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11. Q_tilde (int a) z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 = 0" by blast
  next
    assume asm2: "∃z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11. Q_tilde (int a) z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 = 0"
    obtain z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 where z_prop:
      "Q_tilde (int a) z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 = 0" using asm2 by auto

    have cs2_0:
      "(combined_variables.Q P) (int a) z1 z2 z3 z4 z5 z6 z7 z8 (z9^2 + z10^2 + z11^2 + z11) = 0"
      using z_prop Q_tilde_def by simp
    have "z9^2 + z10^2 + z11^2 + z11 ≥0" by (meson four_decomposition_int)
    thus cs2:"∃w1 w2 w3 w4 w5 w6 w7 w8 w9. w9 ≥ 0 ∧
          (combined_variables.Q P) (int a) w1 w2 w3 w4 w5 w6 w7 w8 w9 = 0" using cs2_0 by blast
  qed

  thus ?thesis
    using theorem_III_new_statement assms by presburger
qed

end 

lemma eleven_unknowns_over_Z_polynomial: 
  fixes A :: "nat set" and P :: "int mpoly"
  assumes "is_diophantine_over_N_with A P"
  shows "a ∈ A = (∃z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11.
                  insertion ((!) [int a, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11]) (Q_tilde_poly P) = 0)"
  unfolding Q_tilde_correct eleven_unknowns_over_Z[of A P a, OF assms(1)] by simp

end