Signed bounds for conventional IEEE directed rational rounding

Positive-magnitude rational packing bounds extend to signed rationals by exchanging the magnitude rounders under negation. Directed rounding swaps the lower and upper magnitude rounders for negative values, while executable negation transports the result to the negative half-line.

The main theorems apply to conventional IEEE FloatFormats, retain infinities as valid outward bounds in EReal, and establish that a nonzero denominator never produces NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_neg (fmt : FloatFormat) (roundMagnitudeUp : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : roundRatMagnitudeDirectedScaled fmt roundMagnitudeUp true numerator denominator exponent = (roundRatMagnitudeDirectedScaled fmt roundMagnitudeUp false numerator denominator exponent).neg

Changing only the stored sign negates a directed rational magnitude result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_roundRatDownScaled_le (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : (roundRatDownScaled fmt sign numerator denominator exponent).toEReal ≤ ↑(signedScaledRatToReal sign numerator denominator exponent)

Downward rounding of a signed scaled rational is an extended-real lower bound.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_roundRatUpScaled (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : ↑(signedScaledRatToReal sign numerator denominator exponent) ≤ (roundRatUpScaled fmt sign numerator denominator exponent).toEReal

A signed scaled rational is bounded above by its upward-rounded result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundRatDownScaled_eq_false (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : (roundRatDownScaled fmt sign numerator denominator exponent).isNaN = false

Downward rational rounding with a nonzero denominator never produces NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundRatUpScaled_eq_false (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : (roundRatUpScaled fmt sign numerator denominator exponent).isNaN = false

Upward rational rounding with a nonzero denominator never produces NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_roundRatDown_le (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : (roundRatDown fmt sign numerator denominator).toEReal ≤ ↑(signedScaledRatToReal sign numerator denominator 0)

Downward rounding of an unscaled signed rational is an extended-real lower bound.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_roundRatUp (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : ↑(signedScaledRatToReal sign numerator denominator 0) ≤ (roundRatUp fmt sign numerator denominator).toEReal

An unscaled signed rational is bounded above by its upward-rounded result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundRatDown_eq_false (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : (roundRatDown fmt sign numerator denominator).isNaN = false

Unscaled downward rational rounding with a nonzero denominator never produces NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundRatUp_eq_false (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) : (roundRatUp fmt sign numerator denominator).isNaN = false

Unscaled upward rational rounding with a nonzero denominator never produces NaN.