Guruswami-Sudan Polynomial Helpers

Reusable univariate and bivariate polynomial operations used by the Guruswami-Sudan interpolation and root-finding kernels.

def CompPoly.CPolynomial.dropXPower {R : Type u_1} [Zero R] (p : CPolynomial R) : ℕ → CPolynomial R

Drop the first n powers of X, i.e. divide by X^n when possible and truncate toward zero otherwise.

def CompPoly.CPolynomial.truncate {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (n : ℕ) : CPolynomial R

Keep only coefficients of degree < n.

def CompPoly.CPolynomial.xAdicOrder? {R : Type u_1} [Zero R] [BEq R] (p : CPolynomial R) : Option ℕ

First nonzero coefficient index of a univariate polynomial, if it is nonzero.

def CompPoly.CPolynomial.inverseSeriesNextCoeff {F : Type u_1} [Field F] (p : CPolynomial F) (constantInv : F) (prev : Array F) (idx : ℕ) : F

Coefficients of the inverse of a power series with known nonzero constant coefficient, truncated to length n.

def CompPoly.CPolynomial.inverseSeriesCoeffs {F : Type u_1} [Field F] (p : CPolynomial F) (constantInv : F) (n : ℕ) : Array F

Coefficients of the inverse of a power series with known nonzero constant coefficient, truncated to length n.

def CompPoly.CPolynomial.inverseSeries? {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p : CPolynomial F) (n : ℕ) : Option (CPolynomial F)

Inverse of a univariate power series modulo X^n, if the constant term is invertible.

def CompPoly.CPolynomial.mulCoeff {R : Type u_1} [Semiring R] (p q : CPolynomial R) (n : ℕ) : R

Coefficient of X^n in p * q, computed without materializing the product.

def CompPoly.CPolynomial.mulWindow {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (low width : ℕ) : CPolynomial R

Coefficient window of p * q, shifted down by low and truncated to width, computed without materializing the full product.

def CompPoly.CPolynomial.mulWindowWithLowProduct {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (mulLow : Raw.MulLowContext R) (p q : CPolynomial R) (low width : ℕ) : CPolynomial R

Coefficient window of p * q computed through a raw low-product context.

def CompPoly.CPolynomial.powCoeff {R : Type u_1} [Semiring R] (p : CPolynomial R) : ℕ → ℕ → R

Coefficient of X^n in p^k, computed by coefficient convolution without materializing the intermediate powers.

def CompPoly.CPolynomial.mulPowCoeff {R : Type u_1} [Semiring R] (a p : CPolynomial R) (k n : ℕ) : R

Coefficient of X^n in a * p^k, computed coefficient-wise.

structure CompPoly.CBivariate.Monomial : Type

A bivariate monomial exponent pair.

• xDegree : ℕ
• yDegree : ℕ

def CompPoly.CBivariate.instBEqMonomial.beq : Monomial → Monomial → Bool

@[instance_reducible]

instance CompPoly.CBivariate.instBEqMonomial : BEq Monomial

def CompPoly.CBivariate.instDecidableEqMonomial.decEq (x✝ x✝¹ : Monomial) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance CompPoly.CBivariate.instDecidableEqMonomial : DecidableEq Monomial

def CompPoly.CBivariate.instReprMonomial.repr : Monomial → ℕ → Std.Format

@[instance_reducible]

instance CompPoly.CBivariate.instReprMonomial : Repr Monomial

structure CompPoly.CBivariate.HasseTerm (R : Type u_1) : Type u_1

One monomial contribution to a Hasse derivative.

• xDegree : ℕ
• yDegree : ℕ
• coeff : R

def CompPoly.CBivariate.ofCoeffGrid {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (grid : Array (Array R)) : CBivariate R

Construct a bivariate polynomial from a coefficient grid indexed by grid[y][x].

def CompPoly.CBivariate.ofMonomialCoeffs {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (monomials : Array Monomial) (coeffs : Array R) : CBivariate R

Construct a bivariate polynomial from a monomial list and parallel coefficient vector.

def CompPoly.CBivariate.monomialGrid (bound : ℕ) : List Monomial

Candidate monomials in the finite square used by weighted-degree enumeration.

def CompPoly.CBivariate.monomialsWeightedDegreeLE (xWeight yWeight bound : ℕ) : Array Monomial

Enumerate monomials inside a finite weighted-degree search rectangle.

When both weights are positive this is the complete set of monomials with weighted degree at most bound. If a weight is zero, bound also serves as the finite exponent cap for that variable.

def CompPoly.CBivariate.hasseDerivativeTermList {R : Type u_1} [Semiring R] (a b : ℕ) (Q : CBivariate R) : List (HasseTerm R)

Shared monomial contributions for materialized and directly evaluated Hasse derivatives.

def CompPoly.CBivariate.hasseDerivativeTerms {R : Type u_1} [Semiring R] (a b : ℕ) (Q : CBivariate R) : Array (HasseTerm R)

Shared monomial contributions for materialized and directly evaluated Hasse derivatives.

def CompPoly.CBivariate.hasseDerivativeFromTerms {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (terms : List (HasseTerm R)) : CBivariate R

Materialize a Hasse derivative from a list of derivative terms.

def CompPoly.CBivariate.hasseDerivative {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : ℕ) (Q : CBivariate R) : CBivariate R

Executable Hasse derivative of a bivariate polynomial.

def CompPoly.CBivariate.hasseDerivativeEvalFromTerms {R : Type u_1} [Semiring R] (terms : List (HasseTerm R)) (x y : R) : R

Evaluate derivative terms directly at one point.

def CompPoly.CBivariate.hasseDerivativeEval {R : Type u_1} [Semiring R] (a b : ℕ) (x y : R) (Q : CBivariate R) : R

Evaluate a Hasse derivative at one point without materializing the derivative.

def CompPoly.CBivariate.derivativeOrderGrid (multiplicity : ℕ) : List (ℕ × ℕ)

Candidate derivative orders in the finite square used by multiplicity checks.

def CompPoly.CBivariate.derivativeOrders (multiplicity : ℕ) : Array (ℕ × ℕ)

Derivative orders (a, b) with a + b < multiplicity.

def CompPoly.CBivariate.HasMultiplicityAtLeast {R : Type u_1} [Semiring R] (Q : CBivariate R) (x y : R) (multiplicity : ℕ) : Prop

Mathematical multiplicity constraint used by the GS interpolation specification.

def CompPoly.CBivariate.multiplicityAtLeastBool {R : Type u_1} [Semiring R] [BEq R] (Q : CBivariate R) (x y : R) (multiplicity : ℕ) : Bool

Executable multiplicity check at one point.

def CompPoly.CBivariate.SatisfiesMultiplicityConstraints {R : Type u_1} [Semiring R] (Q : CBivariate R) (points : Array (R × R)) (multiplicity : ℕ) : Prop

Mathematical batch multiplicity constraints over packed point pairs.

def CompPoly.CBivariate.satisfiesMultiplicityConstraintsBool {R : Type u_1} [Semiring R] [BEq R] (Q : CBivariate R) (points : Array (R × R)) (multiplicity : ℕ) : Bool

Executable batch multiplicity check over packed point pairs.

def CompPoly.CBivariate.composeY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (Q : CBivariate R) (p : CPolynomial R) : CPolynomial R

Compose a bivariate polynomial with a univariate polynomial in the Y slot: Q(X, p(X)).

@[inline, specialize #[]]

def CompPoly.CBivariate.composeYHorner {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (Q : CBivariate R) (p : CPolynomial R) : CPolynomial R

Horner implementation of Q(X, p(X)) in the outer Y variable.

@[inline, specialize #[]]

def CompPoly.CBivariate.composeYHornerTruncated {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (Q : CBivariate R) (p : CPolynomial R) (n : ℕ) : CPolynomial R

Truncated Horner implementation of Q(X, p(X)) in the outer Y variable.

After each Horner step, the accumulator is truncated modulo X^n, so callers that only need an X-adic certificate do not materialize coefficients that will be discarded immediately.

def CompPoly.CBivariate.composeYCoeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (Q : CBivariate R) (p : CPolynomial R) (depth : ℕ) : R

Coefficient of X^depth in Q(X, p(X)), computed without materializing the whole composed polynomial.

def CompPoly.CBivariate.yDerivative {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) : CBivariate R

Formal derivative in the outer Y variable.

def CompPoly.CBivariate.xAdicOrder? {R : Type u_1} [Zero R] [BEq R] (Q : CBivariate R) : Option ℕ

Minimum X-adic order across all nonzero Y-coefficients of a bivariate polynomial.

def CompPoly.CBivariate.divXPower {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (Q : CBivariate R) (n : ℕ) : CBivariate R

Divide every Y-coefficient by X^n, truncating coefficients with lower X-degree to zero.

def CompPoly.CBivariate.truncateX {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (Q : CBivariate R) (n : ℕ) : CBivariate R

Keep only coefficients of X-degree < n in every Y-coefficient.

def CompPoly.CBivariate.stripXAdicFactor {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (Q : CBivariate R) : CBivariate R

Strip the common X-adic factor from a bivariate polynomial.

def CompPoly.CBivariate.ofYConstant {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : CBivariate R

View a univariate polynomial in X as a bivariate polynomial constant in Y.

def CompPoly.CBivariate.ofYCoefficient {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (y : ℕ) (p : CPolynomial R) : CBivariate R

View a univariate polynomial in X as the coefficient of Y^y in a bivariate polynomial.