Nearest-away conversion to binary

The rational is rounded to an integer on the destination binary grid. The rounded significand fits the precision, allowing one carry, so the binary encoder preserves its exact value whenever the delivered result is finite. This proves a single rounding, including ties away from zero, rather than assuming that two successive roundings agree.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.rat_eq_unsigned_div {x : ℚ} (hx : 0 ≤ x) : x = ↑x.num.natAbs / ↑x.den

A nonnegative rational is its unsigned numerator divided by its denominator.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.minSubnormalExponent_le_binaryQuantum (fmt : BinaryInterchange.FloatFormat) (x : ℚ) : fmt.minSubnormalExponent ≤ binaryQuantum fmt x

The binary grid exponent is never below the subnormal quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.div_binaryQuantum_lt (fmt : BinaryInterchange.FloatFormat) {x : ℚ} (hx : 0 < x) : x / 2 ^ binaryQuantum fmt x < 2 ^ (fmt.fracWidth + 1)

A positive magnitude scaled to its binary grid is below one full precision carry.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNearestAwayDyadic_significand_le (fmt : BinaryInterchange.FloatFormat) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : (binaryNearestAwayDyadic fmt s x).significand ≤ 2 ^ (fmt.fracWidth + 1)

The nearest-away significand fits the precision, with equality allowed for a carry.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNearestAwayDyadic_genericFormat (fmt : BinaryInterchange.FloatFormat) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : Flocq.genericFormat Numerics.binaryRadix (BinaryInterchange.Model.fexpOf fmt) (binaryNearestAwayDyadic fmt s x).toReal

The nearest-away dyadic lies on the destination grid before imposing its upper exponent bound. A carry is an exact change of exponent, not another rounding.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.roundBinaryMagnitude_nearestAway_eq (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (hfinite : (roundBinaryMagnitude fmt RoundingMode.nearestAway s x).isFinite = true) : (roundBinaryMagnitude fmt RoundingMode.nearestAway s x).toReal = (binaryNearestAwayDyadic fmt s x).toReal

Encoding the nearest-away dyadic preserves its exact real value on a finite result.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.roundBinaryMagnitude_nearestAway_error_le_half (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (hfinite : (roundBinaryMagnitude fmt RoundingMode.nearestAway s x).isFinite = true) : |(roundBinaryMagnitude fmt RoundingMode.nearestAway s x).toReal - if s = true then -↑x else ↑x| ≤ 2 ^ binaryQuantum fmt x / 2

A finite nearest-away conversion is within half a binary grid unit of the input. The grid is clamped at the subnormal quantum.