Rounding-direction theorems for P3109 projection

Format.roundFiniteToPrecision expresses an exact finite dyadic in units of the descriptor quantum 2^Q, with Q = max(floor(log2 |X|), 1 - B) - P + 1, and then chooses between the two integers bracketing the scaled magnitude. This module proves that the deterministic modes make the choice the report prescribes:

• towardZero truncates: the result has the smaller magnitude and lies within one quantum;
• up and down bracket the input from the requested side;
• nearestAway and nearest stay within half a quantum, and on an exact tie select the larger magnitude, respectively the candidate whose P3109 code is even;
• toOdd stays within one quantum, and for P > 1 it returns an odd significand whenever nonzero bits were discarded.

The bounds concern rational denotations before saturation and cover every descriptor width, including P = 1. Projection.Selection and Projection.Rational.Selection prove the stochastic selection formulas for every supplied random word.

def FloatLib.Floats.Formats.P3109.Format.quantumExponent (format : Format) (value : Numerics.Dyadic) : ℤ

Quantum exponent selected by P3109 precision rounding for a nonzero finite dyadic.

This is the Q of Section 4.7.4: the selected precision grid has spacing 2^Q before saturation.

theorem FloatLib.Floats.Formats.P3109.Format.quantum_pos (format : Format) (value : Numerics.Dyadic) : 0 < 2 ^ format.quantumExponent value

The quantum 2^Q as a positive rational.

def FloatLib.Floats.Formats.P3109.Format.Internal.signRat (negative : Bool) : ℚ

Rational sign factor of a dyadic.

theorem FloatLib.Floats.Formats.P3109.Format.Internal.roundFiniteToPrecision_spec (format : Format) (mode : RoundingMode) (value : Numerics.Dyadic) (hzero : value.significand ≠ 0) : ∃ (lower : ℕ) (rem : ℕ) (d : ℕ), rem < 2 ^ d ∧ value.toRat = signRat value.negative * (↑lower + ↑rem / 2 ^ d) * 2 ^ format.quantumExponent value ∧ ((format.roundFiniteToPrecision mode value).significand = if roundAway format mode value.negative (format.quantumExponent value) lower rem d = true then lower + 1 else lower) ∧ (format.roundFiniteToPrecision mode value).toRat = signRat value.negative * ↑(format.roundFiniteToPrecision mode value).significand * 2 ^ format.quantumExponent value

Structural description of one precision-rounding step.

The input equals sign * (lower + rem / 2^d) * 2^Q with rem < 2^d, and the result significand is lower or lower + 1, as roundAway decides.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_exponent (format : Format) (mode : RoundingMode) (value : Numerics.Dyadic) (hresult : (format.roundFiniteToPrecision mode value).significand ≠ 0) : (format.roundFiniteToPrecision mode value).exponent = format.quantumExponent value

Precision rounding keeps the selected quantum exponent whenever the result is nonzero.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_toRat_eq_int_mul (format : Format) (mode : RoundingMode) (value : Numerics.Dyadic) : ∃ (n : ℤ), (format.roundFiniteToPrecision mode value).toRat = ↑n * 2 ^ format.quantumExponent value

The rounded result is an integer multiple of the quantum 2^Q.

Together with the direction theorems below this pins the result down to one of the two grid points bracketing the input.

Directed modes

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_towardZero (format : Format) (value : Numerics.Dyadic) : |(format.roundFiniteToPrecision RoundingMode.towardZero value).toRat| ≤ |value.toRat| ∧ |value.toRat| < |(format.roundFiniteToPrecision RoundingMode.towardZero value).toRat| + 2 ^ format.quantumExponent value

towardZero truncates: the result never exceeds the input in magnitude and is within one quantum of it.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_towardZero_maximal (format : Format) (value : Numerics.Dyadic) (n : ℤ) (hn : |↑n| * 2 ^ format.quantumExponent value ≤ |value.toRat|) : |↑n| * 2 ^ format.quantumExponent value ≤ |(format.roundFiniteToPrecision RoundingMode.towardZero value).toRat|

Every grid point no larger in magnitude than the input is no larger than the truncation.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_up (format : Format) (value : Numerics.Dyadic) : value.toRat ≤ (format.roundFiniteToPrecision RoundingMode.up value).toRat ∧ (format.roundFiniteToPrecision RoundingMode.up value).toRat < value.toRat + 2 ^ format.quantumExponent value

up never rounds down and stays within one quantum above the input.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_down (format : Format) (value : Numerics.Dyadic) : (format.roundFiniteToPrecision RoundingMode.down value).toRat ≤ value.toRat ∧ value.toRat < (format.roundFiniteToPrecision RoundingMode.down value).toRat + 2 ^ format.quantumExponent value

down never rounds up and stays within one quantum below the input.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_up_minimal (format : Format) (value : Numerics.Dyadic) (n : ℤ) (hn : value.toRat ≤ ↑n * 2 ^ format.quantumExponent value) : (format.roundFiniteToPrecision RoundingMode.up value).toRat ≤ ↑n * 2 ^ format.quantumExponent value

Every grid point at or above the input is at or above the up result.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_down_maximal (format : Format) (value : Numerics.Dyadic) (n : ℤ) (hn : ↑n * 2 ^ format.quantumExponent value ≤ value.toRat) : ↑n * 2 ^ format.quantumExponent value ≤ (format.roundFiniteToPrecision RoundingMode.down value).toRat

Every grid point at or below the input is at or below the down result.

Nearest modes

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_nearestAway_abs_sub_le (format : Format) (value : Numerics.Dyadic) : |(format.roundFiniteToPrecision RoundingMode.nearestAway value).toRat - value.toRat| ≤ 2 ^ format.quantumExponent value / 2

nearestAway rounds to within half a quantum of the input.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_nearestAway_tie (format : Format) (value : Numerics.Dyadic) (htie : |(format.roundFiniteToPrecision RoundingMode.nearestAway value).toRat - value.toRat| = 2 ^ format.quantumExponent value / 2) : |value.toRat| < |(format.roundFiniteToPrecision RoundingMode.nearestAway value).toRat|

On an exact tie, nearestAway selects the candidate of larger magnitude.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_nearest_abs_sub_le (format : Format) (value : Numerics.Dyadic) : |(format.roundFiniteToPrecision RoundingMode.nearest value).toRat - value.toRat| ≤ 2 ^ format.quantumExponent value / 2

nearest rounds to within half a quantum of the input.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_nearest_tie (format : Format) (value : Numerics.Dyadic) (htie : |(format.roundFiniteToPrecision RoundingMode.nearest value).toRat - value.toRat| = 2 ^ format.quantumExponent value / 2) : ∃ (lower : ℕ), |value.toRat| = (↑lower + 1 / 2) * 2 ^ format.quantumExponent value ∧ (|(format.roundFiniteToPrecision RoundingMode.nearest value).toRat| = ↑lower * 2 ^ format.quantumExponent value ↔ format.lowerCodeIsEven (format.quantumExponent value) lower = true)

On an exact tie, nearest selects the candidate whose P3109 code is even.

The input is exactly halfway between lower * 2^Q and (lower + 1) * 2^Q in magnitude, and the result has magnitude lower * 2^Q exactly when the lower code is even under the report's CodeIsEven rule (including its P = 1 special case).

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_nearest_tie_even (format : Format) (value : Numerics.Dyadic) (hprecision : 1 < format.precision) (htie : |(format.roundFiniteToPrecision RoundingMode.nearest value).toRat - value.toRat| = 2 ^ format.quantumExponent value / 2) : (format.roundFiniteToPrecision RoundingMode.nearest value).significand % 2 = 0

With more than one significand bit, a nearest tie yields an even significand.

Round to odd

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_toOdd_abs_sub_lt (format : Format) (value : Numerics.Dyadic) : |(format.roundFiniteToPrecision RoundingMode.toOdd value).toRat - value.toRat| < 2 ^ format.quantumExponent value

toOdd stays within one quantum of the input.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_toOdd_odd (format : Format) (value : Numerics.Dyadic) (hprecision : 1 < format.precision) (hinexact : (format.roundFiniteToPrecision RoundingMode.toOdd value).toRat ≠ value.toRat) : (format.roundFiniteToPrecision RoundingMode.toOdd value).significand % 2 = 1

With more than one significand bit, toOdd returns an odd significand whenever rounding was inexact.