Correctness of addition and subtraction backends

The dispatcher has several execution paths: generic exact arithmetic, the one-word UInt64 kernel of NativeSmallWordAdd, native small-word decoding into the compiled component kernel, binary32, binary64, and fixed limbs. They all refine the same format-generic Spec.add and Spec.sub.

Accepted specialized results agree with the finite kernel; declined paths use generic. Together, these refinements give word_eq_spec and subWord_eq_spec for every descriptor and operand pair, including exceptional values. Runtime clients can import Add.Runtime separately.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AddBackend.generic_eq_spec {fmt : FloatFormat} (x y : Model fmt) : generic x y = Spec.add x y

Compact generic addition preserves the exact-dyadic specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AddBackend.word_eq_spec {fmt : FloatFormat} (x y : Model fmt) : word x y = Spec.add x y

Native fixed-format and reusable one-word dispatch preserves addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AddBackend.subWord_eq_spec {fmt : FloatFormat} (x y : Model fmt) : subWord x y = Spec.sub x y

Native fixed-format and reusable one-word dispatch preserves subtraction.