Executable rational-free exact posit quotient rounding

Finite posit operands are dyadic, but their quotient need not be. Correct rounding still requires no rational normalization and no materialized quotient. For a positive denominator d,

candidate ≤ numerator / d exactly when candidate * d ≤ numerator.

This module drives the standard logarithmic code search and every underflow, threshold, saturation, and tie decision with exact dyadic products. Refinement to rational division is proved in Quotient.Proof.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.lowerCode (format : Format) (numerator denominator : Numerics.Dyadic) : ℕ

Greatest nonnegative posit code whose decoded value does not exceed an exact positive quotient.

The quotient itself is never constructed. Multiplying each candidate by the positive denominator turns the comparison into a closed exact-dyadic operation.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.roundFromLowerCode (format : Format) (numerator denominator : Numerics.Dyadic) (lower : ℕ) : ℕ

Round from a known greatest lower quotient code.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.roundPositiveCode (format : Format) (numerator denominator : Numerics.Dyadic) : ℕ

Round a positive exact-dyadic quotient to a nonnegative posit code.

The total guard returns zero unless both carriers have the positive-magnitude shape established by the arithmetic caller. No division is executed: each comparison cross-multiplies by the denominator.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.roundPositive (format : Format) (numerator denominator : Numerics.Dyadic) : Model format

Pack the code chosen by exact cross-multiplied quotient rounding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.roundSignedWith (format : Format) (roundMagnitude : Numerics.Dyadic → Numerics.Dyadic → Model format) (numerator denominator : Numerics.Dyadic) : Model format

Apply the exceptional-value and sign policy shared by exact quotient kernels.

The caller supplies only the positive-magnitude rounder. Inlining this shell keeps the cross-multiplied and direct-prefix kernels specialized while giving both implementations one definition of division by zero, zero numerators, magnitude extraction, and sign restoration.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.round (format : Format) (numerator denominator : Numerics.Dyadic) : Model format

Round the quotient of two arbitrary signed dyadics without constructing the quotient.

A zero denominator produces NaR. With a nonzero denominator, a zero numerator produces the unique posit zero. Otherwise the positive magnitudes use cross-multiplied rounding and the result sign is restored by whole-word posit negation.