P3109 square-root rounding by exact square comparisons

For a nonnegative rational radicand, the floor candidate is sqrt (numerator / denominator) computed in natural numbers. Rounding compares the radicand with the square of an exact rational threshold. This decides rounding of the square root even when it is irrational.

Stochastic A and B select the upper candidate at their supplied random threshold. Stochastic C uses the half-integer threshold of its nearest-even integer rounding, including its tie parity. The random word is an explicit input, as in §4.7.4 of the P3109 4.0.3 working-group report.

Square root, reciprocal square root, and hypotenuse follow §§4.10.8 and 4.10.14 of that unapproved report. Each evaluates its exact radicand before the one rounding and saturation step.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtFloor (numerator denominator : ℕ) : ℕ

Floor of the nonnegative square root of numerator / denominator.

@[inline]

def FloatLib.Floats.Formats.P3109.Arithmetic.compareSqrt (numerator denominator scale threshold : ℕ) : Ordering

Compare sqrt (numerator / denominator) with threshold / scale by squaring. The denominator and threshold scale are positive at every arithmetic call site.

def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRoundDecision (format : Format) (mode : RoundingMode) (quantum : ℤ) (lower : ℕ) (exact : Bool) (compareThreshold : ℕ → ℕ → Ordering) : Bool

Select the upper candidate from exact threshold comparisons.

For stochastic A and B the threshold is the first fraction whose scaled floor reaches the required integer. For C it is the midpoint below that integer, with the integer's tie parity. The comparison argument permits the executable square comparisons and real semantics to share these policy rules.

def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRoundAway (format : Format) (mode : RoundingMode) (quantum : ℤ) (numerator denominator lower : ℕ) : Bool

The executable square-root boundary test for one report rounding mode.

def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtQuantum (format : Format) (numerator denominator : ℕ) : ℤ

The report's quantum for the square root of a positive rational.

def FloatLib.Floats.Formats.P3109.Arithmetic.roundSqrtRatToPrecision (format : Format) (mode : RoundingMode) (radicand : ℚ) : Numerics.Dyadic

Round the exact nonnegative square root to the descriptor's precision.

The integer division of the radicand's binary exponent by two is floor division, including negative exponents. The scaled numerator and denominator represent the square of the significand, so the scaling exponent is -2 * quantum.

Square-root callers establish that the radicand is nonnegative. On an arbitrary rational this precision helper rounds the square root of its absolute value.

def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRounded (format : Format) (mode : RoundingMode) : Numerics.NumericalValue ℚ → Numerics.NumericalValue Numerics.Dyadic

Square root in the closed domain, with precision rounding before saturation.

def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtValue (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue ℚ) : Numerics.NumericalValue Numerics.Dyadic

Apply the report saturation policy after square-root precision rounding.

def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtCode (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue ℚ) : BitVec format.bitWidth

Encode the already rounded and saturated square-root datum.

def FloatLib.Floats.Formats.P3109.Arithmetic.rsqrtRadicand : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact radicand for reciprocal square root, retaining its distinct nonpositive domain.

def FloatLib.Floats.Formats.P3109.Arithmetic.hypotRadicand : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact sum of squares for hypotenuse; either NaN takes precedence over infinity.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.projectSqrt (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (value : Numerics.NumericalValue ℚ) : P3109 destination

Project the exact square root of a closed rational datum.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.sqrtTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (value : P3109 source) : P3109 destination

Square root into an independent destination; negative inputs produce NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.rsqrtTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (value : P3109 source) : P3109 destination

Reciprocal square root with one final projection; nonpositive finite inputs produce NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.hypotTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (left : P3109 leftFormat) (right : P3109 rightFormat) : P3109 destination

Hypotenuse from the exact sum of squares, with no intermediate overflow or rounding.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.sqrt {format : Formats.P3109.Format} (value : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format square root, rounding the exact real value.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.rsqrt {format : Formats.P3109.Format} (value : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format reciprocal square root, rounding the exact real value.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.hypot {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format hypotenuse with one final projection of the exact norm.