Two-word subtraction with equal exponents

The two-word subtraction kernel handles same-sign normal operands with equal exponents. Their significand difference is exact, so the backend only subtracts, normalizes, adjusts the exponent, and packs. Cancellation into the subnormal range and every unsupported case retain the generic exact finite kernel. Start with subNormalSameExponent_refines.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.subNormalSameExponent_refines {fmt : FloatFormat} (h : Eligible fmt) (x y result : Model fmt) (hfast : subNormalSameExponent? x y = some result) : FiniteKernel.add? x y.neg = some result

Every accepted native equal-exponent subtraction is exactly the existing finite path.

Rejected values retain FiniteKernel.add? x (neg y); this theorem is the trust boundary for the native specialization.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.subFinite_eq {fmt : FloatFormat} (h : Eligible fmt) (x y : Model fmt) : subFinite? x y = FiniteKernel.add? x y.neg

The two-word finite subtraction chain equals exact addition with a negated right operand.