# Theory Renegar_Proofs

```theory Renegar_Proofs
imports Renegar_Algorithm
BKR_Proofs
begin

(* Note that there is significant overlap between Renegar and BKR in general, so there is some
similarity between this file and BKR_Proofs.thy
The main difference is that the RHS vector in Renegar is different from the RHS vector in BKR
In BKR, all of the qs are assumed to be relatively prime to p. Renegar removes this assumption.
In general, the _R's on definition and lemma names in this file are to emphasize that we are
working with Renegar style.
*)

section "Tarski Queries Changed"

lemma construct_NofI_R_relation:
fixes p:: "real poly"
fixes I1:: "real poly list"
fixes I2:: "real poly list"
shows "construct_NofI_R p I1 I2 =
construct_NofI (sum_list (map power2 (p # I1))) I2"
unfolding construct_NofI_R_def construct_NofI_def
by metis

lemma sum_list_map_power2:
shows "sum_list (map power2 ls) ≥ (0::real poly)"
apply (induct ls)
by auto

lemma sum_list_map_power2_poly:
shows "poly (sum_list (map power2 (ls::real poly list))) x ≥ (0::real)"
apply (induct ls)
by auto

lemma construct_NofI_R_prop_helper:
fixes p:: "real poly"
fixes I1:: "real poly list"
fixes I2:: "real poly list"
assumes nonzero: "p≠0"
shows "construct_NofI_R p I1 I2 =
rat_of_int (int (card {x. poly (sum_list (map (λx. x^2) (p # I1))) x = 0 ∧ poly (prod_list I2) x > 0}) -
int (card {x. poly (sum_list (map (λx. x^2) (p # I1))) x = 0  ∧ poly (prod_list I2) x < 0}))"
proof -
show ?thesis unfolding construct_NofI_R_relation[of p I1 I2]
apply (subst construct_NofI_prop[of _ I2])
apply auto
using assms sum_list_map_power2
by (metis le_add_same_cancel1 power2_less_eq_zero_iff)
qed

lemma zer_iff:
fixes p:: "real poly"
fixes ls:: "real poly list"
shows "poly (sum_list (map (λx. x^2) ls)) x = 0 ⟷ (∀i ∈ set ls. poly i x = 0)"
proof (induct ls)
case Nil
then show ?case by auto
next
case (Cons a I1)
then show ?case
apply simp
using zero_le_power2 apply blast
using sum_list_map_power2_poly apply presburger
by simp
qed

lemma construct_NofI_prop_R:
fixes p:: "real poly"
fixes I1:: "real poly list"
fixes I2:: "real poly list"
assumes nonzero: "p≠0"
shows "construct_NofI_R p I1 I2 =
rat_of_int (int (card {x. poly p x = 0 ∧ (∀q ∈ set I1. poly q x = 0) ∧ poly (prod_list I2) x > 0}) -
int (card {x. poly p x = 0  ∧ (∀q ∈ set I1. poly q x = 0) ∧ poly (prod_list I2) x < 0}))"
unfolding construct_NofI_R_prop_helper[OF nonzero]
using zer_iff
apply auto
by (smt (verit, del_insts) Collect_cong sum_list_map_power2_poly zero_le_power2 zero_less_power2)

section "Matrix Equation"

definition map_sgas:: "rat list ⇒ rat list"
where "map_sgas l = map (λr. (1 - r^2)) l"

definition z_R:: "(nat list*nat list) ⇒ rat list ⇒ rat"
where "z_R index_list sign_asg ≡ (prod_list (map (nth (map_sgas sign_asg)) (fst(index_list))))*(prod_list (map (nth sign_asg) (snd(index_list))))"

definition mtx_row_R:: "rat list list ⇒ (nat list * nat list) ⇒ rat list"
where "mtx_row_R sign_list index_list ≡ (map ((z_R index_list)) sign_list)"

definition matrix_A_R:: "rat list list ⇒  (nat list * nat list) list ⇒ rat mat"
where "matrix_A_R sign_list subset_list =
(mat_of_rows_list (length sign_list) (map (λi .(mtx_row_R sign_list i)) subset_list))"

definition all_list_constr_R:: "(nat list*nat list) list ⇒ nat ⇒ bool"
where "all_list_constr_R L n ≡ (∀x. List.member L x ⟶ (list_constr (fst x) n ∧ list_constr (snd x) n))"

definition alt_matrix_A_R:: "rat list list ⇒ (nat list*nat list) list ⇒ rat mat"
where "alt_matrix_A_R signs subsets = (mat (length subsets) (length signs)
(λ(i, j). z_R (subsets ! i) (signs ! j)))"

lemma alt_matrix_char_R: "alt_matrix_A_R signs subsets = matrix_A_R signs subsets"
proof -
have h0: "(⋀i j. i < length subsets ⟹
j < length signs ⟹
map (λindex_list. map (z_R index_list) signs) subsets ! i ! j = z_R (subsets ! i) (signs ! j))"
proof -
fix i
fix j
assume i_lt: "i < length subsets"
assume j_lt: "j < length signs"
show "((map (λindex_list. map (z_R index_list) signs) subsets) ! i) ! j = z_R (subsets ! i) (signs ! j)"
proof -
have h0: "(map (λindex_list. map (z_R index_list) signs) subsets) ! i =  map (z_R (subsets ! i)) signs"
using nth_map i_lt
by blast
then show ?thesis using nth_map j_lt
by simp
qed
qed
have h: " mat (length subsets) (length signs) (λ(i, j). z_R (subsets ! i) (signs ! j)) =
mat (length subsets) (length signs) (λ(i, y). map (λindex_list. map (z_R index_list) signs) subsets ! i ! y)"
using h0 eq_matI[where A = "mat (length subsets) (length signs) (λ(i, j). z_R (subsets ! i) (signs ! j))",
where B = "mat (length subsets) (length signs) (λ(i, y). map (λindex_list. map (z_R index_list) signs) subsets ! i ! y)"]
by auto
show ?thesis unfolding alt_matrix_A_R_def matrix_A_R_def mat_of_rows_list_def apply (auto) unfolding mtx_row_R_def
using h  by blast
qed

lemma subsets_are_rows_R: "∀i < (length subsets). row (alt_matrix_A_R signs subsets) i  = vec (length signs) (λj. z_R (subsets ! i) (signs ! j))"
unfolding row_def unfolding alt_matrix_A_R_def by auto

lemma signs_are_cols_R: "∀i < (length signs). col (alt_matrix_A_R signs subsets) i  = vec (length subsets) (λj. z_R (subsets ! j) (signs ! i))"
unfolding col_def unfolding alt_matrix_A_R_def by auto

definition consistent_sign_vec::"real poly list ⇒ real ⇒ rat list"
where "consistent_sign_vec qs x ≡
map (λ q. if (poly q x > 0) then (1::rat) else (if (poly q x = 0) then (0::rat) else (-1::rat))) qs"

definition construct_lhs_vector_R:: "real poly ⇒ real poly list ⇒ rat list list  ⇒ rat vec"
where "construct_lhs_vector_R p qs signs ≡
vec_of_list (map (λw.  rat_of_int (int (length (filter (λv. v = w) (map (consistent_sign_vec qs) (characterize_root_list_p p)))))) signs)"

(* The ith entry of LHS vector is the number of (distinct) real zeros of p where the sign vector of
the qs is the ith entry of signs.*)

(* Putting all of the pieces of the construction together *)
definition satisfy_equation_R:: "real poly ⇒ real poly list ⇒ (nat list*nat list) list ⇒ rat list list ⇒ bool"
where "satisfy_equation_R p qs subset_list sign_list =
(mult_mat_vec (matrix_A_R sign_list subset_list) (construct_lhs_vector_R p qs sign_list) = (construct_rhs_vector_R p qs subset_list))"

(* Recharacterize the LHS vector *)
lemma construct_lhs_vector_clean_R:
assumes "p ≠ 0"
assumes "i < length signs"
shows "(construct_lhs_vector_R p qs signs) \$ i =
card {x. poly p x = 0 ∧ ((consistent_sign_vec qs x) = (nth signs i))}"
proof -
from poly_roots_finite[OF assms(1)] have "finite {x. poly p x = 0}" .
then have eq: "(Collect
((λv. v = signs ! i) ∘
consistent_sign_vec qs) ∩
set (sorted_list_of_set
{x. poly p x = 0})) =
{x. poly p x = 0 ∧ consistent_sign_vec qs x = signs ! i}"
by auto
show ?thesis
unfolding construct_lhs_vector_R_def vec_of_list_index characterize_root_list_p_def
apply auto
apply (subst nth_map[OF assms(2)])
apply auto
apply (subst distinct_length_filter)
apply (auto)
using eq
by auto
qed

lemma construct_lhs_vector_cleaner_R:
assumes "p ≠ 0"
shows "(construct_lhs_vector_R p qs signs) =
vec_of_list (map (λs. rat_of_int (card {x. poly p x = 0 ∧ ((consistent_sign_vec qs x) = s)})) signs)"
apply (rule eq_vecI)
apply (auto simp add:  construct_lhs_vector_clean_R[OF assms] )
apply (simp add: vec_of_list_index)
unfolding construct_lhs_vector_R_def
using assms construct_lhs_vector_clean_R construct_lhs_vector_def apply auto[1]
apply (simp add: construct_lhs_vector_R_def)
by auto

(* Show that because our consistent sign vectors consist of 1, 0's, and -1's, z returns 1, 0, or -1
when applied to a consistent sign vector *)
lemma z_signs_R2:
fixes I:: "nat list"
fixes signs:: "rat list"
assumes lf: "list_all (λi. i < length signs) I"
assumes la:  "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) signs"
shows "(prod_list (map (nth signs) I)) = 1 ∨
(prod_list (map (nth signs) I)) = 0 ∨
(prod_list (map (nth signs) I)) = -1" using assms
proof (induct I)
case Nil
then show ?case by auto
next
case (Cons a I)
moreover have eo: "signs ! a = 1 ∨ signs ! a = 0 ∨ signs ! a = -1"
using assms
by (smt (verit, del_insts) calculation(2) list_all_length list_all_simps(1))
have "prod_list (map ((!) (map_sgas signs)) (a # I)) = (1 - (signs ! a)^2)*prod_list (map ((!) (map_sgas signs)) (I))"
unfolding map_sgas_def apply (auto)
using calculation(2) by auto
then show ?case using eo
using Cons.hyps calculation(2) la by auto
qed

lemma z_signs_R1:
fixes I:: "nat list"
fixes signs:: "rat list"
assumes lf: "list_all (λi. i < length signs) I"
assumes la:  "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) signs"
shows "(prod_list (map (nth (map_sgas signs)) I)) = 1 ∨
(prod_list (map (nth (map_sgas signs)) I)) = 0" using assms
proof (induct I)
case Nil
then show ?case by auto
next
case (Cons a I)
moreover have "signs ! a = 1 ∨ signs ! a = 0 ∨ signs ! a = -1"
using assms
by (smt (verit, best) calculation(2) list_all_length list_all_simps(1))
then have eo: "1 - (signs ! a)^2 = 1 ∨ 1 - (signs !a)^2 = 0"
using cancel_comm_monoid_add_class.diff_cancel diff_zero by fastforce
have "prod_list (map ((!) (map_sgas signs)) (a # I)) = (1 - (signs ! a)^2)*prod_list (map ((!) (map_sgas signs)) (I))"
unfolding map_sgas_def apply (auto)
using calculation(2) by auto
then show ?case using eo
using Cons.hyps calculation(2) la by auto
qed

lemma z_signs_R:
fixes I:: "(nat list * nat list)"
fixes signs:: "rat list"
assumes lf: "list_all (λi. i < length signs) (fst(I))"
assumes ls: "list_all (λi. i < length signs) (snd(I))"
assumes la:  "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) signs"
shows "(z_R I signs = 1) ∨ (z_R I signs = 0) ∨ (z_R I signs = -1)"
using assms z_signs_R2 z_signs_R1 unfolding z_R_def apply (auto)
by (metis (no_types, lifting) mult_cancel_left1 mult_minus1_right)

lemma z_lemma_R:
fixes I:: "nat list * nat list"
fixes sign:: "rat list"
assumes consistent: "sign ∈ set (characterize_consistent_signs_at_roots p qs)"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "(z_R I sign = 1) ∨ (z_R I sign = 0) ∨ (z_R I sign = -1)"
proof (rule z_signs_R)
have same: "length sign = length qs" using consistent
using characterize_consistent_signs_at_roots_def signs_at_def by fastforce
thus "(list_all (λi. i < length sign) (fst I))"
using welldefined1
by (auto simp add: list_constr_def characterize_consistent_signs_at_roots_def consistent_sign_vec_copr_def)
thus "(list_all (λi. i < length sign) (snd I))"
using same welldefined2
by (auto simp add: list_constr_def characterize_consistent_signs_at_roots_def consistent_sign_vec_copr_def)
show "list_all (λs. s = 1 ∨ s = 0 ∨ s = - 1) sign" using consistent
apply (auto simp add: list.pred_map  characterize_consistent_signs_at_roots_def  consistent_sign_vec_def)
using Ball_set
by (simp add: list_all_length signs_at_def squash_def)
qed

(* Show that all consistent sign vectors on roots of polynomials are in characterize_consistent_signs_at_roots  *)
lemma in_set_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
shows "sign ∈ set (characterize_consistent_signs_at_roots p qs)"
proof -
have h1: "consistent_sign_vec qs x ∈
set (remdups (map (signs_at qs) (sorted_list_of_set {x. poly p x = 0})))"
unfolding consistent_sign_vec_def signs_at_def squash_def
using root_p nonzero poly_roots_finite set_sorted_list_of_set apply (auto)
by (smt (verit, ccfv_SIG) Collect_cong comp_def image_eqI map_eq_conv mem_Collect_eq poly_roots_finite set_sorted_list_of_set)
thus ?thesis unfolding characterize_consistent_signs_at_roots_def characterize_root_list_p_def using sign_fix
by blast
qed

lemma consistent_signs_prop_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
shows  "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) sign"
using assms unfolding consistent_sign_vec_def squash_def apply (auto)
by (smt (z3) length_map list_all_length nth_map)

(* The next few lemmas relate z_R to the signs of the product of subsets of polynomials of qs *)
lemma horiz_vector_helper_pos_ind_R1:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
assumes asm: "list_constr I (length qs)"
shows "(prod_list (map (nth (map_sgas sign)) I)) = 1 ⟷
(∀p ∈ set (retrieve_polys qs I). poly p x = 0)"
using asm
proof (induction "I")
case Nil
then show ?case unfolding map_sgas_def apply (auto)
by (simp add: retrieve_polys_def)
next
case (Cons a xa)
then have same0: "(prod_list (map (nth (map_sgas sign)) xa)) = 1 ⟷
(∀p ∈ set (retrieve_polys qs xa). poly p x = 0)" unfolding list_constr_def by auto
have welldef: "a < length qs" using Cons.prems assms unfolding list_constr_def by auto
then have h: "prod_list (map ((!) (map_sgas sign)) (a#xa)) = (1 - (sign ! a)^2)*(prod_list (map ((!) (map_sgas sign)) (xa)))"
unfolding map_sgas_def using assms apply (auto)
by (metis (no_types, lifting) consistent_sign_vec_def length_map nth_map)
have "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) sign" using sign_fix unfolding consistent_sign_vec_def squash_def
apply (auto)
by (smt (z3) length_map list_all_length nth_map)
then have eo: "(prod_list (map ((!) (map_sgas sign)) (xa))) = 0 ∨ (prod_list (map ((!) (map_sgas sign)) (xa))) = 1"
using z_signs_R1 assms Cons.prems consistent_sign_vec_def length_map list_all_simps(1) length_map list_all_length list_constr_def
by (smt (verit, best))
have "(sign ! a)^2 = 1 ∨ (sign ! a)^2 = 0" using sign_fix welldef  unfolding consistent_sign_vec_def
by auto
then have s1: "(prod_list (map (nth (map_sgas sign)) (a#xa))) = 1 ⟷
((sign ! a)^2 = 0 ∧ (prod_list (map ((!) (map_sgas sign)) (xa))) = 1)"
using eo h
by (metis (mono_tags, opaque_lifting) cancel_comm_monoid_add_class.diff_cancel diff_zero mult.left_neutral mult_zero_left)
have "(sign ! a)^2 = 0 ⟷ (poly (qs ! a) x = 0)"
using sign_fix unfolding consistent_sign_vec_def welldef apply (auto)
apply (smt (z3) class_field.neg_1_not_0 class_field.zero_not_one nth_map welldef)
by (smt (z3) nth_map welldef)
then have same1:"(prod_list (map (nth (map_sgas sign)) (a#xa))) = 1 ⟷
((poly (qs ! a) x = 0) ∧ (prod_list (map ((!) (map_sgas sign)) (xa))) = 1)" using s1 by auto
have "set (retrieve_polys qs (a#xa)) = {(qs ! a)} ∪ set (retrieve_polys qs xa)"
by (metis (no_types, lifting) insert_is_Un list.simps(15) list.simps(9) retrieve_polys_def)
then have same2:"(∀p ∈ set (retrieve_polys qs (a#xa)). poly p x = 0) = ((poly (qs ! a) x = 0)
∧ (∀p ∈ set (retrieve_polys qs (xa)). poly p x = 0))"
by auto
then show ?case using same0 same1 same2
assms by auto
qed

lemma csv_length_same_as_qlist:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
shows "length sign = length qs"
using assms unfolding consistent_sign_vec_def by auto

lemma horiz_vector_helper_zer_ind_R2:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
assumes asm: "list_constr I (length qs)"
shows "(prod_list (map (nth sign) I)) = 0 ⟷
(poly (prod_list (retrieve_polys qs I)) x = 0)"
using asm
proof (induction "I")
case Nil
then show ?case unfolding map_sgas_def apply (auto) unfolding retrieve_polys_def
by auto next
case (Cons a xa)
have "poly (prod_list (retrieve_polys qs (a # xa))) x = (poly (qs ! a) x)*poly (prod_list (retrieve_polys qs (xa))) x"
by (simp add: retrieve_polys_def)
then show ?case using Cons.prems
by (smt (z3) Cons.IH class_field.neg_1_not_0 class_field.zero_not_one consistent_sign_vec_def list.simps(9) list_all_simps(1) list_constr_def mult_eq_0_iff nth_map prod_list.Cons sign_fix)
qed

lemma horiz_vector_helper_pos_ind_R2:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
assumes asm: "list_constr I (length qs)"
shows "(prod_list (map (nth sign) I)) = 1 ⟷
(poly (prod_list (retrieve_polys qs I)) x > 0)"
using asm
proof (induction "I")
case Nil
then show ?case unfolding map_sgas_def apply (auto) unfolding retrieve_polys_def
by auto next
case (Cons a xa)
then have ih: "(prod_list (map ((!) sign) xa) = 1) = (0 < poly (prod_list (retrieve_polys qs xa)) x)"
unfolding list_constr_def by auto
have lensame: "length sign = length qs" using sign_fix csv_length_same_as_qlist[of p x sign qs]
nonzero root_p by auto
have "poly (prod_list (retrieve_polys qs (a # xa))) x = (poly (qs ! a) x)*poly (prod_list (retrieve_polys qs (xa))) x"
by (simp add: retrieve_polys_def)
then have iff1: "(poly (prod_list (retrieve_polys qs (a#xa))) x > 0) ⟷
(((poly (qs ! a) x) > 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x > 0) ∨
((poly (qs ! a) x) < 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x < 0))"
by (metis zero_less_mult_iff)
have prodsame: "(prod_list (map (nth sign) (a#xa))) = (sign ! a)* (prod_list (map (nth sign) (xa)))"
using lensame Cons.prems unfolding list_constr_def by auto
have sagt: "sign ! a = 1 ⟷ (poly (qs ! a) x) > 0" using assms unfolding consistent_sign_vec_def
apply (auto)
apply (smt (verit, best) Cons.prems list_all_simps(1) list_constr_def neg_equal_zero nth_map zero_neq_one)
by (smt (verit, ccfv_threshold) Cons.prems list_all_simps(1) list_constr_def nth_map)
have salt: "sign ! a = -1 ⟷ (poly (qs ! a) x) < 0" using assms unfolding consistent_sign_vec_def
apply (auto)
apply (smt (verit, ccfv_SIG) Cons.prems less_minus_one_simps(1) less_minus_one_simps(3) list_all_simps(1) list_constr_def neg_0_less_iff_less nth_map)
by (smt (verit, best) Cons.prems list_all_simps(1) list_constr_def nth_map)
have h1: "((poly (qs ! a) x) > 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x > 0) ⟶
(prod_list (map (nth sign) (a#xa))) = 1"
using prodsame sagt ih by auto
have eo: "(prod_list (map ((!) sign) xa) = 1)  ∨ (prod_list (map ((!) sign) xa) = 0) ∨
(prod_list (map ((!) sign) xa) = -1)"
using Cons.prems consistent_signs_prop_R lensame list_constr_def nonzero root_p sign_fix z_signs_R2 by auto
have d1:"(prod_list (map ((!) sign) xa) = -1) ⟹ (0 > poly (prod_list (retrieve_polys qs xa)) x)"
proof -
assume "(prod_list (map ((!) sign) xa) = -1) "
then show "(0 > poly (prod_list (retrieve_polys qs xa)) x)"
using prodsame salt ih assms Cons.prems class_field.neg_1_not_0 equal_neg_zero horiz_vector_helper_zer_ind_R2 linorder_neqE_linordered_idom list_all_simps(1) list_constr_def
apply (auto)
apply (smt (verit, ccfv_threshold) class_field.neg_1_not_0 list.set_map list_all_length semidom_class.prod_list_zero_iff)
by (smt (verit, ccfv_threshold) class_field.neg_1_not_0 list.set_map list_all_length semidom_class.prod_list_zero_iff)
qed
have d2: "(0 > poly (prod_list (retrieve_polys qs xa)) x) ⟶ (prod_list (map ((!) sign) xa) = -1)"
using eo assms horiz_vector_helper_zer_ind_R2[where p = "p", where x = "x", where sign = "sign", where I ="I"]
apply (auto)
using ih apply force
by (metis (full_types, lifting) Cons.prems class_field.neg_1_not_0 horiz_vector_helper_zer_ind_R2 ih imageI list.set_map list_all_simps(1) list_constr_def mem_Collect_eq neg_equal_0_iff_equal semidom_class.prod_list_zero_iff)
have "(prod_list (map ((!) sign) xa) = -1) = (0 > poly (prod_list (retrieve_polys qs xa)) x)"
using d1 d2
by blast
then have h2: "((poly (qs ! a) x) < 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x < 0) ⟶
(prod_list (map (nth sign) (a#xa))) = 1"
using prodsame salt ih by auto
have h3: "(prod_list (map (nth sign) (a#xa))) = 1 ⟶ (((poly (qs ! a) x) > 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x > 0) ∨
((poly (qs ! a) x) < 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x < 0))"
using prodsame salt ih assms horiz_vector_helper_zer_ind_R2[where p = "p", where x = "x", where sign = "sign", where I ="I"]
by (smt (verit, ccfv_threshold) Cons.prems ‹poly (prod_list (retrieve_polys qs (a # xa))) x = poly (qs ! a) x * poly (prod_list (retrieve_polys qs xa)) x› horiz_vector_helper_zer_ind_R2 mem_Collect_eq mult_cancel_left1 mult_not_zero sagt)
then show ?case using h1 h2 h3 iff1 Cons.prems by auto
qed

lemma horiz_vector_helper_pos_ind_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list * nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
assumes asm1: "list_constr (fst I) (length qs)"
assumes asm2: "list_constr (snd I) (length qs)"
shows "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x > 0)) ⟷ (z_R I sign = 1)"
proof -
have len: "length sign = length qs" using sign_fix csv_length_same_as_qlist[of p x sign qs]
nonzero root_p by auto
have d1: "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x > 0)) ⟶ (z_R I sign = 1)"
using assms horiz_vector_helper_pos_ind_R1[where p = "p", where qs = "qs", where sign = "sign", where x = "x", where I = "fst I"]
horiz_vector_helper_pos_ind_R2[where p = "p", where qs = "qs", where sign = "sign", where x = "x", where I = "snd I"] unfolding z_R_def
by auto
have d2: "(z_R I sign = 1) ⟶ ((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x > 0))"
proof -
have h1: "(z_R I sign = 1) ⟶ (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0)"
proof -
have "(prod_list (map (nth (map_sgas sign)) (fst I))) = 1 ∨ (prod_list (map (nth (map_sgas sign)) (fst I))) = 0"
using len consistent_signs_prop_R[where p = "p", where qs = "qs", where x = "x", where sign = "sign"] z_signs_R1[where signs = "sign", where I = "fst I"] assms
unfolding list_constr_def
by auto
then show ?thesis
using z_signs_R1[where signs = "sign", where I = "fst I"] horiz_vector_helper_pos_ind_R1[where sign = "sign", where I = "fst I", where p = "p", where x = "x"] assms
apply (auto)
by (metis (mono_tags, opaque_lifting) ‹prod_list (map ((!) (map_sgas sign)) (fst I)) = 1 ∨ prod_list (map ((!) (map_sgas sign)) (fst I)) = 0› mult_zero_left z_R_def)
qed
then have h2: "(z_R I sign = 1) ⟶ (poly (prod_list (retrieve_polys qs (snd I))) x > 0)"
unfolding z_R_def using assms horiz_vector_helper_pos_ind_R2[where p = "p", where x = "x", where sign = "sign", where qs = "qs", where I ="snd I"]
by (metis horiz_vector_helper_pos_ind_R1 mult.left_neutral)
show ?thesis using h1 h2 by auto
qed
show ?thesis using d1 d2 by blast
qed

lemma horiz_vector_helper_pos_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list*nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x > 0)) ⟷ (z_R I sign = 1)"
using horiz_vector_helper_pos_ind_R
using  nonzero  root_p sign_fix welldefined1 welldefined2 by blast

lemma horiz_vector_helper_neg_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list*nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x < 0)) ⟷ (z_R I sign = -1)"
proof -
have set_hyp: "sign ∈ set (characterize_consistent_signs_at_roots p qs)"
using in_set_R[of p x sign qs] nonzero root_p sign_fix  by blast
have z_hyp: "((z_R I sign = 1) ∨ (z_R I sign = 0) ∨ (z_R I sign = -1))"
using welldefined1 welldefined2 set_hyp  z_lemma_R[where sign="sign", where I = "I", where p="p", where qs="qs"] by blast
have d1: "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x < 0)) ⟹ (z_R I sign = -1)"
using horiz_vector_helper_pos_R
using nonzero root_p sign_fix welldefined1 welldefined2
by (smt (verit, ccfv_threshold) horiz_vector_helper_pos_ind_R1 horiz_vector_helper_zer_ind_R2 mem_Collect_eq mult_eq_0_iff z_R_def z_hyp)
have d2: "(z_R I sign = -1) ⟹ ((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x < 0))"
using horiz_vector_helper_pos_ind_R1 horiz_vector_helper_zer_ind_R2 nonzero root_p sign_fix welldefined1 welldefined2
by (smt (verit, ccfv_threshold) class_field.neg_1_not_0 consistent_sign_vec_def consistent_signs_prop_R equal_neg_zero horiz_vector_helper_pos_ind_R2 length_map list_all_length list_constr_def mem_Collect_eq mem_Collect_eq mult_cancel_left1 mult_not_zero retrieve_polys_def z_R_def z_signs_R1 zero_neq_one)
then show ?thesis using d1 d2
by linarith
qed

lemma lhs_dot_rewrite:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list*nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
shows
"(vec_of_list (mtx_row_R signs I) ∙ (construct_lhs_vector_R p qs signs)) =
sum_list (map (λs. (z_R I s)  *  rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) signs)"
proof -
have "p ≠ 0" using nonzero by auto
from construct_lhs_vector_cleaner[OF this]
have rhseq: "construct_lhs_vector_R p qs signs =
vec_of_list
(map (λs. rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) signs)"
using construct_lhs_vector_cleaner_R nonzero by presburger
have "(vec_of_list (mtx_row_R signs I) ∙ (construct_lhs_vector_R p qs signs)) =
sum_list (map2 (*) (mtx_row_R signs I) (map (λs. rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) signs))"
unfolding rhseq
apply (intro vec_of_list_dot_rewrite)
by (auto simp add: mtx_row_R_def)
thus ?thesis unfolding mtx_row_R_def
using map2_map_map
by (auto simp add: map2_map_map)
qed

(* If we have a superset of the signs, we can drop to just the consistent ones *)
lemma construct_lhs_vector_drop_consistent_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list*nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots p qs) ⊆ set(signs)"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows
"(vec_of_list (mtx_row_R signs I) ∙ (construct_lhs_vector_R p qs signs)) =
(vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) ∙
(construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs)))"
proof -
have h0: "∀ sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ∧
0 < rat_of_nat (card  {xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn}) ⟶ z_R I sgn = 0"
proof -
have "∀ sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ∧ 0 < rat_of_int (card
{xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn}) ⟶ {xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn} ≠ {}"
by fastforce
then show ?thesis
proof -
{ fix iis :: "rat list"
have ff1: "0 ≠ p"
using nonzero rsquarefree_def by blast
obtain rr :: "(real ⇒ bool) ⇒ real" where
ff2: "⋀p. p (rr p) ∨ Collect p = {}"
by moura
{ assume "∃is. is = iis ∧ {r. poly p r = 0 ∧ consistent_sign_vec qs r = is} ≠ {}"
then have "∃is. consistent_sign_vec qs (rr (λr. poly p r = 0 ∧ consistent_sign_vec qs r = is)) = iis ∧ {r. poly p r = 0 ∧ consistent_sign_vec qs r = is} ≠ {}"
using ff2
by (metis (mono_tags, lifting))
then have "∃r. poly p r = 0 ∧ consistent_sign_vec qs r = iis"
using ff2
by smt
then have "iis ∈ consistent_sign_vec qs ` set (sorted_list_of_set {r. poly p r = 0})"
using ff1 poly_roots_finite
by (metis (mono_tags) imageI mem_Collect_eq set_sorted_list_of_set) }
then have "iis ∉ set signs ∨ iis ∈ consistent_sign_vec qs ` set (characterize_root_list_p p) ∨ ¬ 0 < rat_of_int (int (card {r. poly p r = 0 ∧ consistent_sign_vec qs r = iis}))"
by (metis (no_types) ‹∀sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ∧ 0 < rat_of_int (int (card {xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn})) ⟶ {xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn} ≠ {}› characterize_root_list_p_def) }
then show ?thesis
by fastforce
qed
qed
then have "∀ sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ⟶ ((0 = rat_of_nat (card
{xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn}) ∨ z_R I sgn = 0))"
by auto
then have hyp: "∀ s. s ∈ set signs ∧ s ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ⟶ (z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}) = 0)"
by auto
then have "(∑s∈ set(signs). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s∈(set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
proof -
have "set(signs) =(set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p)))"
by blast
then have sum_rewrite: "(∑s∈ set(signs). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s∈ (set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
by auto
then have sum_split: "(∑s∈ (set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))
=
(∑s∈ (set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))
+ (∑s∈ (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
by (metis (no_types, lifting) List.finite_set sum.Int_Diff)
have sum_zero: "(∑s∈ (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) = 0"
using hyp
by (simp add: hyp)
show ?thesis using sum_rewrite sum_split sum_zero by linarith
qed
then have set_eq: "set (remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p))) = set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))"
using all_info apply (simp add: characterize_consistent_signs_at_roots_def subset_antisym)
by (smt (z3) Int_subset_iff consistent_sign_vec_def list.set_map map_eq_conv o_apply signs_at_def squash_def subsetI subset_antisym)
have hyp1: "(∑s←signs. z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s∈set (signs). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using distinct_signs sum_list_distinct_conv_sum_set by blast
have hyp2: "(∑s←remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))
= (∑s∈ set (remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using sum_list_distinct_conv_sum_set by blast
have set_sum_eq: "(∑s∈(set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s∈ set (remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using set_eq by auto
then have "(∑s←signs. z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s←remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using set_sum_eq hyp1 hyp2
using ‹(∑s∈set signs. z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) = (∑s∈set signs ∩ consistent_sign_vec qs ` set (characterize_root_list_p p). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))› by linarith
then have "consistent_sign_vec qs ` set (characterize_root_list_p p) ⊆ set signs ⟹
(⋀p qss.
characterize_consistent_signs_at_roots p qss =
remdups (map (consistent_sign_vec qss) (characterize_root_list_p p))) ⟹
(∑s←signs. z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s←remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
by linarith
then show ?thesis unfolding lhs_dot_rewrite[OF nonzero]
apply (auto intro!: sum_list_distinct_filter simp add: distinct_signs  consistent_sign_vec_def characterize_consistent_signs_at_roots_def)
using all_info consistent_sign_vec_def characterize_consistent_signs_at_roots_def
by (smt (z3) list.set_map map_eq_conv o_apply set_remdups signs_at_def squash_def)
qed

lemma matrix_equation_helper_step_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list*nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots p qs) ⊆ set(signs)"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "(vec_of_list (mtx_row_R signs I) ∙ (construct_lhs_vector_R p qs signs)) =
rat_of_int (card {x. poly p x = 0 ∧ (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ poly (prod_list (retrieve_polys qs (snd I))) x > 0}) -
rat_of_int (card {x. poly p x = 0 ∧ (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ poly (prod_list (retrieve_polys qs (snd I))) x < 0})"
proof -
have finset: "finite (set (map (consistent_sign_vec qs)  (characterize_root_list_p p)))" by auto
let ?gt = "(set (map (consistent_sign_vec qs)  (characterize_root_list_p p)) ∩ {s. z_R I s = 1})"
let ?lt = "  (set (map (consistent_sign_vec qs)  (characterize_root_list_p p)) ∩ {s. z_R I s = -1})"
let ?zer = "(set (map (consistent_sign_vec qs)  (characterize_root_list_p p)) ∩ {s. z_R I s = 0})"
have eq: "set (map (consistent_sign_vec qs)  (characterize_root_list_p p)) = (?gt ∪ ?lt) ∪ ?zer"
proof safe
fix x
assume h:"x ∈ set (map (consistent_sign_vec qs) (characterize_root_list_p p))"
"z_R I x ≠ 0" "z_R I x ≠ - 1"
then have "x ∈ set (characterize_consistent_signs_at_roots p qs)"
unfolding characterize_consistent_signs_at_roots_def
by (smt (verit, del_insts) characterize_consistent_signs_at_roots_def characterize_root_list_p_def imageE in_set_R nonzero poly_roots_finite set_map sorted_list_of_set(1))
thus "z_R I x = 1"
using h welldefined1 welldefined2 z_lemma_R by blast
qed
have sumeq: "(∑s∈(?gt∪?lt). z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))
= (∑s∈?gt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) +
(∑s∈?lt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
apply (rule sum.union_disjoint) by auto
(* First, drop the signs that are irrelevant *)
from construct_lhs_vector_drop_consistent_R[OF assms(1-5)] have
"vec_of_list (mtx_row_R signs I) ∙ construct_lhs_vector_R p qs signs =
vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) ∙
construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs)" .
(* Now we split the sum *)
from lhs_dot_rewrite[OF assms(1)]
moreover have "... =
(∑s←characterize_consistent_signs_at_roots p qs.
z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))" .
moreover have "... =
(∑s∈set (map (consistent_sign_vec qs)  (characterize_root_list_p p)).
z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))" unfolding characterize_consistent_signs_at_roots_def sum_code[symmetric]
apply (auto)
by (smt (verit, best) consistent_sign_vec_def list.set_map map_eq_conv o_apply signs_at_def squash_def sum.set_conv_list)
moreover have setc1:"... =
(∑s∈(?gt∪?lt). z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) +
(∑s∈?zer. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) "
apply (subst eq)
apply (rule  sum.union_disjoint) by auto
ultimately have setc: "... =
(∑s∈?gt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) +
(∑s∈?lt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) +
(∑s∈?zer. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using sumeq by auto
have "∀s ∈ ?zer. (z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) = 0"
by auto
then have obvzer: "(∑s∈?zer. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) = 0"
by auto
(* Now recharacterize lt, gt*)
have setroots: "set (characterize_root_list_p p) = {x. poly p x = 0}" unfolding characterize_root_list_p_def
using poly_roots_finite nonzero rsquarefree_def set_sorted_list_of_set by blast
have *: "⋀s. {x. poly p x = 0 ∧ consistent_sign_vec qs x = s} =
{x ∈{x. poly p x = 0}. consistent_sign_vec qs x = s}"
by auto
have e1: "(∑s∈consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = 1}.
card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}) =
(sum (λx. if (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x) > 0 then 1 else 0) {x. poly p x = 0})"
unfolding * apply (rule sum_multicount_gen)
using ‹finite (set (map (consistent_sign_vec qs) (characterize_root_list_p p)))› setroots apply auto[1]
apply (metis List.finite_set setroots)
proof safe
fix x
assume rt: "poly p x = 0"
then have 1: "{s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = 1}. consistent_sign_vec qs x = s} =
{s. z_R I s = 1 ∧ consistent_sign_vec qs x = s}"
by auto
have 2: "... = {s. (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (0 < poly (prod_list (retrieve_polys qs (snd I))) x)  ∧ consistent_sign_vec qs x = s}"
using horiz_vector_helper_pos_R assms welldefined1 welldefined2 rt by blast
have 3: "... = (if (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (0 < poly (prod_list (retrieve_polys qs (snd I))) x)  then {consistent_sign_vec qs x} else {})"
by auto
then have "card {s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = 1}. consistent_sign_vec qs x = s} =
(if ((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 < poly (prod_list  (retrieve_polys qs (snd I))) x)
then 1 else 0)" using 1 2 3 by auto
thus " card
{s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = 1}.
consistent_sign_vec qs x = s} =
(if (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧
0 < poly (prod_list (retrieve_polys qs (snd I))) x
then 1 else 0)"
by auto
qed

have gtchr: "(∑s∈?gt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
rat_of_int (card {x. poly p x = 0 ∧ (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 < poly (prod_list (retrieve_polys qs (snd I))) x})"
apply (auto simp add: setroots)
apply (subst of_nat_sum[symmetric])
apply (subst of_nat_eq_iff)
apply (subst e1)
apply (subst card_eq_sum)
apply (rule sum.mono_neutral_cong_right)
apply (metis List.finite_set setroots)
by auto
have e2: " (∑s∈consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = - 1}.
card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}) =
(sum (λx. if (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x) < 0 then 1 else 0) {x. poly p x = 0})"
unfolding * apply (rule sum_multicount_gen)
using ‹finite (set (map (consistent_sign_vec qs) (characterize_root_list_p p)))› setroots apply auto[1]
apply (metis List.finite_set setroots)
proof safe
fix x
assume rt: "poly p x = 0"
then have 1: "{s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = -1}. consistent_sign_vec qs x = s} =
{s. z_R I s = -1 ∧ consistent_sign_vec qs x = s}"
by auto
have 2: "... = {s. ((∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 > poly (prod_list (retrieve_polys qs (snd I))) x)  ∧ consistent_sign_vec qs x = s}"
using horiz_vector_helper_neg_R assms rt welldefined1 welldefined2 by blast
have 3: "... = (if (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (0 > poly (prod_list (retrieve_polys qs (snd I))) x)  then {consistent_sign_vec qs x} else {})"
by auto
thus "card {s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = -1}. consistent_sign_vec qs x = s} =
(if (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 > poly
(prod_list
(retrieve_polys qs (snd I)))
x
then 1 else 0)" using 1 2 3 by auto
qed
have ltchr: "(∑s∈?lt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
- rat_of_int (card {x. poly p x = 0 ∧ (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 > poly (prod_list (retrieve_polys qs (snd I))) x})"
apply (auto simp add: setroots sum_negf)
apply (subst of_nat_sum[symmetric])
apply (subst of_nat_eq_iff)
apply (subst e2)
apply (subst card_eq_sum)
apply (rule sum.mono_neutral_cong_right)
apply (metis List.finite_set setroots)
by auto
show ?thesis using gtchr ltchr obvzer setc
using ‹(∑s←characterize_consistent_signs_at_roots p qs. z_R I s * rat_of_int (int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))) = (∑s∈set (map (consistent_sign_vec qs) (characterize_root_list_p p)). z_R I s * rat_of_int (int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})))› ‹vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) ∙ construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs) = (∑s←characterize_consistent_signs_at_roots p qs. z_R I s * rat_of_int (int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})))› ‹vec_of_list (mtx_row_R signs I) ∙ construct_lhs_vector_R p qs signs = vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) ∙ construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs)› setc1 by linarith
qed

lemma matrix_equation_main_step_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list*nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots p qs) ⊆ set(signs)"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "(vec_of_list (mtx_row_R signs I) ∙
(construct_lhs_vector_R p qs signs)) =
construct_NofI_R p (retrieve_polys qs (fst I)) (retrieve_polys qs (snd I))"
proof -
show ?thesis
unfolding construct_NofI_prop_R[OF nonzero]
using matrix_equation_helper_step_R[OF assms]
by linarith
qed

lemma mtx_row_length_R:
"list_all (λr. length r = length signs) (map (mtx_row_R signs) ls)"
apply (induction ls)
by (auto simp add: mtx_row_R_def)

(* Shows that as long as we have a "basis" of sign assignments (see assumptions all_info, welldefined),
and some other mild assumptions on our inputs (given in nonzero, distinct_signs), the construction
will be satisfied *)
theorem matrix_equation_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes subsets:: "(nat list*nat list) list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots p qs) ⊆ set(signs)"
assumes welldefined: "all_list_constr_R (subsets) (length qs)"
shows "satisfy_equation_R p qs subsets signs"
unfolding satisfy_equation_R_def matrix_A_R_def
construct_lhs_vector_R_def construct_rhs_vector_R_def all_list_constr_R_def
apply (subst mult_mat_vec_of_list)
apply (auto simp add: mtx_row_length_R intro!: map_vec_vec_of_list_eq_intro)
using matrix_equation_main_step_R[OF assms(1-3), unfolded construct_lhs_vector_R_def]
using all_list_constr_R_def in_set_member welldefined by fastforce

(* Prettifying some theorems*)

lemma consistent_signs_at_roots_eq:
assumes "p ≠ 0"
shows "consistent_signs_at_roots p qs =
set (characterize_consistent_signs_at_roots p qs)"
unfolding consistent_signs_at_roots_def characterize_consistent_signs_at_roots_def
characterize_root_list_p_def
apply auto
apply (subst set_sorted_list_of_set)
using assms poly_roots_finite apply blast
unfolding sgn_vec_def sgn_def signs_at_def squash_def o_def
using roots_def apply auto[1]
by (smt Collect_cong assms image_iff poly_roots_finite roots_def sorted_list_of_set(1))

abbreviation w_vec_R:: "real poly ⇒ real poly list ⇒ rat list list  ⇒ rat vec"
where "w_vec_R ≡ construct_lhs_vector_R"

abbreviation v_vec_R:: "real poly ⇒ real poly list ⇒ (nat list*nat list) list ⇒ rat vec"
where "v_vec_R ≡ construct_rhs_vector_R"

abbreviation M_mat_R:: "rat list list ⇒ (nat list*nat list) list ⇒ rat mat"
where "M_mat_R ≡ matrix_A_R"

theorem matrix_equation_pretty:
fixes subsets:: "(nat list*nat list) list"
assumes "p≠0"
assumes "distinct signs"
assumes "consistent_signs_at_roots p qs ⊆ set signs"
assumes "⋀a b i. (a, b) ∈ set ( subsets) ⟹ (i ∈ set a ∨ i ∈ set b) ⟹ i < length qs"
shows "M_mat_R signs subsets *⇩v w_vec_R p qs signs = v_vec_R p qs subsets"
unfolding satisfy_equation_R_def[symmetric]
using matrix_equation_R[of p signs qs subsets] assms
using consistent_signs_at_roots_eq unfolding all_list_constr_R_def list_constr_def apply (auto)
by (metis (no_types, lifting) Ball_set in_set_member)

section "Base Case"
definition satisfies_properties_R:: "real poly ⇒ real poly list ⇒ (nat list*nat list) list ⇒ rat list list ⇒ rat mat ⇒ bool"
where "satisfies_properties_R p qs subsets signs matrix =
( all_list_constr_R subsets (length qs) ∧ well_def_signs (length qs) signs ∧ distinct signs
∧ satisfy_equation_R p qs subsets signs ∧  invertible_mat matrix  ∧ matrix = matrix_A_R signs subsets
∧ set (characterize_consistent_signs_at_roots p qs) ⊆ set(signs)
)"

lemma mat_base_case_R:
shows "matrix_A_R [[1],[0],[-1]] [([], []),([0], []),([], [0])] = (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]])"
unfolding matrix_A_R_def mtx_row_R_def z_R_def map_sgas_def apply (auto)
by (simp add: numeral_3_eq_3)

lemma base_case_sgas_R:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
shows "set (characterize_consistent_signs_at_roots p [q]) ⊆ {[1],[0], [- 1]}"
unfolding characterize_consistent_signs_at_roots_def signs_at_def  apply (auto)
by (meson squash_def)

lemma base_case_sgas_alt_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
assumes len1: "length qs = 1"
assumes nonzero: "p ≠ 0"
shows "set (characterize_consistent_signs_at_roots p qs) ⊆ {[1], [0], [- 1]}"
proof -
have ex_q: "∃(q::real poly). qs = [q]"
using len1
using length_Suc_conv[of qs 0] by auto
then show ?thesis using base_case_sgas_R nonzero
by auto
qed

lemma base_case_satisfy_equation_R:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
shows "satisfy_equation_R p [q] [([], []),([0], []),([], [0])] [[1],[0],[-1]] "
proof -
have h1: "set (characterize_consistent_signs_at_roots p [q]) ⊆ {[1], [0],[- 1]}"
using base_case_sgas_R assms by auto
have h2: "all_list_constr_R [([], []),([0], []),([], [0])] (Suc 0)" unfolding all_list_constr_R_def
by (simp add: list_constr_def member_def)
then show ?thesis using matrix_equation_R[where p = "p", where qs = "[q]", where signs = "[[1],[0],[-1]] ", where subsets = "[([], []),([0], []),([], [0])]"]
nonzero h1  h2 by auto
qed

lemma base_case_satisfy_equation_alt_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
assumes len1: "length qs = 1"
assumes nonzero: "p ≠ 0"
shows "satisfy_equation_R p qs [([], []),([0], []),([], [0])] [[1],[0],[-1]]"
proof -
have ex_q: "∃(q::real poly). qs = [q]"
using len1
using length_Suc_conv[of qs 0] by auto
then show ?thesis using base_case_satisfy_equation_R nonzero
by auto
qed

lemma base_case_matrix_eq:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
shows "(mult_mat_vec (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]) (construct_lhs_vector_R p [q] [[1],[0],[-1]]) =
(construct_rhs_vector_R p [q] [([], []),([0], []),([], [0])]))"
using mat_base_case_R base_case_satisfy_equation_R unfolding satisfy_equation_R_def
by (simp add: nonzero)

lemma less_three: "(n::nat) < Suc (Suc (Suc 0)) ⟷ n = 0 ∨ n = 1 ∨ n = 2"
by auto

lemma inverse_mat_base_case_R:
shows "inverts_mat (mat_of_rows_list 3  [[1/2, -1/2, 1/2], [0, 1, 0], [1/2, -1/2, -1/2]]::rat mat) (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat)"
unfolding inverts_mat_def mat_of_rows_list_def mat_eq_iff apply auto
unfolding less_three by (auto simp add: scalar_prod_def)

lemma inverse_mat_base_case_2_R:
shows "inverts_mat (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat) (mat_of_rows_list 3  [[1/2, -1/2, 1/2], [0, 1, 0], [1/2, -1/2, -1/2]]:: rat mat)"
unfolding inverts_mat_def mat_of_rows_list_def mat_eq_iff apply auto
unfolding less_three by (auto simp add: scalar_prod_def)

lemma base_case_invertible_mat_R:
shows "invertible_mat (matrix_A_R [[1],[0], [- 1]] [([], []),([0], []),([], [0])])"
unfolding invertible_mat_def using inverse_mat_base_case_R inverse_mat_base_case_2_R
apply (auto)
apply (simp add: mat_base_case mat_of_rows_list_def)
using mat_base_case_R by auto

section "Inductive Step"

(***** Need some properties of smashing; smashing signs is just as it was in BKR *****)
subsection "Lemmas on smashing subsets "

definition subsets_first_component_list::"(nat list*nat list) list ⇒ nat list list"
where "subsets_first_component_list I = map (λI. (fst I)) I"

definition subsets_second_component_list::"(nat list*nat list) list ⇒ nat list list"
where "subsets_second_component_list I = map (λI. (snd I)) I"

definition smash_list_list::"('a list*'a list) list ⇒  ('a list*'a list) list ⇒ ('a list*'a list) list"
where "smash_list_list s1 s2 = concat (map (λl1. map (λl2. (fst l1 @ fst l2, snd l1 @ snd l2)) s2) s1)"

lemma smash_list_list_property_set:
fixes l1 l2 :: "('a list*'a list) list"
fixes a b:: "nat"
shows "∀ (elem :: ('a list*'a list)). (elem ∈ (set (smash_list_list l1 l2)) ⟶
(∃ (elem1:: ('a list*'a list)). ∃ (elem2:: ('a list*'a list)).
(elem1 ∈ set(l1) ∧ elem2 ∈ set(l2) ∧ elem = (fst elem1@ fst elem2, snd elem1 @ snd elem2))))"
proof clarsimp
fix a b
assume assum: "(a, b) ∈ set (smash_list_list l1 l2)"
show "∃aa ba. (aa, ba) ∈ set l1 ∧ (∃ab bb. (ab, bb) ∈ set l2 ∧ a = aa @ ab ∧ b = ba @ bb)"
using assum unfolding smash_list_list_def
apply (auto) by blast
qed

lemma subsets_smash_property_R:
fixes subsets1 subsets2 :: "(nat list*nat list) list"
fixes n:: "nat"
shows "∀ (elem :: nat list*nat list). (List.member (subsets_smash_R n subsets1 subsets2) elem) ⟶
(∃ (elem1::nat list*nat list). ∃ (elem2::nat list*nat list).
(elem1 ∈ set(subsets1) ∧ elem2 ∈ set(subsets2) ∧ elem = ((fst elem1) @ (map ((+) n) (fst elem2)), (snd elem1) @ (map ((+) n) (snd elem2)))))"
proof -
let ?fst_component2 = "subsets_first_component_list subsets2"
let ?snd_component2 = "subsets_second_component_list subsets2"
let ?new_subsets = "map (λI. ((map ((+) n)) (fst I),  (map ((+) n)) (snd I))) subsets2"
(* a slightly unorthodox use of signs_smash, but it closes the proof *)
have "subsets_smash_R n subsets1 subsets2 = smash_list_list subsets1 ?new_subsets"
unfolding subsets_smash_R_def smash_list_list_def apply (auto)
by (simp add: comp_def)
then show ?thesis using smash_list_list_property_set[of subsets1 ?new_subsets] apply (auto)
using imageE in_set_member set_map smash_list_list_property_set
by (smt (z3) prod.exhaust_sel)
qed

(* If subsets for smaller systems are well-defined, then subsets for combined systems are, too *)
subsection "Well-defined subsets preserved when smashing"

lemma well_def_step_R:
fixes qs1 qs2 :: "real poly list"
fixes subsets1 subsets2 :: "(nat list*nat list) list"
assumes well_def_subsets1: "all_list_constr_R (subsets1) (length qs1)"
assumes well_def_subsets2: "all_list_constr_R (subsets2) (length qs2)"
shows "all_list_constr_R ((subsets_smash_R (length qs1) subsets1 subsets2))
(length (qs1 @ qs2))"
proof -
let ?n = "(length qs1)"
have h1: "∀elem.
List.member (subsets_smash_R ?n subsets1 subsets2) elem ⟶
(∃ (elem1::nat list*nat list). ∃ (elem2::nat list*nat list).
(elem1 ∈ set(subsets1) ∧ elem2 ∈ set(subsets2) ∧ elem = ((fst elem1) @ (map ((+) ?n) (fst elem2)), (snd elem1) @ (map ((+) ?n) (snd elem2)))))"
using subsets_smash_property_R by ```