Documentation

CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Basic

Approximant-Basis Guruswami-Sudan Modular Data #

Construction of the diagonal modular equations used by the approximant-basis interpolation backend.

References #

source
def CompPoly.GuruswamiSudan.ApproximantBasis.gsModuli {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : ℕ) :
Array (CPolynomial F)

GS column moduli M_b = G^(s-b), for b = 0, ..., s-1, built by iterated context multiplication so each power costs one fast product.

Instances For
    source
    def CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationEntry {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (modCtx : CPolynomial.ModContext F) (R modulus : CPolynomial F) (j b : ℕ) :
    CPolynomial F

    Specification for one relation-matrix entry choose(j,b) * R^(j-b) mod M_b, with zero below the triangular support. This is the reference definition; the production path builds whole columns incrementally with gsRelationColumn.

    Instances For
      source
      def CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationColumn {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R modulus : CPolynomial F) (width b : ℕ) :
      Array (CPolynomial F)

      One relation-matrix column, built by iterated multiply-and-reduce. Entry j of column b is choose(j,b) * R^(j-b) mod M_b; the reduced power of R is carried across entries so each step costs one context multiplication of operands already reduced below deg M_b plus one context remainder.

      Instances For
        source
        def CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationMatrixWithModuli {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R : CPolynomial F) (moduli : Array (CPolynomial F)) (params : GSInterpParams) :
        PolynomialMatrix F

        GS relation matrix for the congruences p * Fmat = 0 mod (G^s, ..., G), assembled from incrementally built columns over precomputed moduli.

        Instances For
          source
          def CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationMatrixWithRG {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R G : CPolynomial F) (params : GSInterpParams) :
          PolynomialMatrix F

          GS relation matrix for the congruences p * Fmat = 0 mod (G^s, ..., G).

          Instances For
            source
            structure CompPoly.GuruswamiSudan.ApproximantBasis.GSModularData (F : Type u_2) [Zero F] :
            Type u_2

            Complete GS modular-equation data for the approximant backend.

            Instances For
              source
              def CompPoly.GuruswamiSudan.ApproximantBasis.buildGSModularDataWithRG {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R G : CPolynomial F) (params : GSInterpParams) :
              GSModularData F

              Build column moduli, the binomial relation matrix, and the GS shift array from precomputed interpolation polynomials R and G. The moduli are computed once and shared with the relation-matrix construction.

              Instances For
                source
                def CompPoly.GuruswamiSudan.ApproximantBasis.buildGSModularData {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (points : Array (F × F)) (params : GSInterpParams) :
                GSModularData F

                Build G, R, column moduli, the binomial relation matrix, and the GS shift array.

                Instances For
                  source
                  def CompPoly.GuruswamiSudan.ApproximantBasis.modularEquation {F : Type u_1} [Field F] (data : GSModularData F) :
                  PolynomialMatrix.Approximant.ModularEquation F

                  Modular-equation view of GS modular data.

                  Instances For