TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Algebraic.Rounding.SqrtRuntime

Integer-root certificates for rational radicands #

The binary logarithm of the exact radicand locates the root's binade without searching the descriptor's exponent range. After target scaling, the proved integer-root kernel supplies the significand. Scaling is shared with the exact fractional classification, and the binade is reused when constructing the final certificate. Degree zero retains the total comparison specification.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootScale (radicand : ℚ) (degree : ℕ) (exponent : ℤ) :
ℕ × ℕ

Exact ratio after scaling a degree-degree root by 2 ^ (-exponent).

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.sqrtMantissa (radicand : ℚ) (exponent : ℤ) :
    ℕ

    Integer part of the square root after exact target scaling.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootBinade (radicand : ℚ) (degree : ℕ) :
      ℤ

      Floor binary logarithm of a positive root, using Euclidean division for negative exponents.

      Instances For
        source
        @[specialize #[0]]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootMantissa (fmt : FloatFormat) (radicand : ℚ) (degree : ℕ) (exponent : ℤ) :
        ℕ

        Exact integer part of a scaled root; degree zero retains the comparison specification.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.scaledRootAccuracy (numerator denominator degree mantissa : ℕ) :
          Float.Model.UnpackedFloat.Accuracy

          Classify the root's fractional part using its already scaled numerator and denominator.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootAccuracy (radicand : ℚ) (degree : ℕ) (exponent : ℤ) (mantissa : ℕ) :
            Float.Model.UnpackedFloat.Accuracy

            Integer cross-products classify the exact root against an integer and its midpoint.

            Instances For
              source
              @[specialize #[0]]
              def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootCertificateAt (fmt : FloatFormat) (radicand : ℚ) (degree : ℕ) (exponent : ℤ) :
              Certificate

              Build an integer-root certificate at a known exponent, sharing the exact scaled ratio.

              Instances For
                source
                @[specialize #[0]]
                def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootCertificate (fmt : FloatFormat) (radicand : ℚ) (degree : ℕ) :
                Certificate

                Build the same accuracy certificate using integer roots and the radicand's binary logarithm.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.sqrtCertificate (fmt : FloatFormat) (radicand : ℚ) :
                  Certificate

                  The degree-two specialization of the integer-root certificate.

                  Instances For
                    source
                    @[specialize #[0]]
                    def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootRat (fmt : FloatFormat) (sign : Bool) (radicand : ℚ) (degree : ℕ) :
                    Model fmt

                    Single-round rational root using integer binade classification and exact integer roots.

                    Only the exact underflow midpoint needs a power comparison at a descriptor boundary. Degree zero and nonpositive radicands retain the reference oracle's total behavior.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.sqrtRat (fmt : FloatFormat) (sign : Bool) (radicand : ℚ) :
                      Model fmt

                      Single-round rational square root without exponent or significand comparison searches.

                      Instances For
                        source
                        @[inline]
                        def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.rootWithSqrt (fmt : FloatFormat) (sign : Bool) (radicand : ℚ) (degree : ℕ) :
                        Model fmt

                        Use integer square root at degree two and proved integer Newton iteration otherwise.

                        Instances For