Requested-precision guarantees for binary character output

The integer rounder is independent of the external radix and the binary descriptor. The shared radix laws then give coefficient bounds, fixed points and the numerical interpretation of the emitted characters.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundTextMagnitude_natCast (mode : IEEERoundingMode) (negative : Bool) (n : ℕ) : roundTextMagnitude mode negative ↑n = n

Every output rounding direction fixes a nonnegative integer.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundTextMagnitude_nearest_error (negative : Bool) (x : ℚ) (hx : 0 ≤ x) : |↑(roundTextMagnitude IEEERoundingMode.nearest negative x) - x| ≤ 1 / 2

Nearest-even integer output has error at most one half on a nonnegative magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.lt_roundTextMagnitude_nearestAway_iff (negative : Bool) (x : ℚ) (hx : 0 ≤ x) (bound : ℕ) : bound < roundTextMagnitude IEEERoundingMode.nearestAway negative x ↔ ↑bound + 1 / 2 ≤ x

Nearest-away integer output of a nonnegative magnitude exceeds a natural bound exactly when the magnitude reaches the bound plus one half.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floor_le_roundTextMagnitude (mode : IEEERoundingMode) (negative : Bool) (x : ℚ) : ⌊x⌋₊ ≤ roundTextMagnitude mode negative x

An external magnitude rounder never falls below floor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundTextMagnitude_le_nat (mode : IEEERoundingMode) (negative : Bool) (x : ℚ) (n : ℕ) (hx : 0 ≤ x) (hn : x ≤ ↑n) : roundTextMagnitude mode negative x ≤ n

An integer upper bound on a magnitude also bounds its rounded coefficient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantDecimal_coefficient_bounds (mode : IEEERoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (hc : value.significand ≠ 0) : 10 ^ (↑digits - 1) ≤ (Numerics.DecimalText.significantDecimal (roundTextMagnitude mode) value digits).significand ∧ (Numerics.DecimalText.significantDecimal (roundTextMagnitude mode) value digits).significand < 10 ^ ↑digits

Requested decimal output has exactly the requested digit count for nonzero inputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantDecimal_exact (mode : IEEERoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (hc : value.significand < 10 ^ ↑digits) : (Numerics.DecimalText.significantDecimal (roundTextMagnitude mode) value digits).toRat = value.toRat

Enough decimal digits preserve the exact value, for any binary descriptor and direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_formatDyadicText_significant_decimal (mode : IEEERoundingMode) (value : Numerics.Dyadic) (digits : ℕ+) : Numerics.DecimalText.parse (formatDyadicText mode TextRadix.decimal (Numerics.DecimalText.Precision.significant digits) value).text = some (Numerics.DecimalText.significantDecimal (roundTextMagnitude mode) (Numerics.DecimalText.ofDyadic value) digits).toRat

Decimal precision output parses to the grid-rounded value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_formatDyadicText_significant_hexadecimal (mode : IEEERoundingMode) (value : Numerics.Dyadic) (digits : ℕ+) : Numerics.HexText.parse (formatDyadicText mode TextRadix.hexadecimal (Numerics.DecimalText.Precision.significant digits) value).text = some (Numerics.HexText.significant (roundTextMagnitude mode) value digits)

Hexadecimal precision output parses to the complete rounded dyadic, including signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.formatDyadicText_decimal_inexact_iff (mode : IEEERoundingMode) (value : Numerics.Dyadic) (digits : ℕ+) : (formatDyadicText mode TextRadix.decimal (Numerics.DecimalText.Precision.significant digits) value).status.inexact = true ↔ (Numerics.DecimalText.significantDecimal (roundTextMagnitude mode) (Numerics.DecimalText.ofDyadic value) digits).toRat ≠ value.toRat

Decimal output raises inexact exactly when its numerical value changes.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.formatDyadicText_hexadecimal_inexact_iff (mode : IEEERoundingMode) (value : Numerics.Dyadic) (digits : ℕ+) : (formatDyadicText mode TextRadix.hexadecimal (Numerics.DecimalText.Precision.significant digits) value).status.inexact = true ↔ (Numerics.HexText.significant (roundTextMagnitude mode) value digits).toRat ≠ value.toRat

Hexadecimal output raises inexact exactly when its numerical value changes.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundTextMagnitude_nearest_midpoint (negative : Bool) (n : ℕ) : roundTextMagnitude IEEERoundingMode.nearest negative (↑n + 1 / 2) = if n % 2 = 0 then n else n + 1

At a halfway integer, the common output rounder selects the even neighbor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantMagnitude_nearest_error (radix : ℕ) (hradix : 1 < radix) (negative : Bool) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) : |↑(Numerics.RadixText.significant radix (roundTextMagnitude IEEERoundingMode.nearest) negative coefficient quantum digits).1 * ↑radix ^ (Numerics.RadixText.significant radix (roundTextMagnitude IEEERoundingMode.nearest) negative coefficient quantum digits).2 - ↑coefficient * ↑radix ^ quantum| ≤ ↑radix ^ Numerics.RadixText.significantQuantum radix coefficient quantum digits / 2

The same half-grid error guarantee holds in any external radix greater than one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantDecimal_nearest_error (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : |(Numerics.DecimalText.significantDecimal (roundTextMagnitude IEEERoundingMode.nearest) value digits).toRat - value.toRat| ≤ 10 ^ Numerics.DecimalText.significantQuantum value.significand value.exponent digits / 2

Nearest-even decimal output has at most half a requested decimal grid unit of error.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantHex_nearest_error (value : Numerics.Dyadic) (digits : ℕ+) : |(Numerics.HexText.significant (roundTextMagnitude IEEERoundingMode.nearest) value digits).toRat - value.toRat| ≤ 16 ^ Numerics.RadixText.significantQuantum 16 (Numerics.HexText.radixPair value).1 (Numerics.HexText.radixPair value).2 digits / 2

Nearest-even hexadecimal output has at most half a requested hexadecimal grid unit of error.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantHex_coefficient_bounds (mode : IEEERoundingMode) (value : Numerics.Dyadic) (digits : ℕ+) (hc : value.significand ≠ 0) : 16 ^ (↑digits - 1) ≤ (Numerics.HexText.significant (roundTextMagnitude mode) value digits).significand ∧ (Numerics.HexText.significant (roundTextMagnitude mode) value digits).significand < 16 ^ ↑digits

Requested hexadecimal output has exactly the requested digit count for nonzero input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_significantDecimal_up (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : value.toRat ≤ (Numerics.DecimalText.significantDecimal (roundTextMagnitude IEEERoundingMode.up) value digits).toRat

Decimal output rounded toward positive infinity is at least the exact input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantDecimal_down_le (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : (Numerics.DecimalText.significantDecimal (roundTextMagnitude IEEERoundingMode.down) value digits).toRat ≤ value.toRat

Decimal output rounded toward negative infinity is at most the exact input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantDecimal_towardZero_abs_le (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : |(Numerics.DecimalText.significantDecimal (roundTextMagnitude IEEERoundingMode.towardZero) value digits).toRat| ≤ |value.toRat|

Decimal output rounded toward zero cannot increase the magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_significantHex_up (value : Numerics.Dyadic) (digits : ℕ+) : value.toRat ≤ (Numerics.HexText.significant (roundTextMagnitude IEEERoundingMode.up) value digits).toRat

Hexadecimal output toward positive infinity is at least the exact input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantHex_down_le (value : Numerics.Dyadic) (digits : ℕ+) : (Numerics.HexText.significant (roundTextMagnitude IEEERoundingMode.down) value digits).toRat ≤ value.toRat

Hexadecimal output toward negative infinity is at most the exact input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significantHex_towardZero_abs_le (value : Numerics.Dyadic) (digits : ℕ+) : |(Numerics.HexText.significant (roundTextMagnitude IEEERoundingMode.towardZero) value digits).toRat| ≤ |value.toRat|

Hexadecimal output toward zero cannot increase the magnitude.