Verified exact subtraction for nearby binary64 values

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

Every rejected input retains the existing 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) : addFiniteImpl? x (negate y) = some result

Every accepted Sterbenz result is exactly the existing finite binary64 subtraction path.

The theorem is the trust boundary for the specialization: rejected inputs retain addFiniteImpl? x (negate y), while an accepted native result is bit-for-bit identical to it.

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

Every accepted signed Sterbenz result is exactly the existing finite subtraction path.

The negative case reuses the positive theorem after negating and swapping both inputs, then uses commutativity of exact finite addition.