Verified fixed-limb significand products

mul128_toNat proves exact 128 × 128 → 256 multiplication using the mul64_toNat theorem from Core.Proof.UInt128. The addition theorems reconstruct the exact sum from its low limbs and outgoing carry. The UInt256 lemmas describe widening, projection, and leading-bit selection.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_ofUInt128 (value : UInt128) : (ofUInt128 value).toNat = value.toNat

Embedding a two-limb value in four limbs preserves its mathematical value.

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_ofUInt128ShiftedLeft (value : UInt128) (shift : ℕ) (hlower : 64 < shift) (hupper : shift < 128) : (ofUInt128ShiftedLeft value shift).toNat = value.toNat <<< shift

The generic widening shuffle has the expected unbounded value for in-range shifts.

theorem FloatLib.Numerics.FixedWord.UInt256.low128_toNat_of_lt (value : UInt256) (hvalue : value.toNat < 2 ^ 128) : value.low128.toNat = value.toNat

The low-half projection is exact whenever the four-limb value fits in two limbs.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_eq_zero_iff (value : UInt256) : value.toNat = 0 ↔ value = { limb3 := 0, limb2 := 0, limb1 := 0, limb0 := 0 }

A four-limb value has mathematical value zero exactly when every limb is zero.

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_injective : Function.Injective toNat

The natural-number interpretation determines every limb of a four-word value.

theorem FloatLib.Numerics.FixedWord.add64_toNat (x y : UInt64) : have result := add64 x y; result.value.toNat + result.carry.toNat * 2 ^ 64 = x.toNat + y.toNat

Native addition with carry represents the corresponding exact natural-number sum.

theorem FloatLib.Numerics.FixedWord.add64_carry_le_one (x y : UInt64) : (add64 x y).carry.toNat ≤ 1

The carry returned by add64 is always either zero or one.

theorem FloatLib.Numerics.FixedWord.addCarry64_toNat (x y carry : UInt64) : have result := addCarry64 x y carry; result.value.toNat + result.carry.toNat * 2 ^ 64 = x.toNat + y.toNat + carry.toNat

addCarry64 represents exact addition.

theorem FloatLib.Numerics.FixedWord.addCarry64_carry_le_one (x y carry : UInt64) (hcarry : carry.toNat ≤ 1) : (addCarry64 x y carry).carry.toNat ≤ 1

The outgoing carry from addCarry64 is a bit when the incoming carry is a bit.

theorem FloatLib.Numerics.FixedWord.add128_toNat (x y : UInt128) : have result := add128 x y; result.value.toNat + result.carry.toNat * 2 ^ 128 = x.toNat + y.toNat

add128 represents exact addition, including its carry above bit 127.

theorem FloatLib.Numerics.FixedWord.add128_carry_le_one (x y : UInt128) : (add128 x y).carry.toNat ≤ 1

The carry returned by add128 is zero or one.

theorem FloatLib.Numerics.FixedWord.add128_carry_eq_zero_of_lt (x y : UInt128) (hfit : x.toNat + y.toNat < 2 ^ 128) : (add128 x y).carry = 0

A 128-bit addition has no carry when its mathematical sum fits in 128 bits.

theorem FloatLib.Numerics.FixedWord.add128_value_toNat_of_carry_zero (x y : UInt128) (hcarry : (add128 x y).carry = 0) : (add128 x y).value.toNat = x.toNat + y.toNat

The value limbs of add128 contain the exact sum when its carry is zero.

theorem FloatLib.Numerics.FixedWord.add128_value_toNat_of_lt (x y : UInt128) (hfit : x.toNat + y.toNat < 2 ^ 128) : (add128 x y).value.toNat = x.toNat + y.toNat

The low two limbs of add128 contain the ordinary sum whenever that sum fits in 128 bits.

This is the common refinement fact needed by fixed-limb midpoint, significand, and remainder kernels. Keeping it next to add128 avoids backend-local copies of the same carry argument.

theorem FloatLib.Numerics.FixedWord.add256_toNat (x y : UInt256) : have result := add256 x y; result.value.toNat + result.carry.toNat * 2 ^ 256 = x.toNat + y.toNat

add256 represents exact addition, including its carry above bit 255.

theorem FloatLib.Numerics.FixedWord.add256_value_toNat_of_carry_zero (x y : UInt256) (hcarry : (add256 x y).carry = 0) : (add256 x y).value.toNat = x.toNat + y.toNat

The value limbs of add256 contain the exact sum when its carry is zero.

@[simp]

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

Native four-limb leading-bit selection agrees with Nat.log2.

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_lt (value : UInt256) : value.toNat < 2 ^ 256

Every four-word unsigned value lies below the first unrepresentable 256-bit integer.

@[simp]

theorem FloatLib.Numerics.FixedWord.mul128_toNat (x y : UInt128) : (mul128 x y).toNat = x.toNat * y.toNat

mul128 represents the exact mathematical product of its operands.