Guruswami-Sudan Polynomial Correctness Lemmas

Correctness lemmas for dense bivariate coefficient assembly, weighted-degree enumeration, and executable Hasse derivatives.

theorem CompPoly.CPolynomial.natDegree_mem_support_of_nonzero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} (hp : p ≠ 0) : p.natDegree ∈ p.support

The natural degree of a nonzero computable polynomial lies in its support.

theorem CompPoly.DenseMatrix.get_ofFn {F : Type u_1} [Zero F] (rows cols : ℕ) (f : ℕ → ℕ → F) {row col : ℕ} (hrow : row < rows) (hcol : col < cols) : (ofFn rows cols f).get row col = f row col

Reading an in-bounds entry from a matrix constructed by ofFn returns that entry.

theorem CompPoly.DenseMatrix.foldl_range_one_special {F : Type u_1} [AddCommMonoid F] {pivot : ℕ} (x : F) (start len : ℕ) (init : F) : List.foldl (fun (acc : F) (j : ℕ) => acc + if j = pivot then x else 0) init (List.range' start len) = init + if start ≤ pivot ∧ pivot < start + len then x else 0

Fold over a range with one distinguished nonzero entry.

theorem CompPoly.DenseMatrix.foldl_range_single_index {F : Type u_1} [AddCommMonoid F] {n k : ℕ} (hk : k < n) (x : F) : List.foldl (fun (acc : F) (j : ℕ) => acc + if j = k then x else 0) 0 (List.range' 0 n) = x

A range fold with a single distinguished index.

theorem CompPoly.DenseMatrix.foldl_range_eq_zero_of_zero {F : Type u_1} [AddMonoid F] {n : ℕ} {f : ℕ → F} (hzero : ∀ c < n, f c = 0) : List.foldl (fun (acc : F) (c : ℕ) => acc + f c) 0 (List.range' 0 n) = 0

A range fold with identically zero contributions is zero.

theorem CompPoly.CBivariate.coeff_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (i j : ℕ) : coeff 0 i j = 0

All bivariate coefficients of zero are zero.

theorem CompPoly.CBivariate.coeff_eq_zero_of_y_size_le {R : Type u_1} [Zero R] (Q : CBivariate R) {i j : ℕ} (hj : Array.size ↑Q ≤ j) : Q.coeff i j = 0

Bivariate coefficients past the stored outer array are zero.

theorem CompPoly.CBivariate.ofMonomialCoeffs_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (monomials : Array Monomial) (coeffs : Array R) (i j : ℕ) : (ofMonomialCoeffs monomials coeffs).coeff i j = List.foldl (fun (acc : R) (col : ℕ) => have monomial := monomials.getD col { xDegree := 0, yDegree := 0 }; acc + if i = monomial.xDegree ∧ j = monomial.yDegree then coeffs.getD col 0 else 0) 0 (List.range' 0 monomials.size)

Coefficients of a polynomial assembled from a monomial array are the folded sum of matching monomial coefficients.

theorem CompPoly.CBivariate.monomialGrid_nodup (bound : ℕ) : (monomialGrid bound).Nodup

The executable monomial grid has no duplicate exponent pairs.

theorem CompPoly.CBivariate.monomialsWeightedDegreeLE_nodup (xWeight yWeight bound : ℕ) : (monomialsWeightedDegreeLE xWeight yWeight bound).toList.Nodup

Weighted-degree monomial enumeration has no duplicate exponent pairs.

theorem CompPoly.CBivariate.monomialsWeightedDegreeLE_sound {xWeight yWeight bound : ℕ} {m : Monomial} (hm : m ∈ (monomialsWeightedDegreeLE xWeight yWeight bound).toList) : xWeight * m.xDegree + yWeight * m.yDegree ≤ bound

All returned weighted-degree monomials satisfy the requested bound.

theorem CompPoly.CBivariate.array_getD_inj_of_nodup {α : Type u_1} [DecidableEq α] {xs : Array α} {default : α} (hnodup : xs.toList.Nodup) {i j : ℕ} (hi : i < xs.size) (hj : j < xs.size) (h : xs.getD i default = xs.getD j default) : i = j

In a nodup array, equal in-bounds getD entries have equal indices.

theorem CompPoly.CBivariate.ofMonomialCoeffs_coeff_getD {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] {monomials : Array Monomial} {coeffs : Array R} (hnodup : monomials.toList.Nodup) {k : ℕ} (hk : k < monomials.size) : (ofMonomialCoeffs monomials coeffs).coeff (monomials.getD k { xDegree := 0, yDegree := 0 }).xDegree (monomials.getD k { xDegree := 0, yDegree := 0 }).yDegree = coeffs.getD k 0

For a nodup monomial array, the assembled polynomial recovers the matching coefficient at each listed monomial.

theorem CompPoly.CBivariate.ofMonomialCoeffs_ne_zero_of_coeff_getD_ne_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] {monomials : Array Monomial} {coeffs : Array R} (hnodup : monomials.toList.Nodup) {k : ℕ} (hk : k < monomials.size) (hcoeff : coeffs.getD k 0 ≠ 0) : ofMonomialCoeffs monomials coeffs ≠ 0

A nonzero coefficient at a listed monomial makes the assembled bivariate polynomial nonzero.

theorem CompPoly.CBivariate.natWeightedDegree_le_of_coeff_zero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (f : CBivariate R) (u v bound : ℕ) (hzero : ∀ (i j : ℕ), bound < u * i + v * j → f.coeff i j = 0) : f.natWeightedDegree u v ≤ bound

If all coefficients above a weighted-degree bound are zero, the executable weighted degree is below that bound.

theorem CompPoly.CBivariate.ofMonomialCoeffs_coeff_eq_zero_of_weight_gt {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] {monomials : Array Monomial} {coeffs : Array R} {u v bound i j : ℕ} (hall : ∀ monomial ∈ monomials.toList, u * monomial.xDegree + v * monomial.yDegree ≤ bound) (hgt : bound < u * i + v * j) : (ofMonomialCoeffs monomials coeffs).coeff i j = 0

Coefficients above a bound are zero for a polynomial assembled from monomials all below that bound.

theorem CompPoly.CBivariate.ofMonomialCoeffs_natWeightedDegree_le {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] {monomials : Array Monomial} {coeffs : Array R} {u v bound : ℕ} (hall : ∀ monomial ∈ monomials.toList, u * monomial.xDegree + v * monomial.yDegree ≤ bound) : (ofMonomialCoeffs monomials coeffs).natWeightedDegree u v ≤ bound

A polynomial assembled from bounded monomials has weighted degree below the same bound.

theorem CompPoly.CBivariate.hasseDerivativeFromTerms_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (terms : List (HasseTerm R)) (i j : ℕ) : (hasseDerivativeFromTerms terms).coeff i j = List.foldl (fun (acc : R) (term : HasseTerm R) => acc + if i = term.xDegree ∧ j = term.yDegree then term.coeff else 0) 0 terms

Coefficients of a polynomial materialized from Hasse terms are the folded sum of matching term coefficients.

theorem CompPoly.CBivariate.hasseDerivativeEvalFromTerms_append_single {R : Type u_1} [Semiring R] (terms : List (HasseTerm R)) (term : HasseTerm R) (x y : R) : hasseDerivativeEvalFromTerms (terms ++ [term]) x y = hasseDerivativeEvalFromTerms terms x y + term.coeff * x ^ term.xDegree * y ^ term.yDegree

Evaluating after appending one Hasse term adds that term's contribution.

theorem CompPoly.CBivariate.hasseDerivativeTermList_coeff_fold {R : Type u_1} [Semiring R] (a b i j : ℕ) (Q : CBivariate R) : List.foldl (fun (acc : R) (term : HasseTerm R) => acc + if i = term.xDegree ∧ j = term.yDegree then term.coeff else 0) 0 (hasseDerivativeTermList a b Q) = List.foldl (fun (acc : R) (yDeg : ℕ) => have coeffY := (↑Q).coeff yDeg; if b ≤ yDeg then List.foldl (fun (acc : R) (xDeg : ℕ) => if a ≤ xDeg then acc + if i = xDeg - a ∧ j = yDeg - b then ↑(xDeg.choose a) * ↑(yDeg.choose b) * coeffY.coeff xDeg else 0 else acc) acc (List.range' 0 (Array.size ↑coeffY)) else acc) 0 (List.range' 0 (Array.size ↑Q))

The fixed coefficient of the executable Hasse term list is the matching coefficient fold over the same degree ranges.

theorem CompPoly.CBivariate.hasseDerivativeTermList_coeff_inner_fold {R : Type u_1} [Semiring R] (a b i j yDeg : ℕ) (coeffY : CPolynomial R) (acc : R) (hy : b ≤ yDeg) : List.foldl (fun (acc : R) (xDeg : ℕ) => if a ≤ xDeg then acc + if i = xDeg - a ∧ j = yDeg - b then ↑(xDeg.choose a) * ↑(yDeg.choose b) * coeffY.coeff xDeg else 0 else acc) acc (List.range' 0 (Array.size ↑coeffY)) = acc + if yDeg = j + b ∧ i + a < Array.size ↑coeffY then ↑((i + a).choose a) * ↑(yDeg.choose b) * coeffY.coeff (i + a) else 0

Collapse the inner x-fold in a fixed Hasse coefficient calculation.

theorem CompPoly.CBivariate.hasseDerivativeTermList_coeff_value {R : Type u_1} [Semiring R] (a b i j : ℕ) (Q : CBivariate R) : List.foldl (fun (acc : R) (term : HasseTerm R) => acc + if i = term.xDegree ∧ j = term.yDegree then term.coeff else 0) 0 (hasseDerivativeTermList a b Q) = ↑((i + a).choose a) * ↑((j + b).choose b) * Q.coeff (i + a) (j + b)

The fixed coefficient of the executable Hasse term list has the closed coefficient-shift formula.

theorem CompPoly.CBivariate.hasseDerivative_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b i j : ℕ) (Q : CBivariate R) : (hasseDerivative a b Q).coeff i j = ↑((i + a).choose a) * ↑((j + b).choose b) * Q.coeff (i + a) (j + b)

Coefficients of the executable Hasse derivative are shifted source coefficients scaled by the corresponding binomial factors.

theorem CompPoly.CBivariate.hasseDerivative_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : ℕ) (P Q : CBivariate R) : hasseDerivative a b (P + Q) = hasseDerivative a b P + hasseDerivative a b Q

Hasse derivatives are additive.

theorem CompPoly.CBivariate.hasseDerivative_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : ℕ) : hasseDerivative a b 0 = 0

The Hasse derivative of zero is zero.

theorem CompPoly.CBivariate.hasseDerivative_monomialXY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b n m : ℕ) (c : R) : hasseDerivative a b (monomialXY n m c) = if a ≤ n ∧ b ≤ m then monomialXY (n - a) (m - b) (↑(n.choose a) * ↑(m.choose b) * c) else 0

Hasse derivative of a single bivariate monomial.

theorem CompPoly.CBivariate.evalEval_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (x y : R) (P Q : CBivariate R) : evalEval x y (P + Q) = evalEval x y P + evalEval x y Q

Full evaluation is additive.

theorem CompPoly.CBivariate.evalEval_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (x y : R) : evalEval x y 0 = 0

Full evaluation of zero is zero.

theorem CompPoly.CBivariate.evalEval_monomialXY {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (x y c : R) (n m : ℕ) : evalEval x y (monomialXY n m c) = c * x ^ n * y ^ m

Full evaluation of a bivariate monomial has the expected closed form.

theorem CompPoly.CBivariate.hasseDerivativeTerms_eval_aux {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (x y : R) (terms : List (HasseTerm R)) (acc : CBivariate R) : evalEval x y (List.foldl (fun (out : CBivariate R) (term : HasseTerm R) => out + monomialXY term.xDegree term.yDegree term.coeff) acc terms) = List.foldl (fun (z : R) (term : HasseTerm R) => z + term.coeff * x ^ term.xDegree * y ^ term.yDegree) (evalEval x y acc) terms

Evaluating the materialized derivative-term fold matches the direct scalar fold.

theorem CompPoly.CBivariate.hasseDerivativeFromTerms_eval {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (x y : R) (terms : List (HasseTerm R)) : evalEval x y (hasseDerivativeFromTerms terms) = hasseDerivativeEvalFromTerms terms x y

Evaluating a materialized derivative-term polynomial matches direct term evaluation.

theorem CompPoly.CBivariate.hasseDerivative_eval_eq_eval {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : ℕ) (x y : R) (Q : CBivariate R) : evalEval x y (hasseDerivative a b Q) = hasseDerivativeEval a b x y Q

Correctness of executable Hasse derivative evaluation.

theorem CompPoly.CBivariate.eval_hasseDeriv_eval_hasseDeriv_toPoly {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (x y : F) (a b : ℕ) : Polynomial.eval x ((Polynomial.hasseDeriv a) (Polynomial.eval (Polynomial.C y) ((Polynomial.hasseDeriv b) Q.toPoly))) = hasseDerivativeEval a b x y Q

Evaluating the univariate X-Hasse derivative of the evaluated Y-Hasse derivative matches the executable bivariate Hasse derivative.

theorem CompPoly.CBivariate.coeff_shiftC_eq_hasseDerivativeEval {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (x y : F) (a b : ℕ) : (shiftC x y Q).coeff a b = hasseDerivativeEval a b x y Q

The coefficient of the generic Taylor shift is the direct Hasse derivative evaluation at the shift point.

theorem CompPoly.CBivariate.hasMultiplicity_iff_hasMultiplicityAtLeast {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (r : ℕ) (x y : F) : Q.hasMultiplicity r x y ↔ Q.HasMultiplicityAtLeast x y r

The generic multiplicity predicate agrees with the direct GS Hasse multiplicity predicate.

theorem CompPoly.CBivariate.satisfiesMultiplicityConstraints_iff_hasMultiplicity {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (points : Array (F × F)) (r : ℕ) : Q.SatisfiesMultiplicityConstraints points r ↔ ∀ point ∈ points.toList, Q.hasMultiplicity r point.1 point.2

The GS batch Hasse predicate agrees with the generic multiplicity predicate over every packed point.

theorem CompPoly.CBivariate.multiplicityAtLeastBool_iff_hasMultiplicity {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (x y : F) (r : ℕ) : Q.multiplicityAtLeastBool x y r = true ↔ Q.hasMultiplicity r x y

The executable GS point checker agrees with the generic multiplicity predicate.

theorem CompPoly.CBivariate.satisfiesMultiplicityConstraintsBool_iff_hasMultiplicity {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (points : Array (F × F)) (r : ℕ) : Q.satisfiesMultiplicityConstraintsBool points r = true ↔ ∀ point ∈ points.toList, Q.hasMultiplicity r point.1 point.2

The executable GS batch checker agrees with the generic multiplicity predicate over every packed point.

theorem CompPoly.CBivariate.multiplicityAtLeastBool_iff_checkMultiplicity {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (x y : F) (r : ℕ) : Q.multiplicityAtLeastBool x y r = true ↔ Q.checkMultiplicity r x y = true

The executable GS point checker agrees with the generic boolean checker.

theorem CompPoly.CBivariate.satisfiesMultiplicityConstraintsBool_iff_checkMultiplicity {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (points : Array (F × F)) (r : ℕ) : Q.satisfiesMultiplicityConstraintsBool points r = true ↔ ∀ point ∈ points.toList, Q.checkMultiplicity r point.1 point.2 = true

The executable GS batch checker agrees pointwise with the generic boolean checker over the packed point array.

theorem CompPoly.CBivariate.hasseDerivativeEval_add {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : ℕ) (x y : R) (P Q : CBivariate R) : hasseDerivativeEval a b x y (P + Q) = hasseDerivativeEval a b x y P + hasseDerivativeEval a b x y Q

Direct Hasse evaluation is additive in the input polynomial.

theorem CompPoly.CBivariate.hasseDerivativeEval_zero {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : ℕ) (x y : R) : hasseDerivativeEval a b x y 0 = 0

Direct Hasse evaluation of zero is zero.