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; nearest-away conversion has the exact integer-grid semantics proved in NearestAwayProof. The directed conversions inherit the binary kernels' extended-real enclosure bounds, which include overflow to infinity.

Exception theorems expose the exact 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 nor its flags.

@[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 := { } }

Infinities preserve their sign and raise 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 } }

A signaling NaN raises invalid; a quiet NaN does not. Both use the documented quiet payload-selection policy 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 source-signed binary zero 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 has one binary rounding. The observable finiteness condition excludes an infinite delivered result.

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 equals its exact rounded dyadic on the destination grid; the encoder contributes 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.