Documentation

CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Algorithm

Dense Guruswami-Sudan Interpolation #

Executable interpolation backend for the Guruswami-Sudan decoder [GS99]. For positive Y weight, it builds a Hasse-constraint matrix, computes one homogeneous-kernel witness, and normalizes it. For low message degree, it returns an explicit product witness.

References #

source
def CompPoly.GuruswamiSudan.denseInterpolateWithBasisAndKernel {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (kernelContext : LinearKernelContext F) (basis : Array CBivariate.Monomial) (points : Array (F × F)) (params : GSInterpParams) :
Option (CBivariate F)

Dense interpolation over an explicitly supplied finite monomial basis.

Instances For
    source
    def CompPoly.GuruswamiSudan.denseInterpolateWithKernel {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (kernelContext : LinearKernelContext F) (points : Array (F × F)) (params : GSInterpParams) :
    Option (CBivariate F)

    Interpolation through an explicit homogeneous-kernel backend, with a constructive low-message branch.

    When messageDegree ≤ 1, yWeight params = 0, so weighted degree alone does not bound the Y-degree. This branch returns an explicit product witness for the low-message-degree branch.

    Instances For
      source
      def CompPoly.GuruswamiSudan.denseInterpolate {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (points : Array (F × F)) (params : GSInterpParams) :
      Option (CBivariate F)

      Dense interpolation using the built-in Gaussian-elimination kernel backend.

      Instances For