Downward bounds for directed rational packing #
For a positive exact rational and a descriptor with fmt.isIEEE = true, the executable downward
rounder returns a finite value no greater than the input.
The proof follows the same branch partition as the runtime packer (overflow saturation,
below-minimum underflow, subnormal, and normal), using the equations from Packing.Branches and the
shared grid inequalities from Packing.Grid. The final EReal theorem packages the result in the
order used by the generic directed-rounding semantics.
Positive downward bounds #
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_down_finite_le
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(hfmt : fmt.isIEEE = true)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
:
(roundRatMagnitudeDirectedScaled fmt false false numerator denominator exponent).isFinite = true ∧ (roundRatMagnitudeDirectedScaled fmt false false numerator denominator exponent).toReal ≤ scaledRatToReal numerator denominator exponent
Positive downward rational rounding is finite and never exceeds the exact scaled rational.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_roundRatMagnitudeDirectedScaled_pos_down_eq_false
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(hfmt : fmt.isIEEE = true)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
:
Positive downward rational rounding is never classified as NaN.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_roundRatMagnitudeDirectedScaled_pos_down_le
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(hfmt : fmt.isIEEE = true)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
:
(roundRatMagnitudeDirectedScaled fmt false false numerator denominator exponent).toEReal ≤ ↑(scaledRatToReal numerator denominator exponent)
Positive downward rational rounding is a lower bound in the extended reals.