Rounded-real semantics

Scaled rational inputs connect to the independent real-number rounding definition roundAt through their exponent and mantissa. The proof removes the sign, identifies the exact exponent and scaled mantissa seen by the generic rounding theory, and proves that nearest-even quotient selection makes the same tie decision.

For descriptors with fmt.isIEEE = true, the remaining lemmas show that an exact magnitude at most the largest finite value produces a finite packed result.

Sign reduction

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

Non-NaN scaled rational rounding restores a negative sign by exact sign-bit negation.

Rounded-real exponent and mantissa

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_signedScaledRatToReal (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : |signedScaledRatToReal sign numerator denominator exponent| = scaledRatToReal numerator denominator exponent

The absolute value of a signed scaled rational is its unsigned magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.magnitude_signedScaledRatToReal (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : Flocq.magnitude Numerics.binaryRadix (signedScaledRatToReal sign numerator denominator exponent) = Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1

The Flocq magnitude of a nonzero scaled rational is one above its leading binary exponent, Numerics.RationalBinary.floorLog2 numerator denominator + exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cexp_signedScaledRatToReal (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : Flocq.cexp Numerics.binaryRadix (fexpOf fmt) (signedScaledRatToReal sign numerator denominator exponent) = fexpOf fmt (Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1)

The rounded-real model and rational implementation choose the same target exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledMantissa_signedScaledRatToReal (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have target := fexpOf fmt (Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1); have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent - target); Flocq.scaledMantissa Numerics.binaryRadix (fexpOf fmt) (signedScaledRatToReal sign numerator denominator exponent) = if sign = true then -(↑scaled.1 / ↑scaled.2) else ↑scaled.1 / ↑scaled.2

The canonical scaled mantissa of a rational is the same quotient after moving the selected binary exponent into its natural numerator or denominator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nearestEven_scaledRat (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have target := fexpOf fmt (Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1); have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent - target); Flocq.nearestEven (Flocq.scaledMantissa Numerics.binaryRadix (fexpOf fmt) (signedScaledRatToReal sign numerator denominator exponent)) = if sign = true then -Int.ofNat (Numerics.roundQuotientEven scaled.1 scaled.2) else Int.ofNat (Numerics.roundQuotientEven scaled.1 scaled.2)

Nearest-even selection of the scaled rational is roundQuotientEven, with its sign restored.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_scaledRat_eq (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have target := fexpOf fmt (Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1); have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent - target); have rounded := Numerics.roundQuotientEven scaled.1 scaled.2; roundAt fmt (signedScaledRatToReal sign numerator denominator exponent) = ↑(if sign = true then -Int.ofNat rounded else Int.ofNat rounded) * bpow target

Rounded-real nearest-even semantics of a nonzero signed scaled rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_roundRatScaled_of_abs_le_posMaxFinite (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) (hbound : |signedScaledRatToReal sign numerator denominator exponent| ≤ (posMaxFinite fmt).toReal) : (roundRatScaled fmt sign numerator denominator exponent).isFinite = true

Nearest-even scaled-rational rounding cannot overflow when the exact magnitude is at most the largest finite value of the destination format.