Exact-rational P3109 projection

Configured binary floats, posits, integer inputs, and exact finite arithmetic can all supply exact rational values. This module projects them into any valid P3109 descriptor, rounding from the numerator and denominator with no intermediate approximation.

The runtime follows the same P3109 projection order as dyadic projection:

1. select the descriptor quantum;
2. round the exact quotient according to the requested P3109 mode;
3. apply the shared saturation rule;
4. encode the resulting datum.

The dyadic entry point suits a caller that already has an exact binary value. Both paths share saturation, encoding, and descriptor logic.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.scaleRationalFractionFloor (remainder denominator outputBits : ℕ) : ℕ

Floor of (remainder / denominator) * 2^outputBits.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.scaleRationalFractionNearestEven (remainder denominator outputBits : ℕ) : ℕ

Nearest-even integer to (remainder / denominator) * 2^outputBits.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.roundRationalAwayWithParity (mode : RoundingMode) (negative lowerEven : Bool) (remainder denominator : ℕ) : Bool

Decide whether exact rational rounding selects the integer above the quotient floor.

denominator is positive, as for every Rat. Passing it as its own argument lets the stochastic formulas follow P3109 Section 4.7.4 term by term.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.Internal.roundRationalAway (format : Format) (mode : RoundingMode) (negative : Bool) (quantumExponent : ℤ) (lower remainder denominator : ℕ) : Bool

P3109 rational rounding uses the descriptor's code parity, including precision one.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision (format : Format) (mode : RoundingMode) (exact : ℚ) : Numerics.Dyadic

Round one exact finite rational to the descriptor's P3109 precision.

The selected quantum is max(floor(log2 |x|), 1 - B) - P + 1. Scaling by the opposite quantum turns the rounding decision into one natural-number quotient and remainder. The result is an exact dyadic datum on the P3109 precision grid.

@[inline]

def FloatLib.Floats.Formats.P3109.Format.roundRatToPrecision (format : Format) (mode : RoundingMode) (value : Numerics.NumericalValue ℚ) : Numerics.NumericalValue Numerics.Dyadic

Apply P3109 precision rounding to an exact-rational closed value.

@[inline]

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

Exact-rational P3109 result before representation encoding.

@[inline]

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

Project one exact-rational closed value and return its descriptor-width code.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.projectRat {format : Formats.P3109.Format} (value : Numerics.NumericalValue ℚ) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 format

Project an exact rational, infinity, or exceptional observation into a P3109 descriptor.

Finite values are rounded once from their exact numerator and denominator, in mode, before saturation applies. No intermediate binary or host floating-point format is involved.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.ofRat {format : Formats.P3109.Format} (value : ℚ) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 format

Round one exact rational into a P3109 descriptor, nearest-even with no saturation request by default, as in ExecFloat.P3109.ofRat (format := .binary8p4se) (1 / 3) (mode := .up).