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. 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 falls back to the generic kernel.

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

Every accepted native equal-exponent addition agrees with the finite binary64 path addFiniteComponents?.

Rejected values fall back to addFiniteComponents?, so this theorem is the trust boundary for the native specialization.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.addFinite_eq_addFiniteComponents (x y : Value) : addFinite? x y = addFiniteComponents? x y

Native addFinite? is bit-for-bit equal to the exact finite implementation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.subFinite_eq_addFiniteComponents_negate (x y : Value) : subFinite? x y = addFiniteComponents? x (negate y)

Native subFinite? is bit-for-bit equal to exact finite subtraction.