Verified native-word rounding

The one-word nearest-even shift and quotient kernels agree with the shared arbitrary-precision definitions. The compiler substitutions therefore change only the representation used for bounded inputs, not the numerical result.

@[simp]

theorem FloatLib.Numerics.FixedWord.finiteScale_toNat (exponent : UInt64) : (finiteScale exponent).toNat = if exponent = 0 then 0 else exponent.toNat - 1

Natural-number view of the shared nonnegative finite-scale encoding.

@[simp]

theorem FloatLib.Numerics.FixedWord.roundShiftRightEven_toNat (value : UInt64) (shift : ℕ) : (roundShiftRightEven value shift).toNat = Numerics.roundShiftRightEven value.toNat shift

Native word rounding agrees exactly with the generic natural-number rounder.

theorem FloatLib.Numerics.FixedWord.roundShiftRightEvenNat_eq_roundShiftRightEven (value shift : ℕ) : roundShiftRightEvenNat value shift = Numerics.roundShiftRightEven value shift

Capacity-selected nearest-even shifting agrees with arbitrary-precision rounding.

@[csimp]

theorem FloatLib.Numerics.FixedWord.roundShiftRightEven_eq_roundShiftRightEvenNat : Numerics.roundShiftRightEven = roundShiftRightEvenNat

The compiler uses native nearest-even shifting for one-word inputs and the arbitrary-precision definition otherwise.

theorem FloatLib.Numerics.FixedWord.roundQuotientEven_toNat (num den : UInt64) (hden : den ≠ 0) (hquotientFit : num.toNat / den.toNat + 1 < 2 ^ 64) : (roundQuotientEven num den).toNat = Numerics.roundQuotientEven num.toNat den.toNat

Native quotient rounding agrees with natural-number quotient rounding whenever the denominator is nonzero and the incremented quotient fits in one word.

No bound on den is needed: the kernel compares the remainder with den - remainder instead of doubling it, so its intermediates never wrap.

theorem FloatLib.Numerics.FixedWord.roundQuotientEvenNat_eq_roundQuotientEven (num den : ℕ) : roundQuotientEvenNat num den = Numerics.roundQuotientEven num den

The native and arbitrary-precision branches compute the same nearest-even natural-number quotient.

@[csimp]

theorem FloatLib.Numerics.FixedWord.roundQuotientEven_eq_roundQuotientEvenNat : Numerics.roundQuotientEven = roundQuotientEvenNat

The compiler uses native quotient rounding for bounded inputs and the arbitrary-precision definition otherwise.