Exact binary character round trips

The string scanner recovers the exact coefficient and exponent. For conventional IEEE descriptors, finite hexadecimal output round-trips in every supported rounding mode; finite decimal output round-trips under nearest-even input. Both results include signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TextParser.run_of_readText (fmt : FloatFormat) (mode : IEEERoundingMode) (text : String) (value : TextValue) (hread : readText text = some value) : run fmt mode text = convertText fmt mode value

Successfully scanned text passes unchanged to the destination conversion.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.readText_decimal_format (value : Numerics.DecimalText.Decimal) : readText value.format = some (TextValue.decimal value)

The shared binary scanner recognizes every exact decimal spelling.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.readText_hex_format (value : Numerics.Dyadic) : readText (Numerics.HexText.format value) = some (TextValue.dyadic value)

The shared binary scanner recognizes every exact hexadecimal spelling.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_formatHex_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) (value : Model fmt) (hfinite : value.isFinite = true) : parse fmt value.formatHex mode = Except.ok value

Hexadecimal text restores a finite IEEE word in every supported rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signedScaledRatToReal_decimal (value : Numerics.DecimalText.Decimal) : have magnitude := ↑value.significand * 10 ^ value.exponent; signedScaledRatToReal value.negative magnitude.num.natAbs magnitude.den 0 = ↑value.toRat

The rational operands used by decimal conversion denote the complete decimal value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.convertDecimalText_eq_of_nonzero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) (hzero : value.toReal ≠ 0) (textValue : Numerics.DecimalText.Decimal) (hexact : ↑textValue.toRat = value.toReal) : (convertDecimalText fmt IEEERoundingMode.nearestEven textValue).value = value

Decimal conversion of an exact finite nonzero value restores its complete IEEE word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_formatDecimal_of_isFinite_of_nonzero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) (hzero : value.toReal ≠ 0) : parse fmt value.formatDecimal = Except.ok value

Exact decimal output restores every nonzero finite IEEE word under nearest-even input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_formatDecimal_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) : parse fmt value.formatDecimal = Except.ok value

Exact decimal output restores every finite IEEE word, including either signed zero.