Correctness of word-specialized square-root dispatch

Binary32 and binary64 have their own word kernels. Other descriptors use native one-word decoding when eligible, or the generic square-root kernel. word_eq_spec proves that all these routes agree with Model.Spec.sqrt for every input.

The fixed-format theorems cover the NaN, infinity, signed-zero, and negative-input cases, and the positive finite cases reuse the corresponding kernel refinements.

Direct binary32 kernel

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.sqrt_eq_spec (x : Value) : sqrt x = Spec.sqrt x

Native binary32 square root agrees with Model.Spec.sqrt.

Direct binary64 kernel

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.sqrt_eq_spec (x : Value) : sqrt x = Spec.sqrt x

Native binary64 square root agrees with Model.Spec.sqrt.

Descriptor-driven backend dispatch

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

Generic square root agrees with Spec.sqrt on every input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtBackend.smallWord_eq_generic {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) : smallWord heligible x = generic x

One-word square root with native decoding agrees with generic.

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

The width-specialized dispatcher agrees with Spec.sqrt on every input.