TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Algebraic.Root.Runtime

Decimal integer-degree roots by exact power comparisons #

The integer root brackets the scaled coefficient. Comparing the radicand with the power of the exact midpoint decides nearest rounding, including ties. Precision, degree, and intermediate integers are unbounded.

Negative degrees invert the exact rational radicand before root rounding. Negative nonzero operands require an odd degree. Signed zeros follow the same odd-degree sign rule; a negative degree at zero raises divide-by-zero.

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

Decimal grid shift for a root of positive integer degree.

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

    Smallest coefficient grid which fits the exact nonnegative root.

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

      Integer floor of a nonnegative rational's positive-degree root.

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

        Exact decision between adjacent coefficients, with directed rounding respecting sign.

        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.rootRound (mode : RoundingMode) (negative : Bool) (degree : ℕ) (radicand : ℚ) :
          ℕ

          Round a nonnegative root magnitude on the integer grid.

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

            Rounded root coefficient and quantum, after an exact power-of-ten carry.

            Instances For
              source
              def FloatLib.Floats.Formats.DecimalInterchange.rootMagnitude (f : Format) (mode : RoundingMode) (negative : Bool) (degree : ℕ) (radicand : ℚ) (preferred : ℤ) :
              Outcome

              Round a positive-degree root of a nonnegative rational magnitude. Only the final root can raise overflow or underflow. Exact results retain the preferred cohort, and inexactness is decided by an exact power equality.

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

                Integer-degree root with one final rounding. Degree zero is invalid for every operand, including NaNs. Other degrees use the usual decimal NaN propagation. For an exact finite result, the preferred quantum is the floor of the signed operand quantum divided by the positive degree magnitude.

                Instances For