Executable word-specialized square-root dispatch

Only executable square-root kernels and their format dispatcher live here. Correctness theorems remain in SqrtWord.Proof, so runtime-only clients do not load the native refinement developments.

Selection is based on proved format and capacity conditions: binary32 and binary64 use their native paths, suitable smaller formats use the shared word kernel, and the general implementation remains available outside those envelopes. These are implementations of one operation contract, not format-specific definitions of square root.

def FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtBackend.generic {fmt : FloatFormat} (x : Model fmt) : Model fmt

Width-generic compiled square root.

The outer dispatcher retains NaN payload, infinity, signed-zero, and negative-input policy. Positive finite nonzero values use the compact decoder and checked model square root. Their classification proof makes the finite decoder total, so this path has no exceptional fallback.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtBackend.smallWord {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) : Model fmt

One-word square root with native finite-field decoding.

The outer cases intentionally match SqrtBackend.generic; only the positive finite decoder is replaced. Eligibility and classification evidence are erased, leaving the native field kernel in compiled code without an impossible fallback.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtBackend.word {fmt : FloatFormat} (x : Model fmt) : Model fmt

Word-specialized compiled implementation of sqrt.

Binary32 uses the checked direct UInt32/UInt64 backend. Binary64 uses the two-limb restoring kernel. Other eligible one-word IEEE formats use native storage decoding before entering the shared square-root kernel. Remaining formats use SqrtBackend.generic. The dispatcher is specialized on the descriptor, as described in Dispatch.Add.Runtime.