Documentation

CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Lemmas

Alekhnovich Root Search Lemmas #

Proof support for the Alekhnovich bounded bivariate root backend.

source
def CompPoly.GuruswamiSudan.RootMod {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (Q : CBivariate F) (p : CPolynomial F) (N : ℕ) :
Prop

p is a root of Q modulo X^N, stated as finitely many coefficient equalities.

Instances For
    source
    def CompPoly.GuruswamiSudan.MatchesPrefix {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (p f : CPolynomial F) (t : ℕ) :
    Prop

    f matches the first t coefficients of p.

    Instances For
      source
      def CompPoly.GuruswamiSudan.MatchesRootPrefix {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (p : CPolynomial F) (rp : RootPrefix F) :
      Prop

      rp is a root-prefix record matching the first rp.precision coefficients of p.

      Instances For
        source
        def CompPoly.GuruswamiSudan.SubstitutionDegreeBound {F : Type u_1} [Zero F] [BEq F] (Q : CBivariate F) (k N : ℕ) :
        Prop

        Logical exactness bound for substituting any degree < k univariate polynomial into Q.

        Instances For