TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Sqrt.Runtime

Decimal square root by exact squared comparisons #

An integer square root brackets the scaled result. Comparing the radicand with the squared midpoint decides nearest rounding exactly, including ties. All decisions use integer and rational arithmetic.

The preferred exponent is the floor of half the operand quantum (IEEE 754-2019 §5.4.1). Negative zero survives, while a negative nonzero operand raises invalid (§§6.3, 7.2).

source
def FloatLib.Floats.Formats.DecimalInterchange.sqrtScaleShift (precision : ℕ) (scaledRadicand : ℚ) :
ℕ

Decimal scale shift for a square root, computed without evaluating a real square root.

Instances For
    source
    def FloatLib.Floats.Formats.DecimalInterchange.sqrtQuantum (f : Format) (radicand : ℚ) :
    ℤ

    Smallest coefficient grid which fits the exact square root.

    Instances For
      source
      def FloatLib.Floats.Formats.DecimalInterchange.sqrtFloor (radicand : ℚ) :
      ℕ

      Integer floor of a nonnegative rational's square root.

      Instances For
        source
        def FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.sqrtIncrement (mode : RoundingMode) (lower : ℕ) (radicand : ℚ) :
        Bool

        Decide the upper adjacent integer by exact comparison with a squared midpoint.

        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.sqrtRound (mode : RoundingMode) (radicand : ℚ) :
          ℕ

          Round a nonnegative square root on the integer grid.

          Instances For
            source
            def FloatLib.Floats.Formats.DecimalInterchange.sqrtPair (f : Format) (mode : RoundingMode) (radicand : ℚ) :
            ℕ × ℤ

            Rounded coefficient and quantum; an exact power-of-ten carry loses no value.

            Instances For
              source
              def FloatLib.Floats.Formats.DecimalInterchange.sqrtMagnitude (f : Format) (mode : RoundingMode) (radicand : ℚ) (preferred : ℤ) :
              Outcome

              Round the square root of a nonnegative rational, selecting the preferred cohort member when the result is exact.

              Instances For
                source
                def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.sqrt (f : Format) (mode : RoundingMode) :
                Datum → Outcome

                Square root in all five rounding modes, including signed zeros and NaN diagnostics.

                Instances For