Integer-to-decimal numerical contracts

Integer sources are converted from their exact value, with preferred quantum zero. Every integer representable in the destination remains exact, including integers whose decimal representation requires a positive exponent. Other nonoverflowing results satisfy the decimal grid's error and direction bounds.

Custom descriptors may exclude quantum zero. Zero then takes the nearest allowed quantum, and a coarse minimum quantum can make a nonzero integer underflow. The standard presets satisfy the optional HasQuantumZero assumption.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_valid (destination : Format) (mode : RoundingMode) (source : ℤ) : Datum.Valid destination (convertFromInt destination mode source).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_zero_clamped (destination : Format) (mode : RoundingMode) : convertFromInt destination mode 0 = { value := Datum.finite false 0 (max destination.minQuantum (min 0 destination.maxQuantum)) }

Integer zero is exact and positive, with its preferred exponent clamped to the destination interval. This includes custom descriptors that exclude quantum zero.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_zero (destination : Format) [destination.HasQuantumZero] (mode : RoundingMode) : convertFromInt destination mode 0 = { value := Datum.finite false 0 0 }

When quantum zero is available, integer zero keeps that exponent and raises no flags.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_exact (destination : Format) (mode : RoundingMode) (source : ℤ) (s : Bool) (c : ℕ) (q : ℤ) (hvalid : Datum.Valid destination (Datum.finite s c q)) (hs : (Datum.finite s c q).toRat? = some ↑source) : (convertFromInt destination mode source).value.toRat? = some ↑source ∧ (convertFromInt destination mode source).status = { }

Representability suffices for exact conversion; no coefficient-size restriction is imposed on the integer itself. Changing its cohort does not raise an exception.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_error_le_half (destination : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (source : ℤ) (hfinite : (convertFromInt destination mode source).status.overflow = false) : ∃ (value : ℚ), (convertFromInt destination mode source).value.toRat? = some value ∧ |value - ↑source| ≤ 10 ^ roundingQuantum destination |↑source| / 2

A nearest conversion incurs at most half a unit on the selected decimal grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_error_lt_one (destination : Format) (mode : RoundingMode) (source : ℤ) (hfinite : (convertFromInt destination mode source).status.overflow = false) : ∃ (value : ℚ), (convertFromInt destination mode source).value.toRat? = some value ∧ |value - ↑source| < 10 ^ roundingQuantum destination |↑source|

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.le_convertFromInt_towardPositive (destination : Format) (source : ℤ) (hfinite : (convertFromInt destination RoundingMode.towardPositive source).status.overflow = false) : ∃ (value : ℚ), (convertFromInt destination RoundingMode.towardPositive source).value.toRat? = some value ∧ ↑source ≤ value

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_towardNegative_le (destination : Format) (source : ℤ) (hfinite : (convertFromInt destination RoundingMode.towardNegative source).status.overflow = false) : ∃ (value : ℚ), (convertFromInt destination RoundingMode.towardNegative source).value.toRat? = some value ∧ value ≤ ↑source

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.abs_convertFromInt_towardZero_le (destination : Format) (source : ℤ) (hfinite : (convertFromInt destination RoundingMode.towardZero source).status.overflow = false) : ∃ (value : ℚ), (convertFromInt destination RoundingMode.towardZero source).value.toRat? = some value ∧ |value| ≤ |↑source|

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_inexact_iff (destination : Format) (mode : RoundingMode) (source : ℤ) (value : ℚ) (hfinite : (convertFromInt destination mode source).status.overflow = false) (hv : (convertFromInt destination mode source).value.toRat? = some value) : (convertFromInt destination mode source).status.inexact = true ↔ value ≠ ↑source

Inexact reports a numerical change, never a change of exponent alone.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_underflow_iff (destination : Format) (mode : RoundingMode) (source : ℤ) (value : ℚ) (hfinite : (convertFromInt destination mode source).status.overflow = false) (hv : (convertFromInt destination mode source).value.toRat? = some value) : (convertFromInt destination mode source).status.underflow = true ↔ |↑source| < destination.minNormal ∧ value ≠ ↑source

For an arbitrary descriptor, underflow means a tiny exact integer input together with a numerical change. Coarse custom formats can therefore underflow on integers.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt_underflow (destination : Format) [destination.HasQuantumZero] (mode : RoundingMode) (source : ℤ) : (convertFromInt destination mode source).status.underflow = false

When quantum zero is available, integer sources cannot underflow: every integer below the normal range is exactly representable as an integer coefficient. Larger integers are not tiny. The least normal value need not be at most one.