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 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 text parses back to fixedRepresentation, which absorbs a positive exponent.

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

fixedRepresentation is the record itself when the exponent is not positive.

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

Fixed text of a decimal with a nonpositive exponent parses back to the same 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.

theorem FloatLib.Numerics.DecimalText.Decimal.trimTrailingZerosLoop_toRat (fuel : ℕ) (value : Decimal) : (trimTrailingZerosLoop fuel value).toRat = value.toRat

Removing trailing zeros with any amount of fuel preserves the exact rational value.

@[simp]

theorem FloatLib.Numerics.DecimalText.Decimal.trimTrailingZeros_toRat (value : Decimal) : value.trimTrailingZeros.toRat = value.toRat

Removing trailing zeros preserves the exact rational value.

theorem FloatLib.Numerics.DecimalText.Decimal.compactLoop_toRat (fuel : ℕ) (value : Decimal) : (compactLoop fuel value).toRat = value.toRat

Moving trailing zeros into the exponent with any amount of fuel preserves the value.

theorem FloatLib.Numerics.DecimalText.Decimal.compactLoop_negative (fuel : ℕ) (value : Decimal) : (compactLoop fuel value).negative = value.negative

Moving trailing zeros into the exponent with any amount of fuel preserves the sign.

@[simp]

theorem FloatLib.Numerics.DecimalText.Decimal.compact_toRat (value : Decimal) : value.compact.toRat = value.toRat

Moving trailing zeros into the exponent preserves the exact rational value.

@[simp]

theorem FloatLib.Numerics.DecimalText.Decimal.compact_negative (value : Decimal) : value.compact.negative = value.negative

Moving trailing zeros into the exponent preserves the sign, including the sign of zero.

@[simp]

theorem FloatLib.Numerics.DecimalText.parse_formatDyadicCompact (value : Dyadic) : parse (formatDyadicCompact value) = some value.toRat

Compact dyadic text parses back to the dyadic's rational value.