Verified two-word values and exact wide multiplication

The natural-number meaning of UInt128 is injective, and the native 64 × 64 → 128 multiplication kernel computes the exact product through two 64-bit output limbs. These facts are independent of any floating-point family, so multiplication, division, and square-root backends can share the same native/arbitrary-precision boundary.

Later proofs reason about the mathematical value of the pair instead of reopening carry code at every use site.

theorem FloatLib.Numerics.FixedWord.UInt128.toNat_lt (value : UInt128) : value.toNat < 2 ^ 128

Every two-word unsigned value lies below the first unrepresentable 128-bit integer.

theorem FloatLib.Numerics.FixedWord.UInt128.lo_toNat_eq_toNat_of_lt_two_pow (value : UInt128) (hvalue : value.toNat < 2 ^ 64) : value.lo.toNat = value.toNat

Below the one-word boundary, a two-limb value is represented entirely by its low limb.

theorem FloatLib.Numerics.FixedWord.UInt128.toNat_ofNat (value : ℕ) (hvalue : value < 2 ^ 128) : (ofNat value).toNat = value

Two-limb splitting is exact for values below 2^128.

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

The two native limbs are uniquely determined by their mathematical value.

@[simp]

theorem FloatLib.Numerics.FixedWord.low32_toNat (value : UInt64) : (low32 value).toNat = value.toNat % 2 ^ 32

The low 32-bit half of a word represents its residue modulo 2^32.

@[simp]

theorem FloatLib.Numerics.FixedWord.high32_toNat (value : UInt64) : (high32 value).toNat = value.toNat / 2 ^ 32

The high 32-bit half of a word represents its quotient by 2^32.

theorem FloatLib.Numerics.FixedWord.split32_toNat (value : UInt64) : value.toNat = (low32 value).toNat + 2 ^ 32 * (high32 value).toNat

Recombining the low and high 32-bit halves recovers the original word value.

theorem FloatLib.Numerics.FixedWord.uint64_toNat_eq_zero (value : UInt64) : value.toNat = 0 ↔ value = 0

A native word is zero exactly when its natural-number view is zero.

theorem FloatLib.Numerics.FixedWord.UInt128.toNat_ne_zero_iff (value : UInt128) : value.toNat ≠ 0 ↔ value.lo ≠ 0 ∨ value.hi ≠ 0

A two-limb value is nonzero exactly when at least one native limb is nonzero.

@[simp]

theorem FloatLib.Numerics.FixedWord.mul64_toNat (x y : UInt64) : (mul64 x y).toNat = x.toNat * y.toNat

mul64 represents the exact mathematical product of its operands.

theorem FloatLib.Numerics.FixedWord.mul64_lo_toNat_of_hi_eq_zero (left right : UInt64) (hhigh : (mul64 left right).hi = 0) : (mul64 left right).lo.toNat = left.toNat * right.toNat

A zero high product limb certifies that the low limb is the complete exact product.