Exact rational meaning of report precision rounding

The executable scale, quotient, and remainder represent the report's scaled magnitude, floor, and fractional part exactly. The resulting formula is uniform in the rounding mode, including each supplied stochastic word. Binary exponent bounds characterize the selected logarithm without approximating it by a real-valued computation.

Reference: P3109 unapproved interim report 4.0.3, revision 34f5964, §4.7.4.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.quotientFloor_lt_precision (precision : ℕ) (minimumNormalExponent : ℤ) (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have leading := Numerics.RationalBinary.floorLog2 numerator denominator; have quantum := max leading minimumNormalExponent - Int.ofNat precision + 1; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (-quantum); scaled.1 / scaled.2 < 2 ^ precision

At the precision quantum, the exact quotient is below 2^precision. Clamping the leading exponent to the minimum normal exponent can only decrease the quotient. The bound depends on these two parameters, not on an encoding or saturation policy.

def FloatLib.Floats.Formats.P3109.RationalRounding.signed (negative : Bool) (magnitude : ℚ) : ℚ

Apply the sign of the input to a nonnegative candidate.

def FloatLib.Floats.Formats.P3109.RationalRounding.scaledMagnitude (value : ℚ) (quantum : ℤ) : ℚ

The report's real-valued significand, which is rational for a rational input.

def FloatLib.Floats.Formats.P3109.RationalRounding.codeEven (precision bias : ℕ) (quantum : ℤ) (lower : ℕ) : Bool

Report parity of the lower code, including its exceptional precision-one rule.

def FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger (mode : RoundingMode) (negative : Bool) (parity : ℕ → Bool) (scaled : ℚ) : ℕ

Report selection between the two adjacent integer significands.

def FloatLib.Floats.Formats.P3109.RationalRounding.roundAt (mode : RoundingMode) (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) : ℚ

Precision rounding at a specified quantum, expressed by mathematical floor and fraction.

def FloatLib.Floats.Formats.P3109.RationalRounding.quantum (precision bias : ℕ) (value : ℚ) : ℤ

The report quantum uses the actual precision and exponent bias.

def FloatLib.Floats.Formats.P3109.RationalRounding.round (precision bias : ℕ) (mode : RoundingMode) (value : ℚ) : ℚ

Mathematical report precision rounding of a finite rational.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.magnitude_eq_ratio (value : ℚ) : |value| = ↑value.num.natAbs / ↑value.den

The absolute numerator and positive denominator represent the magnitude exactly.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.signed_abs (value : ℚ) : signed (decide (value.num < 0)) |value| = value

The stored numerator sign is exactly the sign of the rational input.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.scaleByPowerOfTwo_rat (numerator denominator : ℕ) (exponent : ℤ) : ↑(Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator exponent).1 / ↑(Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator exponent).2 = ↑numerator / ↑denominator * 2 ^ exponent

Moving a binary exponent into an integer quotient preserves its exact rational value.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.scaledMagnitude_eq (value : ℚ) (quantum : ℤ) : scaledMagnitude value quantum = ↑(Numerics.RationalBinary.scaleByPowerOfTwo value.num.natAbs value.den (-quantum)).1 / ↑(Numerics.RationalBinary.scaleByPowerOfTwo value.num.natAbs value.den (-quantum)).2

The executable scaled quotient is the report's scaled magnitude.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.floor_scaledMagnitude (value : ℚ) (quantum : ℤ) : ⌊scaledMagnitude value quantum⌋₊ = (Numerics.RationalBinary.scaleByPowerOfTwo value.num.natAbs value.den (-quantum)).1 / (Numerics.RationalBinary.scaleByPowerOfTwo value.num.natAbs value.den (-quantum)).2

The quotient is exactly the lower adjacent integer in the report.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.fraction_scaledMagnitude (value : ℚ) (quantum : ℤ) : scaledMagnitude value quantum - ↑⌊scaledMagnitude value quantum⌋₊ = ↑((Numerics.RationalBinary.scaleByPowerOfTwo value.num.natAbs value.den (-quantum)).1 % (Numerics.RationalBinary.scaleByPowerOfTwo value.num.natAbs value.den (-quantum)).2) / ↑(Numerics.RationalBinary.scaleByPowerOfTwo value.num.natAbs value.den (-quantum)).2

The remainder ratio is exactly the fractional part, not an approximation to it.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.select_eq_roundedInteger (mode : RoundingMode) (value : ℚ) (quantum : ℤ) (parity : ℕ → Bool) : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo value.num.natAbs value.den (-quantum); have lower := scaled.1 / scaled.2; (if Format.Internal.roundRationalAwayWithParity mode (decide (value.num < 0)) (parity lower) (scaled.1 % scaled.2) scaled.2 = true then lower + 1 else lower) = roundedInteger mode (decide (value.num < 0)) parity (scaledMagnitude value quantum)

All runtime rounding modes select the report's integer candidate at the given quantum.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.normalized_toRat (negative : Bool) (significand : ℕ) (exponent : ℤ) : (if significand = 0 then Numerics.Dyadic.zero else { negative := negative, significand := significand, exponent := exponent }).toRat = signed negative (↑significand * 2 ^ exponent)

Canonicalizing a zero significand does not change the mathematical rounded value.

@[simp]

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_zero (mode : RoundingMode) (quantum : ℤ) (parity : ℕ → Bool) : roundAt mode quantum parity 0 = 0

Zero is preserved by every mode and every supplied random word.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.leadingExponent_bounds (value : ℚ) (hvalue : value ≠ 0) : have leading := Numerics.RationalBinary.floorLog2 value.num.natAbs value.den; 2 ^ leading ≤ |value| ∧ |value| < 2 ^ (leading + 1)

The executable logarithm is characterized by the two consecutive enclosing powers of two.

theorem FloatLib.Floats.Formats.P3109.Format.lowerCodeIsEven_eq (format : Format) (quantum : ℤ) (lower : ℕ) : format.lowerCodeIsEven quantum lower = RationalRounding.codeEven format.precision format.exponentBias quantum lower

Executable code parity agrees with the report, including precision one and the zero code.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_toRat (format : Format) (mode : RoundingMode) (value : ℚ) : (format.roundFiniteRatToPrecision mode value).toRat = RationalRounding.round format.precision format.exponentBias mode value

Every finite rational runtime result is the report's exact precision-rounding formula.