Exact comparison rounding for binary algebraic operations

A comparison oracle orders a nonnegative real target against exact rational candidates. Two bounded searches locate its binade and a truncated significand with two extra bits. An exact comparison with the half-integer then supplies Lean's accuracy certificate. The final rounding discards that certificate once; no floating-point approximation of the target is needed.

The search bounds come from the complete descriptor. Custom biases and finite encodings use the descriptor-aware dyadic rounder with a representative of the same accuracy class.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.powerOfTwo (exponent : ℤ) : ℚ

Exact rational power of two, including negative exponents.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.bisect (accept : ℕ → Bool) : ℕ → ℕ → ℕ → ℕ

Reuse the total bounded integer search shared by exact posit operations.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.lowerExponent (fmt : FloatFormat) : ℤ

The lowest binade whose values can round to a nonzero encoding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.upperExponent (fmt : FloatFormat) : ℤ

An exclusive upper bound above every finite magnitude.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.exponentSpan (fmt : FloatFormat) : ℕ

Number of candidate exponent intervals.

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.binade (fmt : FloatFormat) (compare : ℚ → Ordering) : ℤ

Locate the binade by exact comparisons with powers of two.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.certificateExponent (fmt : FloatFormat) (binade : ℤ) : ℤ

Keep two bits below the final normal or subnormal rounding position.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.Certificate : Type

A truncated positive magnitude and the exact location of its discarded fraction.

• mantissa : ℕ

  Integer part of the magnitude after scaling by 2 ^ (-exponent).

• exponent : ℤ

  Power of two represented by one unit of the mantissa.

• accuracy : Float.Model.UnpackedFloat.Accuracy

  Whether the discarded fraction is zero, below a half, a half, or above a half.

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.truncatedMantissa (fmt : FloatFormat) (compare : ℚ → Ordering) (exponent : ℤ) : ℕ

Integer part of a scaled magnitude, found by exact comparisons.

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.accuracyAt (compare : ℚ → Ordering) (mantissa : ℕ) : Float.Model.UnpackedFloat.Accuracy

Exact fractional classification after finding the integer part.

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.certificate (fmt : FloatFormat) (compare : ℚ → Ordering) : Certificate

Build a certificate with a search bounded by the descriptor's precision.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.accuracyQuarter : Float.Model.UnpackedFloat.Accuracy → ℕ

A quarter-integer in the same accuracy class as a certificate's real mantissa.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.roundCertificate (fmt : FloatFormat) (sign : Bool) (c : Certificate) : Model fmt

Round a certificate once. Its exponent must be no greater than the target exponent; the constructor above reserves two guard bits to ensure this throughout the finite search interval.

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.round (fmt : FloatFormat) (sign : Bool) (compare : ℚ → Ordering) : Model fmt

Total nearest-even rounding of a signed magnitude given an exact comparison oracle.

The oracle's contract is comparison with a nonnegative real. At half the least subnormal, ties select signed zero. The upper cutoff uses the descriptor's overflow policy; values just below it still pass through the significand rounder, which handles overflow caused by carry.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.root (fmt : FloatFormat) (sign : Bool) (radicand : ℚ) (degree : ℕ) : Model fmt

Single-round evaluation of a nonnegative rational root.