IEEE remainder contracts

IEEE remainder subtracts the nearest integer multiple of the divisor, with ties going to an even quotient. Reducing an aligned numerator modulo twice the divisor preserves both the remainder and the quotient parity needed to resolve a tie.

The finite kernel has this exact rational semantics. For finite inputs and a nonzero divisor in an IEEE encoding, the resulting dyadic is representable, so its final encoding loses no precision. Separate equations specify the value and status for zero divisors and infinities.

Nearest-even quotient arithmetic

Exact finite remainder

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderDyadic_toRat (dividend divisor : Numerics.Dyadic) (hdivisor : divisor.significand ≠ 0) : (remainderDyadic dividend divisor hdivisor).toRat = if divisor.exponent ≤ dividend.exponent then have shift := (dividend.exponent - divisor.exponent).toNat; have numerator := dividend.significand.shiftLeft shift; have quotient := Numerics.roundQuotientEven numerator divisor.significand; have coefficient := Int.ofNat numerator - Int.ofNat (quotient * divisor.significand); Rat.ofInt (if dividend.negative = true then -coefficient else coefficient) * 2 ^ divisor.exponent else have shift := (divisor.exponent - dividend.exponent).toNat; have denominator := divisor.significand.shiftLeft shift; have quotient := Numerics.roundQuotientEven dividend.significand denominator; have coefficient := Int.ofNat dividend.significand - Int.ofNat (quotient * denominator); Rat.ofInt (if dividend.negative = true then -coefficient else coefficient) * 2 ^ dividend.exponent

The optimized finite remainder kernel has the exact unbounded nearest-even quotient semantics.

When the dividend exponent is larger, modular exponentiation recovers the aligned numerator's quotient parity and remainder without constructing it. In the other direction, a sufficiently large exponent gap guarantees that the nearest quotient is zero, allowing an early return. Both paths agree with the unbounded aligned calculation below.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderDyadic_of_significand_eq_zero (dividend divisor : Numerics.Dyadic) (hzero : dividend.significand = 0) (hdivisor : divisor.significand ≠ 0) : remainderDyadic dividend divisor hdivisor = dividend

Zero has zero IEEE remainder against every nonzero finite divisor.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainder_eq_value {fmt : FloatFormat} (dividend divisor : Model fmt) : dividend.remainder divisor = (dividend.remainderWithStatus divisor).value

remainder is exactly the value component of its status-bearing operation.

Status-bearing exceptional branches

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderWithStatus_of_finite {fmt : FloatFormat} (dividend divisor : Model fmt) (exactDividend exactDivisor : Numerics.Dyadic) (hdividend : dividend.exactValue = ExactValue.finite exactDividend) (hdivisor : divisor.exactValue = ExactValue.finite exactDivisor) (hnonzero : exactDivisor.significand ≠ 0) : dividend.remainderWithStatus divisor = have exact := remainderDyadic exactDividend exactDivisor hnonzero; have value := if (exact.significand == 0) = true then zero fmt exactDividend.negative else roundDyadic fmt exact; { value := value, status := IEEEStatus.clear }

For two finite operands with a nonzero divisor, the runtime encodes the selected dyadic remainder and returns clear status. A zero result uses the dividend's sign, subject to the format's zero policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderWithStatus_of_zero_divisor {fmt : FloatFormat} (dividend divisor : Model fmt) (exactDividend exactDivisor : Numerics.Dyadic) (hdividend : dividend.exactValue = ExactValue.finite exactDividend) (hdivisor : divisor.exactValue = ExactValue.finite exactDivisor) (hzero : exactDivisor.significand = 0) : dividend.remainderWithStatus divisor = { value := invalidResult fmt, status := { invalid := true } }

A finite zero divisor makes IEEE remainder invalid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderWithStatus_of_finite_of_infinity {fmt : FloatFormat} (dividend divisor : Model fmt) (exact : Numerics.Dyadic) (negative : Bool) (hdividend : dividend.exactValue = ExactValue.finite exact) (hdivisor : divisor.exactValue = ExactValue.infinity negative) : dividend.remainderWithStatus divisor = { value := dividend, status := IEEEStatus.clear }

A finite dividend is unchanged when the divisor is infinite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderWithStatus_of_infinity_of_finite {fmt : FloatFormat} (dividend divisor : Model fmt) (dividendNegative : Bool) (exactDivisor : Numerics.Dyadic) (hdividend : dividend.exactValue = ExactValue.infinity dividendNegative) (hdivisor : divisor.exactValue = ExactValue.finite exactDivisor) : dividend.remainderWithStatus divisor = { value := invalidResult fmt, status := { invalid := true } }

An infinite dividend and finite divisor make IEEE remainder invalid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderWithStatus_of_infinity_of_infinity {fmt : FloatFormat} (dividend divisor : Model fmt) (dividendNegative divisorNegative : Bool) (hdividend : dividend.exactValue = ExactValue.infinity dividendNegative) (hdivisor : divisor.exactValue = ExactValue.infinity divisorNegative) : dividend.remainderWithStatus divisor = { value := invalidResult fmt, status := { invalid := true } }

Two infinite operands make IEEE remainder invalid.

Exactness of the encoded remainder

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderDyadic_eq_or_le (dividend divisor : Numerics.Dyadic) (hdivisor : divisor.significand ≠ 0) : remainderDyadic dividend divisor hdivisor = dividend ∨ (remainderDyadic dividend divisor hdivisor).exponent = divisor.exponent ∧ (remainderDyadic dividend divisor hdivisor).significand ≤ divisor.significand ∨ (remainderDyadic dividend divisor hdivisor).exponent = dividend.exponent ∧ (remainderDyadic dividend divisor hdivisor).significand ≤ dividend.significand

The exact remainder is either the dividend itself or a dyadic at the exponent of one operand whose significand is no larger than that operand's. These bounds establish representability in remainderWithStatus_exact.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.remainderWithStatus_exact {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (dividend divisor : Model fmt) (exactDividend exactDivisor : Numerics.Dyadic) (hdividend : dividend.exactValue = ExactValue.finite exactDividend) (hdivisor : divisor.exactValue = ExactValue.finite exactDivisor) (hnonzero : exactDivisor.significand ≠ 0) : (dividend.remainder divisor).isFinite = true ∧ (dividend.remainder divisor).toReal = (remainderDyadic exactDividend exactDivisor hnonzero).toReal

With a nonzero divisor, the remainder of two finite operands is exactly representable in an IEEE encoding. The final rounding preserves the exact dyadic's real value and produces a finite result, justifying the clear status on this branch.