Decimal text roundtrips

The character scanner recovers the full datum. Destination rounding then fixes every valid datum: preferred-cohort optimality recovers the printed quantum, and numerical exactness recovers its coefficient. This preserves more than a rational value: signed zeros, trailing coefficient zeros, and NaN diagnostics survive a format/parse roundtrip.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.projectMagnitude_same_quantum (f : Format) (mode : RoundingMode) (negative : Bool) (coefficient : ℕ) (quantum : ℤ) (hvalid : Datum.Valid f (Datum.finite negative coefficient quantum)) : (projectMagnitude f mode negative (↑coefficient * 10 ^ quantum) quantum).value = Datum.finite negative coefficient quantum

Projection with a representable input's own quantum preserves its full representation.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.convert_of_valid (f : Format) (mode : RoundingMode) (value : Datum) (hvalid : Datum.Valid f value) : convert f mode value = { value := value }

Valid decoded datums are fixed, with no flags, in every rounding mode.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.readCharacters_characters (value : Datum) : readCharacters (characters value) = some value

Decoding the exact character spelling recovers every field, without a format restriction.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.read_formatExact (value : Datum) : read (formatExact value) = some value

Exact output and unbounded parsing are inverses, including all NaNs and signed zeros.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_formatExact (f : Format) (mode : RoundingMode) (value : Datum) (hvalid : Datum.Valid f value) : parse f mode (formatExact value) = { value := value }

Full destination-format representation roundtrip, in every rounding mode and with no flags.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.formatExact_injective : Function.Injective formatExact

Distinct datums, including members of the same cohort, have distinct exact spellings.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.convert_valid (f : Format) (mode : RoundingMode) (value : Datum) : Datum.Valid f (convert f mode value).value

Every parser result is representable in its destination format, even on invalid input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_valid (f : Format) (mode : RoundingMode) (text : String) : Datum.Valid f (parse f mode text).value

Character conversion always returns a valid destination datum, including on invalid input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_of_decimal (f : Format) (mode : RoundingMode) (text : String) (value : Numerics.DecimalText.Decimal) (hread : Numerics.DecimalText.parseCharacters text.toList = some value) : parse f mode text = projectMagnitude f mode value.negative (↑value.significand * 10 ^ value.exponent) value.exponent

The finite parser performs exactly one destination rounding, using the written quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_zero (f : Format) (mode : RoundingMode) (text : String) (negative : Bool) (quantum : ℤ) (hread : Numerics.DecimalText.parseCharacters text.toList = some { negative := negative, significand := 0, exponent := quantum }) : parse f mode text = { value := Datum.finite negative 0 (max f.minQuantum (min quantum f.maxQuantum)) }

Zero keeps its sign and uses the written quantum clamped to the destination range.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (text : String) (value : Numerics.DecimalText.Decimal) (hread : Numerics.DecimalText.parseCharacters text.toList = some value) (hfinite : (parse f mode text).status.overflow = false) : ∃ (result : ℚ), (parse f mode text).value.toRat? = some result ∧ |result - value.toRat| ≤ 10 ^ roundingQuantum f (↑value.significand * 10 ^ value.exponent) / 2

Nearest decimal parsing has half-grid error unless the destination overflows.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_inexact_iff (f : Format) (mode : RoundingMode) (text : String) (value : Numerics.DecimalText.Decimal) (result : ℚ) (hread : Numerics.DecimalText.parseCharacters text.toList = some value) (hfinite : (parse f mode text).status.overflow = false) (hvalue : (parse f mode text).value.toRat? = some result) : (parse f mode text).status.inexact = true ↔ result ≠ value.toRat

A finite parser result is inexact precisely when its numerical value changed.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.le_parse_towardPositive (f : Format) (text : String) (value : Numerics.DecimalText.Decimal) (hread : Numerics.DecimalText.parseCharacters text.toList = some value) (hfinite : (parse f RoundingMode.towardPositive text).status.overflow = false) : ∃ (result : ℚ), (parse f RoundingMode.towardPositive text).value.toRat? = some result ∧ value.toRat ≤ result

Upward parsing returns an upper bound on the exact decimal input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_towardNegative_le (f : Format) (text : String) (value : Numerics.DecimalText.Decimal) (hread : Numerics.DecimalText.parseCharacters text.toList = some value) (hfinite : (parse f RoundingMode.towardNegative text).status.overflow = false) : ∃ (result : ℚ), (parse f RoundingMode.towardNegative text).value.toRat? = some result ∧ result ≤ value.toRat

Downward parsing returns a lower bound on the exact decimal input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_exact_cohort_closest (f : Format) (mode : RoundingMode) (text : String) (value : Numerics.DecimalText.Decimal) (hread : Numerics.DecimalText.parseCharacters text.toList = some value) (coefficient : ℕ) (quantum : ℤ) (hvalid : Datum.Valid f (Datum.finite value.negative coefficient quantum)) (hexact : ↑value.significand * 10 ^ value.exponent = ↑coefficient * 10 ^ quantum) (d : ℕ) (r : ℤ) (hout : (parse f mode text).value = Datum.finite value.negative d r) (e : ℕ) (t : ℤ) (he : Datum.Valid f (Datum.finite value.negative e t)) (hvalue : ↑coefficient * 10 ^ quantum = ↑e * 10 ^ t) : |value.exponent - r| ≤ |value.exponent - t|

Exact input selects the valid cohort member closest to the written quantum. The written coefficient and quantum need not themselves fit the destination.

theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parse_inexact_quantum_minimal (f : Format) (mode : RoundingMode) (text : String) (value : Numerics.DecimalText.Decimal) (hread : Numerics.DecimalText.parseCharacters text.toList = some value) (hinexact : (parse f mode text).status.inexact = true) (c : ℕ) (q : ℤ) (hout : (parse f mode text).value = Datum.finite value.negative c q) (d : ℕ) (r : ℤ) (hvalid : Datum.Valid f (Datum.finite value.negative d r)) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : q ≤ r

Inexact parsing uses the least quantum in the result's cohort, including directed overflow.