Documentation

CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Algorithm

Alekhnovich Bivariate Bounded Root Search #

Executable batched X-adic root lifting for the Guruswami-Sudan bivariate root phase. The public output is exactly filtered against Q(X, p(X)) = 0 and degree p < k, following Alekhnovich's lattice-based root-search approach [Ale05].

References #

source
structure CompPoly.GuruswamiSudan.RootPrefix (F : Type u_1) [Zero F] :
Type u_1

A prefix coset prefixPoly + X^precision * g(X).

Instances For
    source
    @[instance_reducible]
    instance CompPoly.GuruswamiSudan.instBEqRootPrefix {F✝ : Type u_1} {inst✝ : Zero F✝} [BEq F✝] :
    BEq (RootPrefix F✝)
    source
    def CompPoly.GuruswamiSudan.instBEqRootPrefix.beq {F✝ : Type u_1} {inst✝ : Zero F✝} [BEq F✝] :
    RootPrefix F✝ → RootPrefix F✝ → Bool
    Instances For
      source
      def CompPoly.GuruswamiSudan.instDecidableEqRootPrefix.decEq {F✝ : Type u_1} {inst✝ : Zero F✝} [DecidableEq F✝] (x✝ x✝¹ : RootPrefix F✝) :
      Decidable (x✝ = x✝¹)
      Instances For
        source
        @[instance_reducible]
        instance CompPoly.GuruswamiSudan.instDecidableEqRootPrefix {F✝ : Type u_1} {inst✝ : Zero F✝} [DecidableEq F✝] :
        DecidableEq (RootPrefix F✝)
        source
        def CompPoly.GuruswamiSudan.alekhnovichPrecisionBound {F : Type u_1} [Zero F] [BEq F] (Q : CBivariate F) (k : ℕ) :
        ℕ

        Precision requested by the Alekhnovich top-level root search.

        This asks for a small margin over the exactness bound; exact filtering remains the public soundness boundary.

        Instances For
          source
          structure CompPoly.GuruswamiSudan.AlekhnovichResidual (F : Type u_1) [Zero F] :
          Type u_1

          Normalized shifted residual and its stripped X-adic valuation.

          Instances For
            source
            def CompPoly.GuruswamiSudan.instBEqAlekhnovichResidual.beq {F✝ : Type u_1} {inst✝ : Zero F✝} [BEq F✝] :
            AlekhnovichResidual F✝ → AlekhnovichResidual F✝ → Bool
            Instances For
              source
              @[instance_reducible]
              instance CompPoly.GuruswamiSudan.instBEqAlekhnovichResidual {F✝ : Type u_1} {inst✝ : Zero F✝} [BEq F✝] :
              BEq (AlekhnovichResidual F✝)
              source
              def CompPoly.GuruswamiSudan.instDecidableEqAlekhnovichResidual.decEq {F✝ : Type u_1} {inst✝ : Zero F✝} [DecidableEq F✝] (x✝ x✝¹ : AlekhnovichResidual F✝) :
              Decidable (x✝ = x✝¹)
              Instances For
                source
                @[instance_reducible]
                instance CompPoly.GuruswamiSudan.instDecidableEqAlekhnovichResidual {F✝ : Type u_1} {inst✝ : Zero F✝} [DecidableEq F✝] :
                DecidableEq (AlekhnovichResidual F✝)
                source
                def CompPoly.GuruswamiSudan.shiftedResidualUpTo {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (f : CPolynomial F) (t N : ℕ) :
                AlekhnovichResidual F

                Shift, truncate, strip the visible X-adic factor, and report the residual.

                Instances For
                  source
                  def CompPoly.GuruswamiSudan.composeRootPrefixes {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (outer suffix : RootPrefix F) :
                  RootPrefix F

                  Compose an outer prefix with a suffix prefix returned by a residual call.

                  Instances For
                    source
                    def CompPoly.GuruswamiSudan.normalizeAlekhnovichInput {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (Q : CBivariate F) (N : ℕ) :
                    Option (CBivariate F × ℕ)

                    Normalize a residual by stripping an initial common X factor only up to the requested precision. Returning none means the current equation is unconstrained modulo the requested precision.

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

                      Alekhnovich root prefixes with explicit fuel.

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

                        Alekhnovich root prefixes through the requested precision.

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

                          Finish one Alekhnovich prefix with Alekhnovich-only recursive suffix completion. Prefixes already at precision k are simply truncated to the final degree bound.

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

                            Materialize bounded-degree candidates from Alekhnovich prefixes.

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

                              Finish one Alekhnovich prefix with Alekhnovich-only suffix completion.

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

                                Materialize bounded-degree candidates from Alekhnovich prefixes.

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

                                  Alekhnovich bounded-degree roots, with exact final filtering and deduplication. The zero bivariate input follows the finite-output convention used by the Roth backend and returns no roots.

                                  Instances For