Decimal-to-binary conversion contracts

Finite decimal inputs are evaluated as exact rationals, independently of their cohort. Nearest-even conversion refines binary rounded-real semantics, and nearest-away conversion has the integer-grid semantics proved in NearestAwayProof. The directed conversions inherit the binary kernels' extended-real enclosure bounds, which include overflow to infinity.

Exception theorems state the overflow and tininess predicates, including the distinction between exponent overflow and an inexact result at the largest finite value.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.signedScaledRatToReal_eq_rat (s : Bool) {x : ℚ} (hx : 0 ≤ x) : BinaryInterchange.Model.signedScaledRatToReal s x.num.natAbs x.den 0 = if s = true then -↑x else ↑x

Signed natural quotient semantics agree with the exact rational input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_eq_of_magnitude_eq (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s : Bool) (c₁ c₂ : ℕ) (q₁ q₂ : ℤ) (h : ↑c₁ * 10 ^ q₁ = ↑c₂ * 10 ^ q₂) : toBinary fmt hfmt mode (Datum.finite s c₁ q₁) = toBinary fmt hfmt mode (Datum.finite s c₂ q₂)

The source cohort affects neither the rounded binary value, its flags, nor its ternary value.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_infinity (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s : Bool) : toBinary fmt hfmt mode (Datum.infinity s) = { value := BinaryInterchange.Model.infinityOrMaxFinite fmt s, status := { }, ternary := Ordering.eq }

An infinity keeps its sign and raises no exception.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_nan (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s signaling : Bool) (payload : ℕ) : toBinary fmt hfmt mode (Datum.nan s signaling payload) = { value := binaryNaN fmt s payload, status := { invalid := signaling }, ternary := Ordering.eq }

A signaling NaN raises invalid and a quiet NaN does not. Both deliver the quiet NaN of binaryNaN and raise no other flag.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.roundBinaryMagnitude_zero (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s : Bool) : roundBinaryMagnitude fmt mode s 0 = BinaryInterchange.Model.zero fmt s

Zero magnitude rounds to the binary zero of sign s in every mode.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.roundBinaryMagnitude_nearestEven_eq (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (hfinite : (roundBinaryMagnitude fmt RoundingMode.nearestEven s x).isFinite = true) : (roundBinaryMagnitude fmt RoundingMode.nearestEven s x).toReal = BinaryInterchange.Model.roundAt fmt (if s = true then -↑x else ↑x)

Finite nearest-even rational conversion equals binary rounded-real semantics.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_nearestEven_eq (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) (c : ℕ) (q : ℤ) (hfinite : (toBinary fmt hfmt RoundingMode.nearestEven (Datum.finite s c q)).value.isFinite = true) : (toBinary fmt hfmt RoundingMode.nearestEven (Datum.finite s c q)).value.toReal = BinaryInterchange.Model.roundAt fmt ↑(Datum.finiteValue s c q)

Nearest-even conversion of a finite decimal input is one binary rounding of its value, provided the delivered result is finite.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_nearestAway_eq (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) (c : ℕ) (q : ℤ) (hfinite : (toBinary fmt hfmt RoundingMode.nearestAway (Datum.finite s c q)).value.isFinite = true) : (toBinary fmt hfmt RoundingMode.nearestAway (Datum.finite s c q)).value.toReal = (binaryNearestAwayDyadic fmt s (↑c * 10 ^ q)).toReal

Nearest-away conversion of a finite decimal input with a finite result delivers its rounded dyadic on the destination grid, so the encoder adds no second rounding.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.le_roundBinaryMagnitude_towardPositive (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : ↑(if s = true then -↑x else ↑x) ≤ (roundBinaryMagnitude fmt RoundingMode.towardPositive s x).toEReal

Upward rational conversion encloses the exact input, including an infinite result.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.roundBinaryMagnitude_towardNegative_le (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : (roundBinaryMagnitude fmt RoundingMode.towardNegative s x).toEReal ≤ ↑(if s = true then -↑x else ↑x)

Downward rational conversion encloses the exact input, including an infinite result.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.le_toBinary_towardPositive (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) (c : ℕ) (q : ℤ) : ↑↑(Datum.finiteValue s c q) ≤ (toBinary fmt hfmt RoundingMode.towardPositive (Datum.finite s c q)).value.toEReal

Conversion toward positive infinity is an extended-real upper bound.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_towardNegative_le (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (s : Bool) (c : ℕ) (q : ℤ) : (toBinary fmt hfmt RoundingMode.towardNegative (Datum.finite s c q)).value.toEReal ≤ ↑↑(Datum.finiteValue s c q)

Conversion toward negative infinity is an extended-real lower bound.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_towardZero_positive_le (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (c : ℕ) (q : ℤ) : (toBinary fmt hfmt RoundingMode.towardZero (Datum.finite false c q)).value.toEReal ≤ ↑↑(Datum.finiteValue false c q)

A positive decimal input rounded toward zero does not increase.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.le_toBinary_towardZero_negative (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (c : ℕ) (q : ℤ) : ↑↑(Datum.finiteValue true c q) ≤ (toBinary fmt hfmt RoundingMode.towardZero (Datum.finite true c q)).value.toEReal

A negative decimal input rounded toward zero does not decrease.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_finite_invalid (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) : (toBinary fmt hfmt mode (Datum.finite s c q)).status.invalid = false

A finite decimal input cannot raise invalid during numeric conversion.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_divideByZero (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (x : Datum) : (toBinary fmt hfmt mode x).status.divideByZero = false

Numeric conversion cannot raise division-by-zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_overflow_iff (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) : (toBinary fmt hfmt mode (Datum.finite s c q)).status.overflow = true ↔ binaryOverflow fmt mode s (↑c * 10 ^ q) = true

The finite conversion path raises overflow exactly at the mode's rational boundary.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_inexact_iff (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) : (toBinary fmt hfmt mode (Datum.finite s c q)).status.inexact = true ↔ (toBinary fmt hfmt mode (Datum.finite s c q)).status.overflow = true ∨ (toBinary fmt hfmt mode (Datum.finite s c q)).value.toRat? ≠ some (Datum.finiteValue s c q)

Inexact means exponent overflow or a changed exact rational value.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary_underflow_iff (fmt : BinaryInterchange.FloatFormat) (hfmt : fmt.isIEEE = true) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) : (toBinary fmt hfmt mode (Datum.finite s c q)).status.underflow = true ↔ (toBinary fmt hfmt mode (Datum.finite s c q)).status.overflow = false ∧ binaryTiny fmt mode s (↑c * 10 ^ q) (toBinary fmt hfmt mode (Datum.finite s c q)).value = true ∧ (toBinary fmt hfmt mode (Datum.finite s c q)).status.inexact = true

Underflow is an inexact tiny result without exponent overflow. Tininess is measured after rounding to the destination precision with an unbounded exponent range.