Documentation

CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.FiniteField

Guruswami-Sudan Finite-Field Root Adapter #

Adapter from the reusable finite-field univariate root operation to the certified FieldRootContext context consumed by Roth-Ruckenstein root finding.

source
def CompPoly.GuruswamiSudan.finiteFieldRootContextWith (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F) (ctx : CPolynomial.Roots.FiniteField.FiniteFieldContext F) (splitter : CPolynomial.Roots.FiniteField.LinearFactorProductSplitter F) (splitterValid : ∀ {p : CPolynomial F}, p ≠ 0 → splitter.validInput ctx.q (CPolynomial.Roots.FiniteField.finiteFieldRootProductWith M D ctx p)) :
FieldRootContext F

Package the generic finite-field root finder as a GS field-root backend.

Instances For
    source
    def CompPoly.GuruswamiSudan.finiteFieldRootContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] (ctx : CPolynomial.Roots.FiniteField.FiniteFieldContext F) (splitter : CPolynomial.Roots.FiniteField.LinearFactorProductSplitter F) (splitterValid : ∀ {p : CPolynomial F}, p ≠ 0 → splitter.validInput ctx.q (CPolynomial.Roots.FiniteField.finiteFieldRootProduct ctx p)) :
    FieldRootContext F

    Package the generic finite-field root finder with the default raw arithmetic backends.

    Instances For
      source
      def CompPoly.GuruswamiSudan.smoothFiniteFieldRootContextWith (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] (M : CPolynomial.Raw.MulContext F) (D : CPolynomial.Raw.ModContext F) (ctx : CPolynomial.Roots.FiniteField.FiniteFieldContext F) (smoothCtx : CPolynomial.Roots.FiniteField.SmoothCyclicRootContext F) (smoothValid : ∀ {p : CPolynomial F}, p ≠ 0 → smoothCtx.validInput (CPolynomial.Roots.FiniteField.finiteFieldRootProductWith M D ctx p)) :
      FieldRootContext F

      Package a smooth cyclic splitter as a GS field-root backend.

      Instances For
        source
        def CompPoly.GuruswamiSudan.smoothFiniteFieldRootContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] (ctx : CPolynomial.Roots.FiniteField.FiniteFieldContext F) (smoothCtx : CPolynomial.Roots.FiniteField.SmoothCyclicRootContext F) (smoothValid : ∀ {p : CPolynomial F}, p ≠ 0 → smoothCtx.validInput (CPolynomial.Roots.FiniteField.finiteFieldRootProduct ctx p)) :
        FieldRootContext F

        Package a smooth cyclic splitter with default raw arithmetic as a GS field-root backend.

        Instances For