Correctness of wide-limb square root

The integer candidate is certified by square inequalities. For positive normal inputs, its exact root and remainder meet the hypotheses of the shared square-root rounding theorem. All other inputs use the reference operation, including its signed-zero and NaN payload behavior.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.sqrtMantissa_eq_normalMantissa {fmt : FloatFormat} (x : Value fmt) : sqrtMantissa x = (normalMantissa x).toNat

The significand read of sqrtMantissa agrees with the stored normal significand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.sqrtNormal?_refines {fmt : FloatFormat} (h : Eligible fmt) (x result : Value fmt) (hresult : sqrtNormal? fmt x = some result) : toModel result = Spec.sqrt (toModel x)

Every accepted normal candidate has the reference square-root encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_sqrt {fmt : FloatFormat} (h : Eligible fmt) (x : Value fmt) : toModel (sqrt fmt x) = Spec.sqrt (toModel x)

Wide-limb square root agrees with Spec.sqrt on every eligible value, including rounding, special values, signed zeros, and NaN payloads.