Correctness of fixed and scientific decimal output

The notation scanner recovers the decimal value selected by rounding in the fixed and scientific styles of format. Fixed output has at most half a decimal place of nearest-even error, and scientific output inherits the significant-digit bound. Neither decimal-point placement nor exponent notation introduces additional rounding. Every style raises at most inexact, and the exact styles raise nothing.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDecimal_nearest_error (value : Numerics.DecimalText.Decimal) (quantum : ℤ) : |(Numerics.DecimalText.roundDecimal (roundTextMagnitude IEEERoundingMode.nearest) 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_fixedText (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.Dyadic) : Numerics.DecimalText.parse (fixedText mode places value).text = some (roundFixed mode places (Numerics.DecimalText.ofDyadic value)).toRat

Fixed output denotes the decimal selected by rounding, without an extra rounding step.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_scientificText (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.Dyadic) : Numerics.DecimalText.parse (scientificText mode places value).text = some (roundScientific mode places (Numerics.DecimalText.ofDyadic value)).toRat

Scientific output denotes the decimal selected by rounding, without an extra rounding step.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundFixed_negative (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.DecimalText.Decimal) : (roundFixed mode places value).negative = value.negative

Fixed rounding preserves the sign, including when the result is zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundScientific_negative (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.DecimalText.Decimal) : (roundScientific mode places value).negative = value.negative

Scientific rounding preserves the sign, including when the result is zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fixedText_inexact_iff (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.Dyadic) : (fixedText mode places value).status.inexact = true ↔ (roundFixed mode places (Numerics.DecimalText.ofDyadic value)).toRat ≠ value.toRat

Fixed output raises inexact exactly when the rounding changes the numerical value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scientificText_inexact_iff (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.Dyadic) : (scientificText mode places value).status.inexact = true ↔ (roundScientific mode places (Numerics.DecimalText.ofDyadic value)).toRat ≠ value.toRat

Scientific output raises inexact exactly when the rounding changes the numerical value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.format_status {fmt : FloatFormat} (value : Model fmt) (style : TextStyle) (mode : IEEERoundingMode) : (value.format style mode true).status = { inexact := (value.format style mode true).status.inexact }

Text output can raise only inexact, so the other four exception indicators stay clear.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.format_exact_status {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) : (value.format TextStyle.exact mode true).status = { }

Exact decimal output raises none of the five exception indicators.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.format_hex_status {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) : (value.format TextStyle.hex mode true).status = { }

Exact hexadecimal output raises none of the five exception indicators.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_format_fixed_of_toDyadic? {fmt : FloatFormat} (mode : IEEERoundingMode) (places : ℕ) (value : Model fmt) (d : Numerics.Dyadic) (h : value.toDyadic? = some d) : Numerics.DecimalText.parse (value.format (TextStyle.fixed places) mode) = some (roundFixed mode places (Numerics.DecimalText.ofDyadic d)).toRat

A finite model's fixed output denotes its exact dyadic value rounded to places places.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_format_scientific_of_toDyadic? {fmt : FloatFormat} (mode : IEEERoundingMode) (places : ℕ) (value : Model fmt) (d : Numerics.Dyadic) (h : value.toDyadic? = some d) : Numerics.DecimalText.parse (value.format (TextStyle.scientific places) mode) = some (roundScientific mode places (Numerics.DecimalText.ofDyadic d)).toRat

A finite model's scientific output denotes its exact dyadic value rounded to places + 1 significant digits.

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

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

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

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