Binary-to-decimal conversion guarantees

Finite decoding feeds one exact rational projection. The proofs transfer its error bounds, directed inequalities and exception conditions to the returned decimal datum. Neither the binary storage width nor the decimal encoding choice occurs in the numerical argument.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_eq_project {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) (a : ℚ) (hx : x.toRat? = some a) : fromBinary f mode x = project f mode a 0 x.signBit

A successfully decoded binary value is projected once, with preferred quantum zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_valid {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) : Datum.Valid f (fromBinary f mode x).value

Binary conversion always returns a valid destination datum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_nan {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) (hx : x.isNaN = true) : fromBinary f mode x = { value := Datum.nan x.signBit false (if binaryPayload x < f.payloadBound then binaryPayload x else 0), status := { invalid := x.isSNaN } }

A source NaN is quieted, preserves a fitting diagnostic payload, and reports signaling.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_infinity {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) (hx : x.isInf = true) : fromBinary f mode x = { value := Datum.infinity x.signBit }

An infinite source retains its sign and raises no exception.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_zero_clamped {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) (hx : x.isZero = true) : fromBinary f mode x = { value := Datum.finite x.signBit 0 (max f.minQuantum (min 0 f.maxQuantum)) }

Both binary zeros retain their sign, with preferred quantum zero clamped to the destination quantum range.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_zero {fmt : BinaryInterchange.FloatFormat} (f : Format) [f.HasQuantumZero] (mode : RoundingMode) (x : BinaryInterchange.Model fmt) (hx : x.isZero = true) : fromBinary f mode x = { value := Datum.finite x.signBit 0 0 }

When quantum zero is available, both binary zeros convert to it with the same sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_error_le_half {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : BinaryInterchange.Model fmt) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (fromBinary f mode x).status.overflow = false) : ∃ (value : ℚ), (fromBinary f mode x).value.toRat? = some value ∧ |value - a| ≤ 10 ^ roundingQuantum f |a| / 2

Both nearest conversions bound the error of the returned decimal value by half a grid unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_error_lt_one {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (fromBinary f mode x).status.overflow = false) : ∃ (value : ℚ), (fromBinary f mode x).value.toRat? = some value ∧ |value - a| < 10 ^ roundingQuantum f |a|

All five conversion directions have less than one grid unit of nonoverflowing error.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.le_fromBinary_towardPositive {fmt : BinaryInterchange.FloatFormat} (f : Format) (x : BinaryInterchange.Model fmt) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (fromBinary f RoundingMode.towardPositive x).status.overflow = false) : ∃ (value : ℚ), (fromBinary f RoundingMode.towardPositive x).value.toRat? = some value ∧ a ≤ value

Upward conversion bounds the exact binary input from above.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_towardNegative_le {fmt : BinaryInterchange.FloatFormat} (f : Format) (x : BinaryInterchange.Model fmt) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (fromBinary f RoundingMode.towardNegative x).status.overflow = false) : ∃ (value : ℚ), (fromBinary f RoundingMode.towardNegative x).value.toRat? = some value ∧ value ≤ a

Downward conversion bounds the exact binary input from below.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_inexact_iff {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) (a value : ℚ) (hx : x.toRat? = some a) (hfinite : (fromBinary f mode x).status.overflow = false) (hv : (fromBinary f mode x).value.toRat? = some value) : (fromBinary f mode x).status.inexact = true ↔ value ≠ a

A cohort change is not inexact; inexactness detects precisely a numerical change.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary_underflow_iff {fmt : BinaryInterchange.FloatFormat} (f : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (fromBinary f mode x).status.overflow = false) : (fromBinary f mode x).status.underflow = true ↔ |a| < f.minNormal ∧ (fromBinary f mode x).status.inexact = true

Decimal conversion signals underflow precisely for an inexact tiny input.