Documentation

CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Algorithm

Roth-Ruckenstein-Style Root Finding #

Executable bounded-degree roots for CBivariate F using recursive coefficient reconstruction and an explicit univariate field-root backend, following the Roth-Ruckenstein root-search step [RR00].

References #

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

Substitute Y = a + X * Y into a bivariate polynomial.

Instances For
    source
    def CompPoly.GuruswamiSudan.transformedRothRuckensteinResidual {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (a : F) :
    CBivariate F

    One residual step in the transformed Roth-Ruckenstein recursion.

    Instances For
      source
      def CompPoly.GuruswamiSudan.nextCoefficientSlope {F : Type u_1} [Field F] (Q : CBivariate F) (pref : CPolynomial F) :
      F

      The linear coefficient of the next recursive root equation after depth zero.

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

        Polynomial equation for the next coefficient in the prefix recursion.

        Instances For
          source
          def CompPoly.GuruswamiSudan.rootPrefixExtensionsWithFieldRootContext {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fieldRoots : FieldRootContext F) (Q : CBivariate F) (depth : ℕ) (prefixes : Array (CPolynomial F)) :
          List (CPolynomial F)

          Ordered recursive candidate extensions using a field-root backend.

          This direct coefficient-equation helper does not expand zero equations. The residual-transform Roth-Ruckenstein backend uses residual normalization before field-root queries.

          Instances For
            source
            def CompPoly.GuruswamiSudan.rothRuckensteinRootPrefixes {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fieldRoots : FieldRootContext F) (Q : CBivariate F) :
            ℕ → Array (CPolynomial F)

            Candidate prefixes after choosing coefficients through depth < k in the direct coefficient-equation recursion. Zero equations are not expanded.

            Instances For
              source
              def CompPoly.GuruswamiSudan.transformedRothRuckensteinRootPrefixesWithFuel {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fieldRoots : FieldRootContext F) :
              ℕ → CBivariate F → ℕ → CPolynomial F → Array (CPolynomial F)

              Residual-transform Roth-Ruckenstein prefixes with explicit recursion fuel.

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

                Candidate prefixes from the residual-transform recursion through precision X^k.

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

                  Residual-transform Roth-Ruckenstein bounded-degree roots.

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

                    Roth-Ruckenstein bounded-degree roots.

                    The public backend uses the residual-transform recursion, which strips common X-adic factors before each field-root query. Zero univariate equations are excluded from the field-root dependency for nonzero bivariate inputs.

                    Instances For