Guruswami-Sudan Interpolation Basics

Dense interpolation constraints and normalized witness helpers shared by concrete interpolation backends.

def CompPoly.GuruswamiSudan.interpolationMonomials (params : GSInterpParams) : Array CBivariate.Monomial

Weighted-degree monomial basis used by dense interpolation.

def CompPoly.GuruswamiSudan.interpolationYCap (params : GSInterpParams) : ℕ

Finite Y cap used by positive-Y-weight interpolation backends.

def CompPoly.GuruswamiSudan.interpolationWidth (params : GSInterpParams) : ℕ

Number of coefficient columns used by bounded-Y interpolation backends.

def CompPoly.GuruswamiSudan.interpolationShifts (params : GSInterpParams) : Array ℕ

Guruswami-Sudan shifted-degree shifts, shift[j] = j * yWeight params.

def CompPoly.GuruswamiSudan.distinctXCoordinatesListBool {F : Type u_1} [BEq F] : List (F × F) → Bool

Executable duplicate-x detector for packed point lists.

def CompPoly.GuruswamiSudan.distinctXCoordinatesBool {F : Type u_1} [BEq F] (points : Array (F × F)) : Bool

Executable duplicate-x detector for packed points.

structure CompPoly.GuruswamiSudan.InterpolationConstraint (F : Type u_1) : Type u_1

Packed interpolation constraint (x, y, a, b).

• x : F
• y : F
• xOrder : ℕ
• yOrder : ℕ

def CompPoly.GuruswamiSudan.instReprInterpolationConstraint.repr {F✝ : Type u_1} [Repr F✝] : InterpolationConstraint F✝ → ℕ → Std.Format

@[instance_reducible]

instance CompPoly.GuruswamiSudan.instReprInterpolationConstraint {F✝ : Type u_1} [Repr F✝] : Repr (InterpolationConstraint F✝)

def CompPoly.GuruswamiSudan.interpolationConstraints {F : Type u_1} (points : Array (F × F)) (multiplicity : ℕ) : Array (InterpolationConstraint F)

Hasse-derivative constraints for every point and every order a + b < m.

def CompPoly.GuruswamiSudan.hasseMonomialEval {F : Type u_1} [Semiring F] (monomial : CBivariate.Monomial) (constraint : InterpolationConstraint F) : F

One interpolation-matrix entry contributed by one monomial and one Hasse constraint.

def CompPoly.GuruswamiSudan.interpolationConstraintMatrixOnBasis {F : Type u_1} [Semiring F] (basis : Array CBivariate.Monomial) (constraints : Array (InterpolationConstraint F)) : DenseMatrix F

Dense Hasse-constraint matrix over an explicitly supplied monomial basis.

def CompPoly.GuruswamiSudan.interpolationConstraintMatrix {F : Type u_1} [Semiring F] (params : GSInterpParams) (constraints : Array (InterpolationConstraint F)) : DenseMatrix F

Dense Hasse-constraint matrix for the interpolation problem.

def CompPoly.GuruswamiSudan.interpolationMatrixOnBasis {F : Type u_1} [Semiring F] (basis : Array CBivariate.Monomial) (points : Array (F × F)) (params : GSInterpParams) : DenseMatrix F

Dense interpolation matrix for packed point pairs over an explicit basis.

def CompPoly.GuruswamiSudan.interpolationMatrix {F : Type u_1} [Semiring F] (points : Array (F × F)) (params : GSInterpParams) : DenseMatrix F

Dense interpolation matrix for packed point pairs.

def CompPoly.GuruswamiSudan.interpolationPolynomialOnBasis {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] [DecidableEq F] (basis : Array CBivariate.Monomial) (coeffs : Array F) : CBivariate F

Rebuild a bivariate polynomial from a dense coefficient vector over a supplied basis.

def CompPoly.GuruswamiSudan.interpolationPolynomial {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] [DecidableEq F] (params : GSInterpParams) (coeffs : Array F) : CBivariate F

Rebuild a bivariate polynomial from its dense interpolation coefficient vector.

def CompPoly.GuruswamiSudan.lowMessageDegreeInterpolation {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (points : Array (F × F)) (multiplicity : ℕ) : CBivariate F

Constructive interpolation witness for the messageDegree ≤ 1 GS range.

def CompPoly.GuruswamiSudan.interpolationCoefficientVectorOnBasis {F : Type u_1} [Zero F] (basis : Array CBivariate.Monomial) (Q : CBivariate F) : Array F

Coefficients of a bivariate polynomial in a supplied monomial order.

def CompPoly.GuruswamiSudan.interpolationCoefficientVector {F : Type u_1} [Zero F] (params : GSInterpParams) (Q : CBivariate F) : Array F

Coefficients of a bivariate polynomial in the interpolation monomial order.

def CompPoly.GuruswamiSudan.firstNonzeroIndex? {F : Type u_1} [Zero F] [BEq F] (v : Array F) : Option ℕ

The first nonzero vector coordinate, if one exists.

def CompPoly.GuruswamiSudan.normalizeVector? {F : Type u_1} [Field F] [BEq F] (v : Array F) : Option (Array F)

Normalize a nonzero vector by making its first nonzero coordinate equal to 1.

def CompPoly.GuruswamiSudan.IsNormalizedInterpolationWitness {F : Type u_1} [Zero F] [One F] [BEq F] (coeffs : Array F) : Prop

Predicate for the normalized interpolation-witness API.

def CompPoly.GuruswamiSudan.normalizeInterpolationPolynomialOnBasis? {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (basis : Array CBivariate.Monomial) (coeffs : Array F) : Option (CBivariate F)

Convert a homogeneous-kernel vector into a normalized basis polynomial.

def CompPoly.GuruswamiSudan.normalizeInterpolationPolynomial? {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (params : GSInterpParams) (coeffs : Array F) : Option (CBivariate F)

Convert a homogeneous-kernel vector into a normalized interpolation polynomial.

def CompPoly.GuruswamiSudan.HasInterpolationDimensionSlackOnBasis {F : Type u_1} (basis : Array CBivariate.Monomial) (points : Array (F × F)) (params : GSInterpParams) : Prop

Dimension slack for a supplied interpolation basis.

def CompPoly.GuruswamiSudan.HasInterpolationDimensionSlack {F : Type u_1} (points : Array (F × F)) (params : GSInterpParams) : Prop

Dimension slack condition that guarantees a nontrivial homogeneous kernel.

def CompPoly.GuruswamiSudan.interpolationWitnessIsValidBool {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (points : Array (F × F)) (params : GSInterpParams) (Q : CBivariate F) : Bool

Executable recognizer for the semantic interpolation witness contract.