Correctness of square-root dispatch

dispatch_eq_spec combines the word and fixed-pair refinements to identify the complete dispatcher with Spec.sqrt, including exceptional inputs. Runtime clients can import Sqrt.Runtime separately.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtBackend.dispatch_eq_spec {fmt : FloatFormat} (x : Model fmt) : dispatch x = Spec.sqrt x

Final structurally selected dispatch preserves square root.