Documentation

CompPoly.Bivariate.GuruswamiSudan.Root.Common

Common Guruswami-Sudan Root Helpers #

Executable helpers shared by bounded bivariate root backends.

source
def CompPoly.GuruswamiSudan.initialCoefficientPolynomial {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) :
CPolynomial F

The coefficient of Y^j in Q(0, Y), as a polynomial in the next root coefficient.

Instances For
    source
    def CompPoly.GuruswamiSudan.isRootYDegreeLtBool {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (Q : CBivariate F) (k : ℕ) (p : CPolynomial F) :
    Bool

    Executable final check for the GS root condition.

    Instances For
      source
      def CompPoly.GuruswamiSudan.rootsYDegreeLtFromCandidates {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (candidates : Array (CPolynomial F)) (Q : CBivariate F) (k : ℕ) :
      Array (CPolynomial F)

      Filter a candidate family to exact bounded-degree roots.

      Instances For
        source
        def CompPoly.GuruswamiSudan.extendPrefix {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (pref : CPolynomial F) (depth : ℕ) (coeff : F) :
        CPolynomial F

        Extend one candidate prefix by one coefficient at X^depth.

        Instances For
          source
          def CompPoly.GuruswamiSudan.polynomialPrefix {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (n : ℕ) :
          CPolynomial R

          Truncate a polynomial to its first n coefficients.

          Instances For
            source
            def CompPoly.GuruswamiSudan.rootsInFieldForNonzeroEquation {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (fieldRoots : FieldRootContext F) (p : CPolynomial F) :
            Array F

            Query a field-root backend only for nonzero equations.

            A zero equation imposes no restriction on the next coefficient. Enumerating all field elements is unsuitable for large fields, so bounded-root backends use residual normalization to avoid zero equations for nonzero bivariate inputs.

            Instances For