Verified exact subtraction for nearby binary64 values

By Sterbenz's lemma, the difference of two finite floating-point values with the same sign and magnitudes within a factor of two is representable. The kernel computes the exact significand difference in UInt64 and packs it without entering the arbitrary-precision generic addition kernel. This module proves the positive normal-input core, then handles negative operands by negating and swapping them.

Rejected inputs use the exact generic implementation.

Bit-level bridges for finite binary64 values

Exact finite-difference packing

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.packExactDifference_eq_round (sign : Bool) (difference exponent : UInt64) (hdifference : difference ≠ 0) (hdifferenceFit : difference.toNat < 2 ^ 53) (hexponentPositive : 0 < exponent.toNat) (hexponentFinite : exponent.toNat < 2047) : packExactDifference sign difference exponent = FiniteProductRound.round FloatFormat.binary64 sign difference.toNat (exponent.toNat + 1073)

Exact native difference packing agrees with the generic unsigned-scale rounder.

Sterbenz exactness in the dyadic model

Component-level binary64 subtraction

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.subSterbenz_refines (x y result : Value) (hfast : subSterbenz? x y = some result) : addFiniteComponents? x (negate y) = some result

Every result of subSterbenz? is also the result of the finite binary64 subtraction path addFiniteComponents? x (negate y), which handles the rejected inputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.subSignedSterbenz_refines (x y result : Value) (hfast : subSignedSterbenz? x y = some result) : addFiniteComponents? x (negate y) = some result

Every result of subSignedSterbenz? is also the result of addFiniteComponents? x (negate y).

For negative operands it reuses subSterbenz_refines after negating and swapping both inputs, then uses commutativity of exact finite addition.