Preservation laws for fixed and scientific decimal notation

Point insertion preserves the positional coefficient. Leading fractional padding does not change that coefficient, and the scanner counts the padding when recovering the decimal scale.

theorem FloatLib.Numerics.DecimalText.parseMagnitude_pointCharacters (whole fraction tail : List Char) (exponent : ℤ) (hwhole : whole ≠ []) (hdigits : ∀ c ∈ whole ++ fraction, ∃ (digit : ℕ), digitValue? c = some digit) (htail : ∀ c ∈ tail.head?, digitValue? c = none) (hexponent : parseExponent tail = some exponent) : RadixText.parseMagnitude (pointCharacters whole fraction ++ tail) 10 digitValue? parseExponent 1 = some ((RadixText.scanDigits (whole ++ fraction) 0 10 digitValue?).1, exponent - ↑fraction.length)

Inserting a point preserves the coefficient and subtracts the fractional digit count. The suffix may be empty or an exponent accepted by the existing decimal scanner.

theorem FloatLib.Numerics.DecimalText.parseMagnitude_fractionalCharacters (coefficient places : ℕ) (tail : List Char) (exponent : ℤ) (htail : ∀ c ∈ tail.head?, digitValue? c = none) (hexponent : parseExponent tail = some exponent) : RadixText.parseMagnitude (fractionalCharacters coefficient places ++ tail) 10 digitValue? parseExponent 1 = some (coefficient, exponent - ↑places)

Fixed fractional digits recover the exact coefficient and the requested decimal scale.

theorem FloatLib.Numerics.DecimalText.parseCharacters_fractionalCharacters (negative : Bool) (coefficient places : ℕ) (tail : List Char) (exponent : ℤ) (htail : ∀ c ∈ tail.head?, digitValue? c = none) (hexponent : parseExponent tail = some exponent) : parseCharacters ((if negative = true then ['-'] else []) ++ (fractionalCharacters coefficient places ++ tail)) = some { negative := negative, significand := coefficient, exponent := exponent - ↑places }

Signed fixed fractional text, optionally followed by an exponent, preserves its coefficient.

@[simp]

theorem FloatLib.Numerics.DecimalText.parseCharacters_fixedCharacters (value : Decimal) : parseCharacters value.fixedCharacters = some value.fixedRepresentation

Fixed notation recovers the coefficient after absorbing any positive exponent.

theorem FloatLib.Numerics.DecimalText.Decimal.fixedRepresentation_eq_self (value : Decimal) (hexponent : value.exponent ≤ 0) : value.fixedRepresentation = value

Fixed notation retains the complete record when its exponent specifies fractional places.

theorem FloatLib.Numerics.DecimalText.parseCharacters_fixedCharacters_of_nonpos (value : Decimal) (hexponent : value.exponent ≤ 0) : parseCharacters value.fixedCharacters = some value

In particular, printing a decimal rounded to exponent -places preserves the exact record.

@[simp]

theorem FloatLib.Numerics.DecimalText.Decimal.fixedRepresentation_toRat (value : Decimal) : value.fixedRepresentation.toRat = value.toRat

Absorbing a positive exponent into the coefficient preserves the exact rational value.

@[simp]

theorem FloatLib.Numerics.DecimalText.Decimal.fixedRepresentation_negative (value : Decimal) : value.fixedRepresentation.negative = value.negative

Fixed presentation preserves the sign, including the sign of zero.

@[simp]

theorem FloatLib.Numerics.DecimalText.parse_formatFixed (value : Decimal) : parse value.formatFixed = some value.toRat

Fixed formatting followed by parsing preserves the exact rational denoted by the input.

@[simp]

theorem FloatLib.Numerics.DecimalText.parseCharacters_scientificCharacters (value : Decimal) : parseCharacters value.scientificCharacters = some value

Scientific notation recovers the entire decimal record, including zero sign and precision.

@[simp]

theorem FloatLib.Numerics.DecimalText.parse_formatScientific (value : Decimal) : parse value.formatScientific = some value.toRat

Scientific formatting followed by parsing preserves the exact rational denoted by the input.