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_nearestEven_error (negative : Bool) (x : ℚ) (hx : 0 ≤ x) : |↑(roundTextMagnitude IEEERoundingMode.nearestEven 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.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 exactly 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 precisely 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 precisely when its numerical value changes.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundTextMagnitude_nearestEven_midpoint (negative : Bool) (n : ℕ) : roundTextMagnitude IEEERoundingMode.nearestEven 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_nearestEven_error (radix : ℕ) (hradix : 1 < radix) (negative : Bool) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) : |↑(Numerics.RadixText.significant radix (roundTextMagnitude IEEERoundingMode.nearestEven) negative coefficient quantum digits).1 * ↑radix ^ (Numerics.RadixText.significant radix (roundTextMagnitude IEEERoundingMode.nearestEven) 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_nearestEven_error (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : |(Numerics.DecimalText.significantDecimal (roundTextMagnitude IEEERoundingMode.nearestEven) 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_nearestEven_error (value : Numerics.Dyadic) (digits : ℕ+) : |(Numerics.HexText.significant (roundTextMagnitude IEEERoundingMode.nearestEven) 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.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.formatWithStatus_exact_status {fmt : FloatFormat} (mode : IEEERoundingMode) (radix : TextRadix) (value : Model fmt) : (formatWithStatus mode radix Numerics.DecimalText.Precision.exact value).status = { }

Exact output raises none of the five exception indicators in either external radix.