Format-independent significant-digit representation laws

Decimal carry preserves the exact rational value at every positive requested precision. Significant-digit conversion preserves the input sign and the numerical result of the caller's magnitude rounding on the selected decimal grid.

@[simp]

theorem FloatLib.Numerics.DecimalText.carryDecimal_toRat (digits : ℕ+) (value : Decimal) : (carryDecimal digits value).toRat = value.toRat

Carrying into a new decade changes the coefficient and quantum, but not the value.

@[simp]

theorem FloatLib.Numerics.DecimalText.significantDecimal_negative (roundMagnitude : Bool → ℚ → ℕ) (value : Decimal) (digits : ℕ+) : (significantDecimal roundMagnitude value digits).negative = value.negative

The sign does not depend on the chosen precision or magnitude rounder.

theorem FloatLib.Numerics.DecimalText.significantDecimal_value (roundMagnitude : Bool → ℚ → ℕ) (value : Decimal) (digits : ℕ+) : (significantDecimal roundMagnitude value digits).toRat = (if value.negative = true then -1 else 1) * ↑(roundMagnitude value.negative (↑value.significand * 10 ^ value.exponent / 10 ^ significantQuantum value.significand value.exponent digits)) * 10 ^ significantQuantum value.significand value.exponent digits

A carry preserves the numerical result of the caller's grid rounding.