Verified four-limb rounding

These theorems connect four-limb shifts, sticky-bit normalization, and nearest-even rounding to their natural-number meanings. Multiplication and fused-operation backends can reuse this layer without converting compiled arithmetic to Nat.

theorem FloatLib.Numerics.FixedWord.UInt256.hasNonzeroBelow_eq (value : UInt256) (width : ℕ) : value.hasNonzeroBelow width = (value.toNat % 2 ^ width != 0)

The fixed-limb low-bit predicate is the exact natural-number remainder test at every width.

Widths above the four-limb capacity inspect the complete value, matching reduction modulo any power of two at least 2^256.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat_of_lt64 (value : UInt256) (shift : ℕ) (hpositive : 0 < shift) (hshift : shift < 64) (htopWord : value.limb3 = 0) (htopBits : value.limb2.toNat < 2 ^ shift) : (value.shiftRight128 shift).toNat = value.toNat >>> shift

Four-limb shifting by less than one word is exact when the quotient fits two limbs.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat_of_eq64 (value : UInt256) (htopWord : value.limb3 = 0) : (value.shiftRight128 64).toNat = value.toNat >>> 64

A one-word shift selects the middle two limbs exactly when the top limb is zero.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat (value : UInt256) (shift : ℕ) (hlarge : 64 < shift) (hshift : shift < 128) (htop : value.limb3.toNat < 2 ^ (shift - 64)) : (value.shiftRight128 shift).toNat = value.toNat >>> shift

Four-limb shifting agrees with mathematical right shift when the result fits two limbs.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat_of_eq128 (value : UInt256) : (value.shiftRight128 128).toNat = value.toNat >>> 128

A two-word shift selects the upper two limbs exactly.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat_of_quotient_lt (value : UInt256) (shift : ℕ) (hfit : value.toNat / 2 ^ shift < 2 ^ 128) : (value.shiftRight128 shift).toNat = value.toNat / 2 ^ shift

A four-limb shift is exact whenever its quotient fits in the returned two-limb carrier.

This theorem hides the native word-boundary cases from clients. The fit condition is the only representation-independent precondition needed by normalization and later fixed-limb kernels.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRightJam128_toNat (value : UInt256) (shift : ℕ) (hquotient : (value.shiftRight128 shift).toNat = value.toNat / 2 ^ shift) (hdiscarded : value.hasNonzeroBelow shift = (value.toNat % 2 ^ shift != 0)) : (value.shiftRightJam128 shift).toNat = shiftRightJam value.toNat shift

The fixed-limb jam operation refines the representation-independent operation once its quotient and discarded-bit test have been established.

theorem FloatLib.Numerics.FixedWord.UInt256.normalizationShift128_le (value : UInt256) : value.normalizationShift128 ≤ 128

Four-to-two-limb normalization never discards more than 128 bits.

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_lt_pow_normalizationShift128_add (value : UInt256) : value.toNat < 2 ^ (value.normalizationShift128 + 128)

A four-limb value fits below the normalization window selected from its leading bit.

theorem FloatLib.Numerics.FixedWord.UInt256.normalizationQuotient128_lt (value : UInt256) : value.toNat / 2 ^ value.normalizationShift128 < 2 ^ 128

The quotient selected by four-to-two-limb normalization fits in two limbs.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt256.normalizeJam128_toNat (value : UInt256) : value.normalizeJam128.toNat = shiftRightJam value.toNat value.normalizationShift128

Native four-to-two-limb normalization refines representation-independent shift-with-jam.

The quotient fits in two limbs, and the low bit records the OR of the quotient's low bit and the discarded suffix's sticky bit.

theorem FloatLib.Numerics.FixedWord.UInt256.normalizeJam128_toNat_eq_zero_iff (value : UInt256) : value.normalizeJam128.toNat = 0 ↔ value.toNat = 0

Four-to-two-limb normalization preserves zero exactly.

theorem FloatLib.Numerics.FixedWord.UInt256.roundShiftRightEven128_toNat (value : UInt256) (shift : ℕ) (hlarge : 64 < shift) (hshift : shift < 128) (htop : value.limb3.toNat < 2 ^ (shift - 64)) (hincrementFit : value.toNat >>> shift + 1 < 2 ^ 128) : (value.roundShiftRightEven128 shift).toNat = Numerics.roundShiftRightEven value.toNat shift

Four-limb nearest-even rounding agrees with the generic natural-number rounder.