Correctness of native-word dyadic comparison

The runtime comparator avoids materializing shifted arbitrary-precision integers when two nonnegative dyadics fit the fixed-word preconditions. This module proves its word comparisons, exponent alignment, and swapped-operand cases equal to the reference Dyadic ordering.

The comparison is format-independent, so binary and posit kernels can share these shift-and-compare theorems.

theorem FloatLib.Numerics.FixedWord.DyadicCompare.compareNonnegativeFields_swap (leftSignificand : ℕ) (leftExponent : ℤ) (rightSignificand : ℕ) (rightExponent : ℤ) : (Dyadic.compareNonnegativeFields leftSignificand leftExponent rightSignificand rightExponent).swap = Dyadic.compareNonnegativeFields rightSignificand rightExponent leftSignificand leftExponent

Reversing the operands of the exact nonnegative dyadic comparator swaps its ordering.

Wide fixed-limb kernels naturally compare their target against a decoded one-word candidate, whereas the generic posit rounder phrases the same question as candidate against target. Keeping the direction bridge beside the shared comparator prevents each format backend from reproving the same order-theoretic fact.

theorem FloatLib.Numerics.FixedWord.DyadicCompare.shiftLeft_toNat (significand : UInt64) (shift : ℕ) (hshift : shift < 64) (hfit : shiftFits significand shift) : (significand <<< UInt64.ofNat shift).toNat = significand.toNat <<< shift

A recognized word shift preserves the corresponding exact natural-number alignment.

Arithmetic backends reuse this theorem after sharing shiftFits with the comparison kernel.

theorem FloatLib.Numerics.FixedWord.DyadicCompare.shiftLeft128_toNat (significand : UInt128) (shift : ℕ) (hshift : shift < 128) (hfit : shiftFits128 significand shift) : (significand.shiftLeft shift).toNat = significand.toNat <<< shift

A recognized two-limb shift preserves the corresponding exact natural-number alignment.

theorem FloatLib.Numerics.FixedWord.DyadicCompare.compareNonnegative_eq (leftSignificand : UInt64) (leftExponent : ℤ) (rightSignificand : UInt64) (rightExponent : ℤ) : compareNonnegative leftSignificand leftExponent rightSignificand rightExponent = Dyadic.compareNonnegativeFields leftSignificand.toNat leftExponent rightSignificand.toNat rightExponent

Native-word comparison returns exactly the same ordering as arbitrary-precision dyadic field comparison.

theorem FloatLib.Numerics.FixedWord.DyadicCompare.compareNonnegative128ToWord_eq (leftSignificand : UInt128) (leftExponent : ℤ) (rightSignificand : UInt64) (rightExponent : ℤ) : compareNonnegative128ToWord leftSignificand leftExponent rightSignificand rightExponent = Dyadic.compareNonnegativeFields leftSignificand.toNat leftExponent rightSignificand.toNat rightExponent

Two-limb-versus-word dyadic comparison is exactly the arbitrary-precision field comparison.

The proof covers all runtime exits: a zero high limb delegates to the established word comparator; a fitting right alignment is represented exactly in two limbs; and each capacity rejection has a strict ordering proof. Consequently the executable wide path introduces no approximation and no additional trust boundary.

theorem FloatLib.Numerics.FixedWord.DyadicCompare.isLessPowerOfTwo_eq (significand : UInt64) (exponent power : ℤ) : isLessPowerOfTwo significand exponent power = Dyadic.isLessNonnegativeFields significand.toNat exponent 1 power

The leading-exponent power-of-two test is exactly the reference arbitrary-precision dyadic comparison.

theorem FloatLib.Numerics.FixedWord.DyadicCompare.isLessNonnegative_eq (leftSignificand : UInt64) (leftExponent : ℤ) (rightSignificand : UInt64) (rightExponent : ℤ) : isLessNonnegative leftSignificand leftExponent rightSignificand rightExponent = Dyadic.isLessNonnegativeFields leftSignificand.toNat leftExponent rightSignificand.toNat rightExponent

Native strict comparison is the reference exact nonnegative comparison.

theorem FloatLib.Numerics.FixedWord.DyadicCompare.isLessOrEqualNonnegative_eq (leftSignificand : UInt64) (leftExponent : ℤ) (rightSignificand : UInt64) (rightExponent : ℤ) : isLessOrEqualNonnegative leftSignificand leftExponent rightSignificand rightExponent = Dyadic.isLessOrEqualNonnegativeFields leftSignificand.toNat leftExponent rightSignificand.toNat rightExponent

Native non-strict comparison is the reference exact nonnegative comparison.