Verified equal-exponent binary64 addition

The binary64 addition kernel handles same-sign normal operands with equal exponents entirely in UInt64. Their exact 54-bit significand sum is rounded once to nearest-even and packed directly. Unequal exponents, opposite signs, subnormals, and overflow boundaries are left to the generic finite kernel. Exceptional values are handled by the outer operation dispatcher.

The subtraction dispatcher composes this adder with the signed Sterbenz backend: same-sign nearby operands use exact native subtraction, opposite-sign operands reuse native addition, and every declined case retains the generic kernel.

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

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

Rejected values retain addFiniteImpl?; this theorem is the trust boundary for the native specialization.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.addFiniteFastImpl_eq (x y : Value) : addFiniteFastImpl? x y = addFiniteImpl? x y

The native addition dispatcher is bit-for-bit equal to the exact finite implementation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.subFiniteFastImpl_eq (x y : Value) : subFiniteFastImpl? x y = addFiniteImpl? x (negate y)

The native subtraction dispatcher is bit-for-bit equal to exact finite subtraction.