Right shift with sticky-bit jamming

shiftRightJam is the representation-independent contract used by fixed words, dynamic limbs, and format-specific rounding kernels. It returns the exact quotient when no discarded bit is set; otherwise it records the discarded nonzero suffix in the quotient's low bit.

Keeping the operation in Numerics prevents a generic rounding argument from depending on one particular fixed-word backend.

@[inline]

def FloatLib.Numerics.shiftRightJam (value shift : ℕ) : ℕ

Shift right and preserve whether any discarded bit was nonzero in the result's low bit.

Exact shifts are unchanged. Inexact shifts return an odd result. This is the proof-facing definition: it materializes 2^shift to form the quotient and remainder, so fixed-word backends execute the limb kernels in FloatLib.Kernels (such as UInt256.shiftRightJam128) and use this definition only as their specification.

theorem FloatLib.Numerics.shiftRightJam_eq_of_mod_eq_zero (value shift : ℕ) (hexact : value % 2 ^ shift = 0) : shiftRightJam value shift = value / 2 ^ shift

Exact right shifts are unchanged by jamming.

theorem FloatLib.Numerics.shiftRightJam_mod_two_eq_one (value shift : ℕ) (hinexact : value % 2 ^ shift ≠ 0) : shiftRightJam value shift % 2 = 1

An inexact right shift with jamming always returns an odd result.

theorem FloatLib.Numerics.shiftRightJam_div_pow (value shift extra : ℕ) (hextra : 0 < extra) : shiftRightJam value shift / 2 ^ extra = value / 2 ^ (shift + extra)

Every bit above the jammed low bit is the corresponding bit of the exact shifted value.

Truncating by at least one more bit therefore gives the same result as a single unjammed shift by the sum of the two shift counts.

theorem FloatLib.Numerics.shiftRightJam_testBit (value shift index : ℕ) (hindex : 0 < index) : (shiftRightJam value shift).testBit index = value.testBit (shift + index)

Every positive-index bit of a jammed quotient is the corresponding original bit.

theorem FloatLib.Numerics.shiftRightJam_mod_pow_ne_zero_iff (value shift extra : ℕ) (hextra : 0 < extra) : shiftRightJam value shift % 2 ^ extra ≠ 0 ↔ value % 2 ^ (shift + extra) ≠ 0

A positive-width suffix is nonzero after jamming exactly when the corresponding original suffix was nonzero. This preserves sticky-bit information when shifts are composed.