Correctness of native-word addition for generic binary32

The UInt64 addition kernel equals its exact-dyadic finite specification. For exponent gaps at most 39, alignment and signed addition are exact in one word. For larger gaps the smaller operand cannot change the nearest-even rounding of the larger one, even at a binade boundary.

Runtime clients can import Addition.Runtime without the alignment, packing and rounding proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.addFiniteWord_eq (x y : Value) : addFiniteWord? x y = addFinite? x y

Word-level finite addition equals the exact-dyadic addFinite?.

Non-finite operands give none on both sides, and zero operands take the exact-dyadic kernel. Nonzero operands split on whether the exponent gap is at most 39.