Guarantees for significant-digit output

The carry adjustment preserves value. The emitted characters therefore denote the result of the existing exact integer-grid rounder, with its nearest and directed error guarantees. The inexact flag detects a numerical change even when the requested precision changes the output quantum.

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

Every nonzero output coefficient has exactly the requested number of decimal digits.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal_value (mode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : (significantDecimal mode value digits).toRat = (if value.negative = true then -1 else 1) * ↑(mode.roundAt value.negative (↑value.significand * 10 ^ value.exponent) (Numerics.DecimalText.significantQuantum value.significand value.exponent digits)) * 10 ^ Numerics.DecimalText.significantQuantum value.significand value.exponent digits

The significant-digit result is one integer-grid rounding of the exact input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal_negative (mode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : (significantDecimal mode value digits).negative = value.negative

Output retains the sign, including for zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.le_significantDecimal_towardPositive (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : value.toRat ≤ (significantDecimal RoundingMode.towardPositive value digits).toRat

Upward decimal output is an upper enclosure at every requested precision.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal_towardNegative_le (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : (significantDecimal RoundingMode.towardNegative value digits).toRat ≤ value.toRat

Downward decimal output is a lower enclosure at every requested precision.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.abs_significantDecimal_towardZero_le (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : |(significantDecimal RoundingMode.towardZero value digits).toRat| ≤ |value.toRat|

Toward-zero decimal output does not increase magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal_nearestEven_midpoint (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (n : ℕ) (hmid : ↑value.significand * 10 ^ value.exponent / 10 ^ Numerics.DecimalText.significantQuantum value.significand value.exponent digits = ↑n + 1 / 2) : (significantDecimal RoundingMode.nearestEven value digits).toRat = (if value.negative = true then -1 else 1) * ↑(if n % 2 = 1 then n + 1 else n) * 10 ^ Numerics.DecimalText.significantQuantum value.significand value.exponent digits

At a midpoint, nearest-even output selects the even adjacent grid coefficient.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal_nearestAway_midpoint (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (n : ℕ) (hmid : ↑value.significand * 10 ^ value.exponent / 10 ^ Numerics.DecimalText.significantQuantum value.significand value.exponent digits = ↑n + 1 / 2) : (significantDecimal RoundingMode.nearestAway value digits).toRat = (if value.negative = true then -1 else 1) * ↑(n + 1) * 10 ^ Numerics.DecimalText.significantQuantum value.significand value.exponent digits

At a midpoint, nearest-away output selects the larger magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal_exact (mode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (hc : value.significand < 10 ^ ↑digits) : (significantDecimal mode value digits).toRat = value.toRat

Enough requested digits preserve the exact numerical value in every rounding mode.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal_exact_of_valid (f : Format) (mode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (hvalid : Datum.Valid f (Datum.finite value.negative value.significand value.exponent)) (hp : f.precision ≤ ↑digits) : (significantDecimal mode value digits).toRat = value.toRat

The descriptor precision suffices for every valid datum, with no restriction on exponent bias.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal_error_le_half (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : |(significantDecimal mode value digits).toRat - value.toRat| ≤ 10 ^ Numerics.DecimalText.significantQuantum value.significand value.exponent digits / 2

Both nearest modes have at most half a requested grid unit of error.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.read_format_significant (mode : RoundingMode) (digits : ℕ+) (value : Numerics.DecimalText.Decimal) : read (format mode (Numerics.DecimalText.Precision.significant digits) (Datum.finite value.negative value.significand value.exponent)).text = some (Datum.finite (significantDecimal mode value digits).negative (significantDecimal mode value digits).significand (significantDecimal mode value digits).exponent)

Actual output characters decode to the computed significant-digit record.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.format_significant_inexact_iff (mode : RoundingMode) (digits : ℕ+) (value : Numerics.DecimalText.Decimal) : (format mode (Numerics.DecimalText.Precision.significant digits) (Datum.finite value.negative value.significand value.exponent)).status.inexact = true ↔ (significantDecimal mode value digits).toRat ≠ value.toRat

Requested-precision output sets inexact exactly when its character value differs from the input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_format_significant_value (f : Format) (outputMode inputMode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (hvalid : Datum.Valid f (Datum.finite value.negative value.significand value.exponent)) (hp : f.precision ≤ ↑digits) : (parse f inputMode (format outputMode (Numerics.DecimalText.Precision.significant digits) (Datum.finite value.negative value.significand value.exponent)).text).value.toRat? = (Datum.finite value.negative value.significand value.exponent).toRat?

At least the format precision preserves numerical value through actual output and input. The two conversions may use different rounding modes; the quantum need not be recovered.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.format_significant_status_of_valid (f : Format) (mode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (hvalid : Datum.Valid f (Datum.finite value.negative value.significand value.exponent)) (hp : f.precision ≤ ↑digits) : (format mode (Numerics.DecimalText.Precision.significant digits) (Datum.finite value.negative value.significand value.exponent)).status = { }

Sufficient-precision output raises none of the five IEEE flags.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_format_significant_status (f : Format) (outputMode inputMode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) (hvalid : Datum.Valid f (Datum.finite value.negative value.significand value.exponent)) (hp : f.precision ≤ ↑digits) : (parse f inputMode (format outputMode (Numerics.DecimalText.Precision.significant digits) (Datum.finite value.negative value.significand value.exponent)).text).status = { }

Parsing sufficient-precision output raises no flags, even if its written quantum cannot fit.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.format_exact (mode : RoundingMode) (value : Datum) : format mode Numerics.DecimalText.Precision.exact value = { text := formatExact value }

Exact precision returns the representation-preserving spelling without flags.