Common Guruswami-Sudan Root Helper Lemmas

Reusable proof facts for bounded bivariate root backends.

theorem CompPoly.array_mem_eraseDups_fold {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (xs : List α) (out : Array α) : a ∈ List.foldl (fun (out : Array α) (x : α) => if x ∈ out then out else out.push x) out xs → a ∈ out ∨ a ∈ xs

theorem CompPoly.array_mem_of_mem_eraseDups {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} (h : a ∈ xs.eraseDups) : a ∈ xs

theorem CompPoly.array_mem_eraseDups_fold_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (xs : List α) (out : Array α) : a ∈ out ∨ a ∈ xs → a ∈ List.foldl (fun (out : Array α) (x : α) => if x ∈ out then out else out.push x) out xs

theorem CompPoly.array_mem_eraseDups_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} (h : a ∈ xs) : a ∈ xs.eraseDups

theorem CompPoly.GuruswamiSudan.degreeLt_of_degreeLtBool {F : Type u_1} [Zero F] {p : CPolynomial F} {k : ℕ} (h : degreeLtBool p k = true) : degreeLt p k

theorem CompPoly.GuruswamiSudan.degreeLtBool_of_degreeLt {F : Type u_1} [Zero F] {p : CPolynomial F} {k : ℕ} (h : degreeLt p k) : degreeLtBool p k = true

theorem CompPoly.GuruswamiSudan.cpoly_truncate_coeff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (n i : ℕ) : (p.truncate n).coeff i = if i < n then p.coeff i else 0

theorem CompPoly.GuruswamiSudan.cbivar_coeff_truncateX {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (Q : CBivariate R) (n i j : ℕ) : (Q.truncateX n).coeff i j = if i < n then Q.coeff i j else 0

theorem CompPoly.GuruswamiSudan.polynomialPrefix_zero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : polynomialPrefix p 0 = 0

theorem CompPoly.GuruswamiSudan.polynomialPrefix_succ {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (p : CPolynomial F) (depth : ℕ) : polynomialPrefix p (depth + 1) = extendPrefix (polynomialPrefix p depth) depth (p.coeff depth)

theorem CompPoly.GuruswamiSudan.polynomialPrefix_eq_self_of_degreeLt {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] {p : CPolynomial F} {k : ℕ} (hdegree : degreeLt p k) : polynomialPrefix p k = p

theorem CompPoly.GuruswamiSudan.list_foldl_add_eq_sum {R : Type u_1} [AddMonoid R] (f : ℕ → R) (xs : List ℕ) (acc : R) : List.foldl (fun (acc : R) (i : ℕ) => acc + f i) acc xs = acc + (List.map f xs).sum

theorem CompPoly.GuruswamiSudan.list_sum_map_range_eq_finset_sum {R : Type u_1} [AddCommMonoid R] (f : ℕ → R) (n : ℕ) : (List.map f (List.range n)).sum = ∑ i ∈ Finset.range n, f i

theorem CompPoly.GuruswamiSudan.cpoly_eval_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (c : R) : CPolynomial.eval c (p + q) = CPolynomial.eval c p + CPolynomial.eval c q

theorem CompPoly.GuruswamiSudan.cpoly_eval_monomial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (y : ℕ) (a c : R) : CPolynomial.eval c (CPolynomial.monomial y a) = a * c ^ y

theorem CompPoly.GuruswamiSudan.composeY_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (P Q : CBivariate R) (p : CPolynomial R) : (P + Q).composeY p = P.composeY p + Q.composeY p

theorem CompPoly.GuruswamiSudan.composeY_outer_monomial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (c p : CPolynomial R) (y : ℕ) : CBivariate.composeY (CPolynomial.monomial y c) p = c * p ^ y

theorem CompPoly.GuruswamiSudan.cpoly_powCoeff_eq_coeff_pow {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) (k n : ℕ) : p.powCoeff k n = (p ^ k).coeff n

theorem CompPoly.GuruswamiSudan.cpoly_mulPowCoeff_eq_coeff_mul_pow {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (a p : CPolynomial R) (k n : ℕ) : a.mulPowCoeff p k n = (a * p ^ k).coeff n

theorem CompPoly.GuruswamiSudan.cpoly_coeff_zero_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p q : CPolynomial F) : (p * q).coeff 0 = p.coeff 0 * q.coeff 0

theorem CompPoly.GuruswamiSudan.cpoly_coeff_zero_pow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p : CPolynomial F) (n : ℕ) : (p ^ n).coeff 0 = p.coeff 0 ^ n

theorem CompPoly.GuruswamiSudan.cpoly_coeff_zero_pow_monomial_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (c : F) (n : ℕ) : (CPolynomial.monomial 0 c ^ n).coeff 0 = c ^ n

theorem CompPoly.GuruswamiSudan.cpoly_mulPowCoeff_monomial_zero_depth_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a : CPolynomial F) (c : F) (y : ℕ) : a.mulPowCoeff (CPolynomial.monomial 0 c) y 0 = a.coeff 0 * c ^ y

theorem CompPoly.GuruswamiSudan.composeY_coeff_zero_zipIdx_eq_range_aux {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (xs : List (CPolynomial F)) (p accPoly : CPolynomial F) (accCoeff : F) (offset : ℕ) (hacc : accPoly.coeff 0 = accCoeff) : List.foldl (fun (acc : F) (y : ℕ) => acc + (xs.getD (y - offset) 0).coeff 0 * p.coeff 0 ^ y) accCoeff (List.range' offset xs.length) = (List.foldl (fun (acc : CPolynomial F) (x : CPolynomial F × ℕ) => acc + x.1 * p ^ x.2) accPoly (xs.zipIdx offset)).coeff 0

theorem CompPoly.GuruswamiSudan.composeY_coeff_zero_fold_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (coeffs : Array (CPolynomial F)) (p : CPolynomial F) : List.foldl (fun (acc : F) (y : ℕ) => acc + (coeffs.getD y 0).coeff 0 * p.coeff 0 ^ y) 0 (List.range' 0 coeffs.size) = (Array.foldl (fun (acc : CPolynomial F) (x : CPolynomial F × ℕ) => acc + x.1 * p ^ x.2) 0 coeffs.zipIdx).coeff 0

theorem CompPoly.GuruswamiSudan.composeY_coeff_zipIdx_eq_range_aux {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (xs : List (CPolynomial R)) (p accPoly : CPolynomial R) (accCoeff : R) (offset n : ℕ) (hacc : accPoly.coeff n = accCoeff) : List.foldl (fun (acc : R) (y : ℕ) => acc + (xs.getD (y - offset) 0 * p ^ y).coeff n) accCoeff (List.range' offset xs.length) = (List.foldl (fun (acc : CPolynomial R) (x : CPolynomial R × ℕ) => acc + x.1 * p ^ x.2) accPoly (xs.zipIdx offset)).coeff n

theorem CompPoly.GuruswamiSudan.composeY_coeff_fold_eq {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (coeffs : Array (CPolynomial R)) (p : CPolynomial R) (n : ℕ) : List.foldl (fun (acc : R) (y : ℕ) => acc + (coeffs.getD y 0 * p ^ y).coeff n) 0 (List.range' 0 coeffs.size) = (Array.foldl (fun (acc : CPolynomial R) (x : CPolynomial R × ℕ) => acc + x.1 * p ^ x.2) 0 coeffs.zipIdx).coeff n

theorem CompPoly.GuruswamiSudan.composeYCoeff_eq_composeY_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (Q : CBivariate R) (p : CPolynomial R) (depth : ℕ) : Q.composeYCoeff p depth = (Q.composeY p).coeff depth

theorem CompPoly.GuruswamiSudan.fold_range_coeff_add_mul_pow {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (coeffs : Array (CPolynomial R)) (p : CPolynomial R) (ys : List ℕ) (acc : CPolynomial R) (accCoeff : R) (n : ℕ) : acc.coeff n = accCoeff → (List.foldl (fun (acc : CPolynomial R) (y : ℕ) => acc + coeffs.getD y 0 * p ^ y) acc ys).coeff n = List.foldl (fun (acc : R) (y : ℕ) => acc + (coeffs.getD y 0 * p ^ y).coeff n) accCoeff ys

theorem CompPoly.GuruswamiSudan.composeY_eq_range_fold {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (Q : CBivariate R) (p : CPolynomial R) : Q.composeY p = List.foldl (fun (acc : CPolynomial R) (y : ℕ) => acc + (↑Q).coeff y * p ^ y) 0 (List.range' 0 (Array.size ↑Q))

theorem CompPoly.GuruswamiSudan.composeY_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) : CBivariate.composeY 0 p = 0

theorem CompPoly.GuruswamiSudan.composeY_toPoly {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (p : CPolynomial F) : (Q.composeY p).toPoly = Polynomial.eval p.toPoly Q.toPoly

theorem CompPoly.GuruswamiSudan.initialCoefficientPolynomial_evalHorner_eq_composeYCoeff_monomial_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (c : F) : CPolynomial.evalHorner c (initialCoefficientPolynomial Q) = Q.composeYCoeff (CPolynomial.monomial 0 c) 0

theorem CompPoly.GuruswamiSudan.composeYCoeff_monomial_zero_eq_composeY_coeff_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (p : CPolynomial F) : Q.composeYCoeff (CPolynomial.monomial 0 (p.coeff 0)) 0 = (Q.composeY p).coeff 0

theorem CompPoly.GuruswamiSudan.initialCoefficientPolynomial_eval_eq_composeY_coeff_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (p : CPolynomial F) : CPolynomial.eval (p.coeff 0) (initialCoefficientPolynomial Q) = (Q.composeY p).coeff 0

theorem CompPoly.GuruswamiSudan.rootsInFieldForNonzeroEquation_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (fieldRoots : FieldRootContext F) {p : CPolynomial F} {a : F} (hp : p ≠ 0) (ha : CPolynomial.eval a p = 0) : a ∈ (rootsInFieldForNonzeroEquation fieldRoots p).toList

theorem CompPoly.GuruswamiSudan.composeY_of_composeYHorner_eq_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {Q : CBivariate F} {p : CPolynomial F} (h : Q.composeYHorner p = 0) : Q.composeY p = 0

theorem CompPoly.GuruswamiSudan.composeYHorner_eq_zero_of_composeY {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {Q : CBivariate F} {p : CPolynomial F} (h : Q.composeY p = 0) : Q.composeYHorner p = 0

theorem CompPoly.GuruswamiSudan.isRootYDegreeLtBool_of_root {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {Q : CBivariate F} {p : CPolynomial F} {k : ℕ} (hdegree : degreeLt p k) (hroot : Q.composeY p = 0) : isRootYDegreeLtBool Q k p = true

theorem CompPoly.GuruswamiSudan.rootsYDegreeLtFromCandidates_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {candidates : Array (CPolynomial F)} {Q : CBivariate F} {k : ℕ} {p : CPolynomial F} (h : p ∈ (rootsYDegreeLtFromCandidates candidates Q k).toList) : degreeLt p k ∧ Q.composeY p = 0

theorem CompPoly.GuruswamiSudan.rootsYDegreeLtFromCandidates_eraseDups_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {candidates : Array (CPolynomial F)} {Q : CBivariate F} {k : ℕ} {p : CPolynomial F} (h : p ∈ (rootsYDegreeLtFromCandidates candidates Q k).eraseDups.toList) : degreeLt p k ∧ Q.composeY p = 0

theorem CompPoly.GuruswamiSudan.rootsYDegreeLtFromCandidates_complete_of_mem {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {candidates : Array (CPolynomial F)} {Q : CBivariate F} {k : ℕ} {p : CPolynomial F} (hmem : p ∈ candidates.toList) (hdegree : degreeLt p k) (hroot : Q.composeY p = 0) : p ∈ (rootsYDegreeLtFromCandidates candidates Q k).toList

theorem CompPoly.GuruswamiSudan.rootsYDegreeLtFromCandidates_eraseDups_complete_of_mem {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {candidates : Array (CPolynomial F)} {Q : CBivariate F} {k : ℕ} {p : CPolynomial F} (hmem : p ∈ candidates.toList) (hdegree : degreeLt p k) (hroot : Q.composeY p = 0) : p ∈ (rootsYDegreeLtFromCandidates candidates Q k).eraseDups.toList