Fixed-limb difference runtime

Unsigned two-limb comparison, subtraction, leading-bit discovery, and normalization share the same borrow and shift conventions. Keeping those conventions here prevents the dyadic comparison and rounding kernels from growing subtly different copies.

The hot path uses explicit UInt64 limbs without converting through Nat. Their natural-number meanings, and the preconditions under which wrapping subtraction denotes ordinary subtraction, are proved separately in Difference.Proof.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.less (x y : UInt128) : Bool

Compare two two-word unsigned values.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.compare (x y : UInt128) : Ordering

Three-way comparison of two two-word unsigned values.

Exact dyadic certificates use this comparison on widened products without rebuilding them as arbitrary-precision naturals.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.sub (x y : UInt128) : UInt128

Subtract two two-word values with borrow. The result wraps modulo 2^128.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.log2 (value : UInt128) : ℕ

Position of the most significant set bit, with zero mapped to zero.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.shiftRight (value : UInt128) (shift : ℕ) : UInt128

Shift a two-word value right, returning zero at and beyond the 128-bit carrier width.

The explicit ranges avoid the modulo reduction performed by native machine-word shifts.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.singleBit (index : ℕ) : UInt128

A two-word value with exactly one bit set, returning zero beyond the 128-bit carrier.

Constructing the bit directly in its containing limb avoids routing fixed-width significands through an arbitrary-precision power before their final mathematical conversion.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.shiftLeft (value : UInt128) (shift : ℕ) : UInt128

Shift a two-word value left, returning zero at and beyond the 128-bit carrier width.

Bits carried above position 127 are discarded, so the result is value * 2^shift reduced modulo 2^128. shiftLeft_toNat gives the exact product when shift < 128 and no bit is lost, and shiftLeft_of_ge covers the total branch. The explicit ranges avoid the modulo reduction performed by native machine-word shifts.