Decimal exponent clamping preserves binary conversion

convertDecimalText clamps a decimal exponent outside the format's range before forming the exact rational. Far above the overflow threshold every rational rounds to the same overflow result with the same flags, and far below the least subnormal every positive rational rounds to the same tiny result with the same flags. In both regions every finite value lies on the same side of the rational, so the ternary value is preserved too. This file proves these saturation facts for scaled rationals and concludes convertDecimalText_eq_exact.

Saturated rounding values

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.roundRatScaled_eq_of_high (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) {n₁ d₁ n₂ d₂ : ℕ} {e₁ e₂ : ℤ} (hn₁ : n₁ ≠ 0) (hd₁ : d₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₂ : d₂ ≠ 0) (h₁ : decimalSaturationHigh fmt ≤ Numerics.RationalBinary.floorLog2 n₁ d₁ + e₁) (h₂ : decimalSaturationHigh fmt ≤ Numerics.RationalBinary.floorLog2 n₂ d₂ + e₂) : roundRatScaled fmt mode sign n₁ d₁ e₁ = roundRatScaled fmt mode sign n₂ d₂ e₂

Above decimalSaturationHigh, the rounded value does not depend on the exact rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.roundRatScaled_eq_of_low (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) {n₁ d₁ n₂ d₂ : ℕ} {e₁ e₂ : ℤ} (hn₁ : n₁ ≠ 0) (hd₁ : d₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₂ : d₂ ≠ 0) (h₁ : Numerics.RationalBinary.floorLog2 n₁ d₁ + e₁ ≤ decimalSaturationLow fmt) (h₂ : Numerics.RationalBinary.floorLog2 n₂ d₂ + e₂ ≤ decimalSaturationLow fmt) : roundRatScaled fmt mode sign n₁ d₁ e₁ = roundRatScaled fmt mode sign n₂ d₂ e₂

Below decimalSaturationLow, the rounded value does not depend on the exact rational.

Saturated status classification

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingOverflowsScaled_of_high (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) {n d : ℕ} {e : ℤ} (hn : n ≠ 0) (hd : d ≠ 0) (h : decimalSaturationHigh fmt ≤ Numerics.RationalBinary.floorLog2 n d + e) : rationalRoundingOverflowsScaled fmt mode sign n d e = true

Above decimalSaturationHigh, every rounding direction reports overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingOverflowsScaled_of_low (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) {n d : ℕ} {e : ℤ} (hn : n ≠ 0) (hd : d ≠ 0) (h : Numerics.RationalBinary.floorLog2 n d + e ≤ decimalSaturationLow fmt) : rationalRoundingOverflowsScaled fmt mode sign n d e = false

Below decimalSaturationLow, no rounding direction reports overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalIsTinyAfterRoundingScaled_of_low (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) {n d : ℕ} {e : ℤ} (hn : n ≠ 0) (hd : d ≠ 0) (h : Numerics.RationalBinary.floorLog2 n d + e ≤ decimalSaturationLow fmt) (rounded : Model fmt) : rationalIsTinyAfterRoundingScaled fmt mode sign n d e rounded = true

Below decimalSaturationLow, every result is tiny after rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalEqualsDyadicScaled_finite_of_low (fmt : FloatFormat) (sign : Bool) {n d : ℕ} {e : ℤ} (hn : n ≠ 0) (hd : d ≠ 0) (h : Numerics.RationalBinary.floorLog2 n d + e ≤ decimalSaturationLow fmt) (rounded : Model fmt) (hfinite : rounded.isFinite = true) : rationalEqualsDyadicScaled sign n d e (rounded.finiteDyadic hfinite) = false

Below decimalSaturationLow, a positive rational never equals a finite result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_eq_of_high (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) {n₁ d₁ n₂ d₂ : ℕ} {e₁ e₂ : ℤ} (hn₁ : n₁ ≠ 0) (hd₁ : d₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₂ : d₂ ≠ 0) (h₁ : decimalSaturationHigh fmt ≤ Numerics.RationalBinary.floorLog2 n₁ d₁ + e₁) (h₂ : decimalSaturationHigh fmt ≤ Numerics.RationalBinary.floorLog2 n₂ d₂ + e₂) (r₁ r₂ : Model fmt) : rationalRoundingStatusScaled fmt mode sign n₁ d₁ e₁ r₁ = rationalRoundingStatusScaled fmt mode sign n₂ d₂ e₂ r₂

Above decimalSaturationHigh, the status does not depend on the exact rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_eq_of_low (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) {n₁ d₁ n₂ d₂ : ℕ} {e₁ e₂ : ℤ} (hn₁ : n₁ ≠ 0) (hd₁ : d₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₂ : d₂ ≠ 0) (h₁ : Numerics.RationalBinary.floorLog2 n₁ d₁ + e₁ ≤ decimalSaturationLow fmt) (h₂ : Numerics.RationalBinary.floorLog2 n₂ d₂ + e₂ ≤ decimalSaturationLow fmt) (rounded : Model fmt) : rationalRoundingStatusScaled fmt mode sign n₁ d₁ e₁ rounded = rationalRoundingStatusScaled fmt mode sign n₂ d₂ e₂ rounded

Below decimalSaturationLow, the status does not depend on the exact rational.

Saturated ternary values

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTernaryScaled_eq_of_high (fmt : FloatFormat) (sign : Bool) {n₁ d₁ n₂ d₂ : ℕ} {e₁ e₂ : ℤ} (hn₁ : n₁ ≠ 0) (hd₁ : d₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₂ : d₂ ≠ 0) (h₁ : decimalSaturationHigh fmt ≤ Numerics.RationalBinary.floorLog2 n₁ d₁ + e₁) (h₂ : decimalSaturationHigh fmt ≤ Numerics.RationalBinary.floorLog2 n₂ d₂ + e₂) (rounded : Model fmt) : rationalTernaryScaled sign n₁ d₁ e₁ rounded = rationalTernaryScaled sign n₂ d₂ e₂ rounded

Above decimalSaturationHigh, the ternary value does not depend on the exact rational.

Every finite value lies below 2^(maxNormalExponent + 1) in magnitude, so a finite delivery is on the same side of both rationals. A non-finite delivery compares by the sign alone.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTernaryScaled_eq_of_low (fmt : FloatFormat) (sign : Bool) {n₁ d₁ n₂ d₂ : ℕ} {e₁ e₂ : ℤ} (hn₁ : n₁ ≠ 0) (hd₁ : d₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₂ : d₂ ≠ 0) (h₁ : Numerics.RationalBinary.floorLog2 n₁ d₁ + e₁ ≤ decimalSaturationLow fmt) (h₂ : Numerics.RationalBinary.floorLog2 n₂ d₂ + e₂ ≤ decimalSaturationLow fmt) (rounded : Model fmt) : rationalTernaryScaled sign n₁ d₁ e₁ rounded = rationalTernaryScaled sign n₂ d₂ e₂ rounded

Below decimalSaturationLow, the ternary value does not depend on the exact rational.

Both rationals lie strictly between zero and the least positive subnormal in magnitude, so every finite delivery, zero included, is on the same side of both. A non-finite delivery compares by the sign alone.

Decimal magnitudes

The clamp preserves every outcome

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.convertDecimalTextExact_clampDecimalExponent (fmt : FloatFormat) (mode : IEEERoundingMode) (x : Numerics.DecimalText.Decimal) : convertDecimalTextExact fmt mode (clampDecimalExponent fmt x) = convertDecimalTextExact fmt mode x

Clamping the decimal exponent never changes the value, status, or ternary value of a binary conversion.

Outside the clamp range the exact rational is either above every overflow threshold or below every underflow threshold, and the rounded value, flags, and ternary value depend only on that side.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.convertDecimalText_eq_exact (fmt : FloatFormat) (mode : IEEERoundingMode) (x : Numerics.DecimalText.Decimal) : convertDecimalText fmt mode x = convertDecimalTextExact fmt mode x

The fast decimal conversion agrees with the exact reference conversion on every input.