Correctness of fused multiply-add dispatch

dispatch_eq_spec combines the word and fixed-limb refinements to identify the complete dispatcher with Spec.fma. For finite inputs, this contract rounds the exact product-plus-addend once. Runtime clients can import Fma.Runtime separately.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FmaBackend.dispatch_eq_spec {fmt : FloatFormat} (x y z : Model fmt) : dispatch x y z = Spec.fma x y z

Final structurally selected dispatch preserves fused multiply-add.