Mathematical meaning of dyadic rounding decisions

The shift-based implementation of §4.7.4 has the same fractional-part formulas as the rational implementation. In particular the stochastic decisions hold for every supplied word, including words of width zero. No probability or distribution hypothesis is used.

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

theorem FloatLib.Floats.Formats.P3109.Format.Internal.scaleFractionFloor_eq_rational (remainder discarded output : ℕ) : scaleFractionFloor remainder discarded output = scaleRationalFractionFloor remainder (2 ^ discarded) output

Scaling a dyadic fraction by a power of two agrees with exact rational division.

theorem FloatLib.Floats.Formats.P3109.Format.Internal.scaled_fraction_eq (remainder discarded output : ℕ) : ↑remainder / 2 ^ discarded * 2 ^ output = if discarded ≤ output then ↑remainder * 2 ^ (output - discarded) else ↑remainder / 2 ^ (discarded - output)

The same scaling identity before taking a floor or nearest integer.

theorem FloatLib.Floats.Formats.P3109.Format.Internal.scaleFractionNearestEven_eq (remainder discarded output : ℕ) : scaleFractionNearestEven remainder discarded output = RationalRounding.nearestEven (↑remainder / 2 ^ discarded * 2 ^ output)

The shift-based stochastic-C helper computes the report's RNITE exactly.

theorem FloatLib.Floats.Formats.P3109.Format.Internal.roundAway_eq_rational (format : Format) (mode : RoundingMode) (negative : Bool) (quantum : ℤ) (lower remainder discarded : ℕ) (hrange : remainder < 2 ^ discarded) : roundAway format mode negative quantum lower remainder discarded = RationalRounding.roundAway mode negative (format.lowerCodeIsEven quantum lower) (↑remainder / 2 ^ discarded)

Every valid dyadic remainder uses exactly the report's rational rounding decision.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_report_spec (format : Format) (mode : RoundingMode) (value : Numerics.Dyadic) : ∃ (lower : ℕ) (remainder : ℕ) (discarded : ℕ), remainder < 2 ^ discarded ∧ value.toRat = Internal.signRat value.negative * (↑lower + ↑remainder / 2 ^ discarded) * 2 ^ format.quantumExponent value ∧ (format.roundFiniteToPrecision mode value).toRat = Internal.signRat value.negative * ↑(if RationalRounding.roundAway mode value.negative (format.lowerCodeIsEven (format.quantumExponent value) lower) (↑remainder / 2 ^ discarded) = true then lower + 1 else lower) * 2 ^ format.quantumExponent value

For every finite dyadic, precision rounding selects the report's floor or successor using the exact fractional part. The witnesses include its binary denominator, so the fractional part lies in [0, 1). The theorem includes zero inputs and every stochastic word.