Saturated projection and exponent clamping

At or above 10^(maxQuantum + precision) every magnitude overflows, and the outcome depends only on the rounding direction and sign. Strictly between zero and half the least quantum, every magnitude rounds on the least-quantum grid to the same coefficient, with inexact and underflow. These two facts show that projectScaled computes the same outcome as projecting the unclamped magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_of_overflow (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 10 ^ (f.maxQuantum + ↑f.precision) ≤ x) (preferred : ℤ) : projectMagnitude f mode s x preferred = { value := if mode.overflowToInfinity s = true then Datum.infinity s else f.maxFinite s, status := { overflow := true, inexact := true } }

Every magnitude at or above 10^(maxQuantum + precision) delivers the overflow outcome.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundMagnitude_eq_of_pos_of_lt_half (mode : RoundingMode) (s : Bool) {y : ℚ} (hy0 : 0 < y) (hy : y < 1 / 2) : mode.roundMagnitude s y = mode.roundMagnitude s (1 / 4)

Below one half, each rounding direction rounds a positive rational to the same integer.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_of_tiny (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx0 : 0 < x) (hx : x < 10 ^ f.minQuantum / 2) (preferred : ℤ) : projectMagnitude f mode s x preferred = { value := Datum.finite s (mode.roundMagnitude s (1 / 4)) f.minQuantum, status := { underflow := true, inexact := true } }

Every magnitude strictly between zero and half the least quantum rounds to the least quantum, with the coefficient chosen by the rounding direction alone, and signals inexact and underflow.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectScaled_eq (f : Format) (mode : RoundingMode) (negative : Bool) (coefficient : ℕ) (exponent preferred : ℤ) : projectScaled f mode negative coefficient exponent preferred = projectMagnitude f mode negative (↑coefficient * 10 ^ exponent) preferred

Clamping the exponent never changes a scaled projection.