Correctness of fixed and scientific decimal output

The notation scanner recovers the decimal value selected by rounding. Fixed output has at most half a decimal place of nearest-even error; scientific output inherits the significant-digit bound. Neither decimal-point placement nor exponent notation introduces additional rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDecimal_nearestEven_error (value : Numerics.DecimalText.Decimal) (quantum : ℤ) : |(Numerics.DecimalText.roundDecimal (roundTextMagnitude IEEERoundingMode.nearestEven) value quantum).toRat - value.toRat| ≤ 10 ^ quantum / 2

Nearest-even rounding on any decimal grid changes the value by at most half a grid unit.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_renderDecimalStyle (style : DecimalStyle) (value : Numerics.DecimalText.Decimal) : Numerics.DecimalText.parse (renderDecimalStyle style value) = some value.toRat

Either decimal notation denotes the original decimal, without an extra rounding step.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_formatDyadicDecimal (mode : IEEERoundingMode) (style : DecimalStyle) (value : Numerics.Dyadic) : Numerics.DecimalText.parse (formatDyadicDecimal mode style value).text = some (roundDecimalForStyle mode style (Numerics.DecimalText.ofDyadic value)).toRat

The characters denote precisely the value selected by decimal rounding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDecimalForStyle_negative (mode : IEEERoundingMode) (style : DecimalStyle) (value : Numerics.DecimalText.Decimal) : (roundDecimalForStyle mode style value).negative = value.negative

Choosing notation and precision preserves the sign, including when the result is zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.formatDyadicDecimal_inexact_iff (mode : IEEERoundingMode) (style : DecimalStyle) (value : Numerics.Dyadic) : (formatDyadicDecimal mode style value).status.inexact = true ↔ (roundDecimalForStyle mode style (Numerics.DecimalText.ofDyadic value)).toRat ≠ value.toRat

Inexact is set exactly when the decimal rounding changes the numerical value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.formatDecimalWithStatus_status {fmt : FloatFormat} (mode : IEEERoundingMode) (style : DecimalStyle) (value : Model fmt) : (formatDecimalWithStatus mode style value).status = { inexact := (formatDecimalWithStatus mode style value).status.inexact }

Decimal text has unbounded exponents; output rounding can raise only inexact.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_formatDecimalWithStatus_of_toDyadic? {fmt : FloatFormat} (mode : IEEERoundingMode) (style : DecimalStyle) (value : Model fmt) (d : Numerics.Dyadic) (h : value.toDyadic? = some d) : Numerics.DecimalText.parse (formatDecimalWithStatus mode style value).text = some (roundDecimalForStyle mode style (Numerics.DecimalText.ofDyadic d)).toRat

A finite model's output denotes its exact dyadic value rounded to the selected decimal grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.formatFixed_nearestEven_error {fmt : FloatFormat} (value : Model fmt) (d : Numerics.Dyadic) (h : value.toDyadic? = some d) (places : ℕ) : ∃ (result : ℚ), Numerics.DecimalText.parse (value.formatFixed places) = some result ∧ |result - d.toRat| ≤ 10 ^ (-↑places) / 2

The actual fixed-point string has at most half a last-place unit of nearest-even error.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.formatScientific_nearestEven_error {fmt : FloatFormat} (value : Model fmt) (d : Numerics.Dyadic) (h : value.toDyadic? = some d) (places : ℕ) : ∃ (result : ℚ), Numerics.DecimalText.parse (value.formatScientific places) = some result ∧ |result - d.toRat| ≤ 10 ^ Numerics.DecimalText.significantQuantum (Numerics.DecimalText.ofDyadic d).significand (Numerics.DecimalText.ofDyadic d).exponent ⟨places + 1, ⋯⟩ / 2

The actual scientific string inherits the nearest-even significant-digit error bound.