Decimal algebraic operations with one rounding

Squares and integer powers project an exact rational result. Reciprocal square root and hypotenuse pass an exact rational radicand to the square-root rounder: neither a reciprocal nor a sum of squares is rounded first.

Exact results select the preferred cohort. Integer powers multiply the operand quantum by the exponent; reciprocal square root uses the floor of its negated half-quantum; hypotenuse uses the smaller operand quantum.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.square (f : Format) (mode : RoundingMode) (x : Datum) : Outcome

Square with the same single rounding, preferred cohort, and flags as multiplication.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powerSign (negative : Bool) (exponent : ℤ) : Bool

Sign of an integer power, including negative odd exponents and signed zero.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.powInt (f : Format) (mode : RoundingMode) : Datum → ℤ → Outcome

Integer power with an exact rational intermediate and one final projection. A quiet NaN to power zero gives the rounded value one; a signaling NaN raises invalid. Negative powers of either zero raise divide-by-zero, with the odd-power sign.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.rsqrt (f : Format) (mode : RoundingMode) : Datum → Outcome

Reciprocal square root, rounding the root of the exact rational reciprocal. Either zero gives the correspondingly signed infinity and divide-by-zero. A negative nonzero input raises invalid; positive infinity gives positive zero.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.hypot (f : Format) (mode : RoundingMode) : Datum → Datum → Outcome

Hypotenuse with an exact sum of squares and one square-root rounding. An infinity dominates a quiet NaN. A signaling NaN raises invalid and propagates the first NaN's diagnostics, as in the other decimal binary operations.