Two-word addition with equal exponents

The two-word addition kernel handles same-sign normal operands with equal exponents. Their exact fracWidth + 2-bit significand sum is rounded once to nearest-even and packed directly. Unequal exponents, opposite signs, subnormals, exceptional values, and overflow boundaries retain the generic exact finite kernel. Every theorem takes NativePair.Eligible fmt; start with addNormalSameExponent_refines.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.expAllOnes_pred_toNat {fmt : FloatFormat} (h : Eligible fmt) : (expAllOnes fmt - 1).toNat = fmt.expAllOnesNat - 1

The all-ones exponent minus one is a proper native predecessor.

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

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

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

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

The two-word finite addition chain equals the width-generic exact finite kernel.