Exponent-operation semantics

The bounds on decimalExponent characterize its answer by consecutive radix powers. Scaling inherits the actual projection's value, range, rounding and cohort guarantees, including signed zero and decimal tininess before rounding.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_finite (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) : scale f mode (Datum.finite s c q) n = projectMagnitude f mode s (↑c * 10 ^ (q + n)) (q + n)

Scaling a finite datum projects the exact product of its magnitude and the radix power.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_valid (f : Format) (mode : RoundingMode) (x : Datum) (n : ℤ) : Datum.Valid f (scale f mode x n).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_exact_magnitude (c : ℕ) (q n : ℤ) : ↑c * 10 ^ (q + n) = ↑c * 10 ^ q * 10 ^ n

The intermediate magnitude is exactly the input magnitude times the radix power.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_exact_status (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) (hvalid : Datum.Valid f (Datum.finite s c (q + n))) : (scale f mode (Datum.finite s c q) n).status = { }

An in-range exact shifted representation incurs no exceptions.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_exact_value (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) (hvalid : Datum.Valid f (Datum.finite s c (q + n))) : (scale f mode (Datum.finite s c q) n).value.toRat? = some (Datum.finiteValue s c q * 10 ^ n)

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_quantum_closest (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) (hvalid : Datum.Valid f (Datum.finite s c (q + n))) (d : ℕ) (r : ℤ) (hout : (scale f mode (Datum.finite s c q) n).value = Datum.finite s d r) (e : ℕ) (t : ℤ) (he : Datum.Valid f (Datum.finite s e t)) (hvalue : ↑c * 10 ^ (q + n) = ↑e * 10 ^ t) : |q + n - r| ≤ |q + n - t|

The selected quantum is closest to q + n among valid representations of the exact result.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_zero (f : Format) (mode : RoundingMode) (s : Bool) (q n : ℤ) : scale f mode (Datum.finite s 0 q) n = { value := Datum.finite s 0 (max f.minQuantum (min (q + n) f.maxQuantum)) }

Scaling zero changes only its quantum, clamped at the format boundaries.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_inexact_iff (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) (v : ℚ) (hq : (roundedPair f mode s (↑c * 10 ^ (q + n))).2 ≤ f.maxQuantum) (hv : (scale f mode (Datum.finite s c q) n).value.toRat? = some v) : (scale f mode (Datum.finite s c q) n).status.inexact = true ↔ v ≠ Datum.finiteValue s c q * 10 ^ n

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scale_underflow_iff (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) (hq : (roundedPair f mode s (↑c * 10 ^ (q + n))).2 ≤ f.maxQuantum) : (scale f mode (Datum.finite s c q) n).status.underflow = true ↔ ↑c * 10 ^ (q + n) < f.minNormal ∧ (scale f mode (Datum.finite s c q) n).status.inexact = true

Scaling uses the exact, unrounded magnitude in the decimal tininess test.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponent_finite (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hc : c ≠ 0) : decimalExponent f (Datum.finite s c q) = { value := q + ↑(Nat.log 10 c) }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponent_bounds (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hc : c ≠ 0) : 10 ^ (decimalExponent f (Datum.finite s c q)).value ≤ ↑c * 10 ^ q ∧ ↑c * 10 ^ q < 10 ^ ((decimalExponent f (Datum.finite s c q)).value + 1)

The returned exponent is exactly the unique radix-power bracket for the magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponent_valid_range (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hc : c ≠ 0) (hvalid : Datum.Valid f (Datum.finite s c q)) : f.minQuantum ≤ (decimalExponent f (Datum.finite s c q)).value ∧ (decimalExponent f (Datum.finite s c q)).value ≤ f.maxQuantum + ↑f.precision - 1

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponentSentinel_twice_bound (f : Format) : 2 * |f.minQuantum| < decimalExponentSentinel f ∧ 2 * |f.maxQuantum + ↑f.precision - 1| < decimalExponentSentinel f

The exceptional integer exceeds twice either absolute endpoint of the exponent range.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponentSentinel_outside_logBBound (f : Format) : 2 * |logBBound f| < decimalExponentSentinel f ∧ -decimalExponentSentinel f < -(2 * |logBBound f|)

Both exceptional integers lie outside the range ±2 × (emax + p - 1), as IEEE 754-2019 §5.3.3 requires for an integer logBFormat.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponent_sentinel_twice_abs (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hc : c ≠ 0) (hvalid : Datum.Valid f (Datum.finite s c q)) : 2 * |(decimalExponent f (Datum.finite s c q)).value| < decimalExponentSentinel f

Every valid finite exponent has absolute value less than half the exceptional sentinel.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponent_sentinel_separated (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hc : c ≠ 0) (hvalid : Datum.Valid f (Datum.finite s c q)) : -decimalExponentSentinel f < (decimalExponent f (Datum.finite s c q)).value ∧ (decimalExponent f (Datum.finite s c q)).value < decimalExponentSentinel f

The integer exceptional result cannot collide with a valid finite nonzero exponent.