Correctness of word-specialized square-root dispatch

Binary32 and binary64 have direct 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 include the NaN, infinity, signed-zero, and negative-input cases. The positive finite cases reuse the corresponding kernel refinements. Runtime clients can import SqrtWord.Runtime separately.

Direct binary32 kernel

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

The direct binary32 square root preserves the exact specification.

Direct binary64 kernel

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

The direct binary64 square root preserves the exact specification.

Descriptor-driven backend dispatch

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

The generic square-root dispatcher 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

Native one-word decoding preserves the compact generic square-root implementation.

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

The width-specialized dispatcher preserves the logical format-generic square root.