Verified fixed-limb differences

These helpers compare, subtract, normalize, and shift two-word unsigned values without converting the executable path to Nat. Their theorems expose the corresponding mathematical values for format-specific subtraction proofs.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt128.less_eq_true_iff (x y : UInt128) : x.less y = true ↔ x.toNat < y.toNat

Native two-word comparison agrees with comparison of mathematical values.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt128.compare_eq_toNat_compare_toNat (x y : UInt128) : x.compare y = Ord.compare x.toNat y.toNat

Native three-way comparison agrees with comparison of mathematical values.

theorem FloatLib.Numerics.FixedWord.UInt128.sub_toNat (x y : UInt128) (hordered : y.toNat ≤ x.toNat) : (x.sub y).toNat = x.toNat - y.toNat

Ordered two-word subtraction agrees with natural-number subtraction.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt128.log2_toNat (value : UInt128) : value.log2 = value.toNat.log2

Native two-word leading-bit selection agrees with Nat.log2.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt128.shiftRight_toNat (value : UInt128) (shift : ℕ) : (value.shiftRight shift).toNat = value.toNat / 2 ^ shift

The total native two-word right shift is exact division by a power of two.

theorem FloatLib.Numerics.FixedWord.UInt128.singleBit_toNat_of_lt (index : ℕ) (hindex : index < 128) : (singleBit index).toNat = 2 ^ index

A bounded native one-hot value represents the corresponding power of two.

theorem FloatLib.Numerics.FixedWord.UInt128.shiftLeft_toNat (value : UInt128) (shift : ℕ) (hshift : shift < 128) (hfit : value.toNat <<< shift < 2 ^ 128) : (value.shiftLeft shift).toNat = value.toNat <<< shift

A bounded native two-word left shift has its exact mathematical value.

theorem FloatLib.Numerics.FixedWord.UInt128.shiftLeft_of_ge (value : UInt128) (shift : ℕ) (hshift : 128 ≤ shift) : value.shiftLeft shift = { hi := 0, lo := 0 }

Shifting a two-word value left by at least the carrier width returns zero.