Signed projection guarantees

The error bounds concern the actual rational value of the returned datum. The bounds assume that the returned overflow flag is false. Directed bounds and midpoint decisions come from the integer-grid rounder.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_overflow_iff (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (preferred : ℤ) : (projectMagnitude f mode s x preferred).status.overflow = true ↔ f.maxQuantum < (roundedPair f mode s x).2

theorem FloatLib.Floats.Formats.DecimalInterchange.project_quantum_le_of_no_overflow (f : Format) (mode : RoundingMode) (x : ℚ) (preferred : ℤ) (negativeZero : Bool) (hfinite : (project f mode x preferred negativeZero).status.overflow = false) : (roundedPair f mode (if x = 0 then negativeZero else decide (x < 0)) |x|).2 ≤ f.maxQuantum

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_error_lt_one (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hq : (roundedPair f mode s x).2 ≤ f.maxQuantum) : ∃ (value : ℚ), (projectMagnitude f mode s x preferred).value.toRat? = some value ∧ |value - if s = true then -x else x| < 10 ^ roundingQuantum f x

theorem FloatLib.Floats.Formats.DecimalInterchange.signed_abs (x : ℚ) (negativeZero : Bool) : (if (if x = 0 then negativeZero else decide (x < 0)) = true then -|x| else |x|) = x

Reconstruct a rational from its magnitude and the sign used by project.

theorem FloatLib.Floats.Formats.DecimalInterchange.project_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : ℚ) (preferred : ℤ) (negativeZero : Bool) (hfinite : (project f mode x preferred negativeZero).status.overflow = false) : ∃ (value : ℚ), (project f mode x preferred negativeZero).value.toRat? = some value ∧ |value - x| ≤ 10 ^ roundingQuantum f |x| / 2

Both nearest modes have at most half a unit of error on the selected decimal grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.project_error_lt_one (f : Format) (mode : RoundingMode) (x : ℚ) (preferred : ℤ) (negativeZero : Bool) (hfinite : (project f mode x preferred negativeZero).status.overflow = false) : ∃ (value : ℚ), (project f mode x preferred negativeZero).value.toRat? = some value ∧ |value - x| < 10 ^ roundingQuantum f |x|

In every rounding direction, a nonoverflowing result is less than one grid unit away.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_inexact_iff (f : Format) (mode : RoundingMode) (s : Bool) (x value : ℚ) (preferred : ℤ) (hq : (roundedPair f mode s x).2 ≤ f.maxQuantum) (hv : (projectMagnitude f mode s x preferred).value.toRat? = some value) : (projectMagnitude f mode s x preferred).status.inexact = true ↔ value ≠ if s = true then -x else x

Without overflow, the inexact flag detects a change in numerical value.

theorem FloatLib.Floats.Formats.DecimalInterchange.project_inexact_iff (f : Format) (mode : RoundingMode) (x value : ℚ) (preferred : ℤ) (negativeZero : Bool) (hfinite : (project f mode x preferred negativeZero).status.overflow = false) (hv : (project f mode x preferred negativeZero).value.toRat? = some value) : (project f mode x preferred negativeZero).status.inexact = true ↔ value ≠ x

Without overflow, inexactness is equivalent to a change in numerical value.

theorem FloatLib.Floats.Formats.DecimalInterchange.project_underflow_iff (f : Format) (mode : RoundingMode) (x : ℚ) (preferred : ℤ) (negativeZero : Bool) (hfinite : (project f mode x preferred negativeZero).status.overflow = false) : (project f mode x preferred negativeZero).status.underflow = true ↔ |x| < f.minNormal ∧ (project f mode x preferred negativeZero).status.inexact = true

Decimal tininess is tested on the exact input, before rounding.