TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Arithmetic.External.Rounding

Report precision rounding for external binary formats #

The external adapter uses its own declared precision and bias in the report formula. Its precision is always greater than one, so lower-code parity is integer significand parity. The rational selection theorem covers every deterministic mode and every supplied stochastic word. These statements concern precision rounding; saturation and encoding are treated separately.

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

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.precisionOf_gt_one (format : BinaryInterchange.FloatFormat) :
1 < precisionOf format

External binary descriptors always have precision greater than one.

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.codeEven_eq (format : BinaryInterchange.FloatFormat) (quantum : ℤ) (lower : ℕ) :
RationalRounding.codeEven (precisionOf format) (exponentBiasOf format) quantum lower = (lower % 2 == 0)

External code parity is the ordinary parity of the integer significand.

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.quantum_eq (format : BinaryInterchange.FloatFormat) (value : ℚ) :
max (Numerics.RationalBinary.floorLog2 value.num.natAbs value.den) format.minNormalExponent - ↑format.fracWidth = RationalRounding.quantum (precisionOf format) (exponentBiasOf format) value

The selected external quantum uses the declared bias, including custom exponent biases.

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.roundFinite_toRat (format : BinaryInterchange.FloatFormat) (mode : RoundingMode) (value : ℚ) :
(roundFinite format mode value).toRat = RationalRounding.round (precisionOf format) (exponentBiasOf format) mode value

External precision rounding implements the report formula for every mode and rational input.

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.roundFinite_nearestTiesToEven_error (format : BinaryInterchange.FloatFormat) (value : ℚ) :
|(roundFinite format RoundingMode.nearestTiesToEven value).toRat - value| ≤ 2 ^ RationalRounding.quantum (precisionOf format) (exponentBiasOf format) value / 2

External nearest-even precision rounding stays within half its own quantum.

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.roundFinite_error_lt_quantum (format : BinaryInterchange.FloatFormat) (mode : RoundingMode) (value : ℚ) :
|(roundFinite format mode value).toRat - value| < 2 ^ RationalRounding.quantum (precisionOf format) (exponentBiasOf format) value

Every external mode stays within its own quantum, including each stochastic word.

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.roundFinite_towardPositive (format : BinaryInterchange.FloatFormat) (value : ℚ) :
value ≤ (roundFinite format RoundingMode.towardPositive value).toRat ∧ (roundFinite format RoundingMode.towardPositive value).toRat < value + 2 ^ RationalRounding.quantum (precisionOf format) (exponentBiasOf format) value

External upward rounding brackets the input from above before saturation.

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.roundFinite_towardNegative (format : BinaryInterchange.FloatFormat) (value : ℚ) :
(roundFinite format RoundingMode.towardNegative value).toRat ≤ value ∧ value < (roundFinite format RoundingMode.towardNegative value).toRat + 2 ^ RationalRounding.quantum (precisionOf format) (exponentBiasOf format) value

External downward rounding brackets the input from below before saturation.