Directed projection bounds

In the absence of overflow, the returned datum bounds the exact input on the side prescribed by the rounding direction. Rounding toward zero cannot increase its magnitude. The bounds include subnormal results and either sign of an exact zero.

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

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

theorem FloatLib.Floats.Formats.DecimalInterchange.le_project_towardPositive (f : Format) (x : ℚ) (preferred : ℤ) (negativeZero : Bool) (hfinite : (project f RoundingMode.towardPositive x preferred negativeZero).status.overflow = false) : ∃ (value : ℚ), (project f RoundingMode.towardPositive x preferred negativeZero).value.toRat? = some value ∧ x ≤ value

An upward-rounded finite datum is an upper bound on the exact rational input.

theorem FloatLib.Floats.Formats.DecimalInterchange.project_towardNegative_le (f : Format) (x : ℚ) (preferred : ℤ) (negativeZero : Bool) (hfinite : (project f RoundingMode.towardNegative x preferred negativeZero).status.overflow = false) : ∃ (value : ℚ), (project f RoundingMode.towardNegative x preferred negativeZero).value.toRat? = some value ∧ value ≤ x

A downward-rounded finite datum is a lower bound on the exact rational input.

theorem FloatLib.Floats.Formats.DecimalInterchange.abs_project_towardZero_le (f : Format) (x : ℚ) (preferred : ℤ) (negativeZero : Bool) (hfinite : (project f RoundingMode.towardZero x preferred negativeZero).status.overflow = false) : ∃ (value : ℚ), (project f RoundingMode.towardZero x preferred negativeZero).value.toRat? = some value ∧ |value| ≤ |x|

Rounding toward zero cannot increase a finite result's magnitude.