Posit rounding from exact rational comparisons

An exact result need not itself be rational. To round it, the posit search only needs to compare it with rational code values and appended-bit boundaries. This module shares that bounded search among algebraic and analytic operations whose comparisons can be decided exactly.

compareTarget q reports the ordering of the mathematical target relative to the rational q. The proof layer states this requirement explicitly; an approximate comparator cannot discharge it.

def FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.lowerCode (format : Format) (compareTarget : ℚ → Ordering) : ℕ

Locate the lower posit code using exact target-to-candidate comparisons.

def FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.roundCode (format : Format) (compareTarget : ℚ → Ordering) : ℕ

Round through the standard appended-bit boundaries, including even ties and saturation.

As with roundPositiveCode, targets at or below zero give zero. Signed operations round the magnitude and restore its sign outside this helper.

def FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.round (format : Format) (compareTarget : ℚ → Ordering) : Model format

Model-valued rounding from an exact comparison procedure.

def FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.roundSigned (format : Format) (compareTarget : ℚ → Ordering) : Model format

Signed rounding, using the comparator itself to determine the sign of the exact result.