Deterministic rational precision-rounding guarantees

These results derive direction, error bounds, and tie selection from the proved rational formula. They hold before saturation, whose overflow behavior is deliberately separate. The common quantum-level results apply to both P3109 descriptors and external binary formats.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.fraction_bounds (scaled : ℚ) (hnonneg : 0 ≤ scaled) : 0 ≤ scaled - ↑⌊scaled⌋₊ ∧ scaled - ↑⌊scaled⌋₊ < 1

The report fractional part of a nonnegative scaled magnitude lies in [0, 1).

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_bounds (mode : RoundingMode) (negative : Bool) (parity : ℕ → Bool) (scaled : ℚ) : ⌊scaled⌋₊ ≤ roundedInteger mode negative parity scaled ∧ roundedInteger mode negative parity scaled ≤ ⌊scaled⌋₊ + 1

Every mode selects one of the adjacent integer candidates.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_natCast (mode : RoundingMode) (negative : Bool) (parity : ℕ → Bool) (value : ℕ) : roundedInteger mode negative parity ↑value = value

Exact integers are preserved for every mode, including every stochastic word.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_error_lt_one (mode : RoundingMode) (negative : Bool) (parity : ℕ → Bool) (scaled : ℚ) (hnonneg : 0 ≤ scaled) : |↑(roundedInteger mode negative parity scaled) - scaled| < 1

Every selected integer is less than one unit from the input, even for stochastic modes.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_towardZero (negative : Bool) (parity : ℕ → Bool) (scaled : ℚ) : roundedInteger RoundingMode.towardZero negative parity scaled = ⌊scaled⌋₊

Truncation is the lower integer candidate.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_up (parity : ℕ → Bool) (scaled : ℚ) (hnonneg : 0 ≤ scaled) : scaled ≤ ↑(roundedInteger RoundingMode.towardPositive false parity scaled) ∧ ↑(roundedInteger RoundingMode.towardPositive false parity scaled) < scaled + 1

Rounding up in magnitude brackets a nonnegative input within one integer unit.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_nearestTiesToAway_error (negative : Bool) (parity : ℕ → Bool) (scaled : ℚ) (hnonneg : 0 ≤ scaled) : |↑(roundedInteger RoundingMode.nearestTiesToAway negative parity scaled) - scaled| ≤ 1 / 2

The nearest-away candidate is at most one half-unit from the exact scaled value.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_nearestTiesToEven_error (negative : Bool) (parity : ℕ → Bool) (scaled : ℚ) (hnonneg : 0 ≤ scaled) : |↑(roundedInteger RoundingMode.nearestTiesToEven negative parity scaled) - scaled| ≤ 1 / 2

The nearest-even candidate is at most one half-unit away, for either lower-code parity.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_nearestTiesToAway_tie (negative : Bool) (parity : ℕ → Bool) (scaled : ℚ) (htie : scaled - ↑⌊scaled⌋₊ = 1 / 2) : roundedInteger RoundingMode.nearestTiesToAway negative parity scaled = ⌊scaled⌋₊ + 1

On a halfway input, nearest-away selects the greater magnitude.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_nearestTiesToEven_tie (negative : Bool) (parity : ℕ → Bool) (scaled : ℚ) (htie : scaled - ↑⌊scaled⌋₊ = 1 / 2) : roundedInteger RoundingMode.nearestTiesToEven negative parity scaled = if parity ⌊scaled⌋₊ = true then ⌊scaled⌋₊ else ⌊scaled⌋₊ + 1

On a halfway input, nearest-even selects the lower candidate when parity ⌊scaled⌋₊ is true, and the upper candidate otherwise.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_nearestTiesToEven_tie_even (negative : Bool) (scaled : ℚ) (htie : scaled - ↑⌊scaled⌋₊ = 1 / 2) : roundedInteger RoundingMode.nearestTiesToEven negative (fun (lower : ℕ) => decide (lower % 2 = 0)) scaled % 2 = 0

With significand parity, the selected halfway candidate is an even integer.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_toOdd_odd (negative : Bool) (scaled : ℚ) (hinexact : 0 < scaled - ↑⌊scaled⌋₊) : roundedInteger RoundingMode.toOdd negative (fun (lower : ℕ) => decide (lower % 2 = 0)) scaled % 2 = 1

With significand parity, inexact round-to-odd selects an odd integer.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.scaledMagnitude_nonneg (value : ℚ) (quantum : ℤ) : 0 ≤ scaledMagnitude value quantum

The scaled magnitude is nonnegative at every quantum.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.scaledMagnitude_mul_quantum (value : ℚ) (quantum : ℤ) : scaledMagnitude value quantum * 2 ^ quantum = |value|

Restoring the quantum recovers the exact input magnitude.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.abs_signed (negative : Bool) (value : ℚ) : |signed negative value| = |value|

Applying a sign does not change absolute magnitude.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_error (mode : RoundingMode) (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) : |roundAt mode quantum parity value - value| = |↑(roundedInteger mode (decide (value.num < 0)) parity (scaledMagnitude value quantum)) - scaledMagnitude value quantum| * 2 ^ quantum

Error in the scaled integer is converted to value error by the positive quantum.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_error_lt_quantum (mode : RoundingMode) (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) : |roundAt mode quantum parity value - value| < 2 ^ quantum

Every mode stays within one quantum before saturation, for every supplied stochastic word.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_nearestTiesToAway_error (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) : |roundAt RoundingMode.nearestTiesToAway quantum parity value - value| ≤ 2 ^ quantum / 2

Nearest-away rounding has error at most half the chosen quantum.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_nearestTiesToEven_error (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) : |roundAt RoundingMode.nearestTiesToEven quantum parity value - value| ≤ 2 ^ quantum / 2

Nearest-even rounding has error at most half the chosen quantum, including precision one.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_towardZero (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) : |roundAt RoundingMode.towardZero quantum parity value| ≤ |value| ∧ |value| < |roundAt RoundingMode.towardZero quantum parity value| + 2 ^ quantum

Truncation reduces magnitude by less than one quantum.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_towardPositive (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) : value ≤ roundAt RoundingMode.towardPositive quantum parity value ∧ roundAt RoundingMode.towardPositive quantum parity value < value + 2 ^ quantum

Directed rounding toward positive infinity brackets the input from above.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_towardNegative (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) : roundAt RoundingMode.towardNegative quantum parity value ≤ value ∧ value < roundAt RoundingMode.towardNegative quantum parity value + 2 ^ quantum

Directed rounding toward negative infinity brackets the input from below.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundAt_nearestTiesToEven_tie (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) (htie : scaledMagnitude value quantum - ↑⌊scaledMagnitude value quantum⌋₊ = 1 / 2) : roundAt RoundingMode.nearestTiesToEven quantum parity value = signed (decide (value.num < 0)) (↑(if parity ⌊scaledMagnitude value quantum⌋₊ = true then ⌊scaledMagnitude value quantum⌋₊ else ⌊scaledMagnitude value quantum⌋₊ + 1) * 2 ^ quantum)

The halfway value is resolved by code parity, with the original sign restored.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.codeEven_one (bias : ℕ) (quantum : ℤ) (lower : ℕ) : codeEven 1 bias quantum lower = decide (lower = 0 ∨ (quantum + ↑bias) % 2 = 0)

The report's precision-one parity uses the zero code or the biased exponent.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.codeEven_of_one_lt (precision bias : ℕ) (quantum : ℤ) (lower : ℕ) (hprecision : 1 < precision) : codeEven precision bias quantum lower = decide (lower % 2 = 0)

At greater precision, report parity is ordinary integer significand parity.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_error_lt_quantum (format : Format) (mode : RoundingMode) (value : ℚ) : |(format.roundFiniteRatToPrecision mode value).toRat - value| < 2 ^ RationalRounding.quantum format.precision format.exponentBias value

All rational modes, including each stochastic word, stay within one precision quantum.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_towardPositive (format : Format) (value : ℚ) : value ≤ (format.roundFiniteRatToPrecision RoundingMode.towardPositive value).toRat ∧ (format.roundFiniteRatToPrecision RoundingMode.towardPositive value).toRat < value + 2 ^ RationalRounding.quantum format.precision format.exponentBias value

Rational rounding toward positive infinity lies above the exact input.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_towardNegative (format : Format) (value : ℚ) : (format.roundFiniteRatToPrecision RoundingMode.towardNegative value).toRat ≤ value ∧ value < (format.roundFiniteRatToPrecision RoundingMode.towardNegative value).toRat + 2 ^ RationalRounding.quantum format.precision format.exponentBias value

Rational rounding toward negative infinity lies below the exact input.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_nearestTiesToAway_error (format : Format) (value : ℚ) : |(format.roundFiniteRatToPrecision RoundingMode.nearestTiesToAway value).toRat - value| ≤ 2 ^ RationalRounding.quantum format.precision format.exponentBias value / 2

Rational nearest-away precision rounding satisfies the half-quantum bound.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_nearestTiesToEven_error (format : Format) (value : ℚ) : |(format.roundFiniteRatToPrecision RoundingMode.nearestTiesToEven value).toRat - value| ≤ 2 ^ RationalRounding.quantum format.precision format.exponentBias value / 2

Rational nearest-even precision rounding satisfies the half-quantum bound.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_nearestTiesToEven_tie (format : Format) (value : ℚ) (htie : have q := RationalRounding.quantum format.precision format.exponentBias value; RationalRounding.scaledMagnitude value q - ↑⌊RationalRounding.scaledMagnitude value q⌋₊ = 1 / 2) : have q := RationalRounding.quantum format.precision format.exponentBias value; have lower := ⌊RationalRounding.scaledMagnitude value q⌋₊; (format.roundFiniteRatToPrecision RoundingMode.nearestTiesToEven value).toRat = RationalRounding.signed (decide (value.num < 0)) (↑(if RationalRounding.codeEven format.precision format.exponentBias q lower = true then lower else lower + 1) * 2 ^ q)

Rational halfway selection uses the report's code parity, including precision one.