Correctness of the one-word square root for small IEEE formats

sqrtPositiveCore_eq shows that the kernel is Lean's logical unpacked square root, rounded and packed, for every nonzero mantissa and finite scale of an eligible format. sqrtPositive_eq then identifies the dispatcher with the shared finite kernel for every positive finite input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordSqrt.sqrtPositiveCore_eq (fmt : FloatFormat) (heligible : Eligible fmt) (mantissa scale : UInt64) (hm : 0 < mantissa.toNat) (hmBound : mantissa.toNat < 2 ^ (fmt.fracWidth + 1)) (hscale : scale.toNat + 1 ≤ 2 * fmt.bias) : NativeSmallWord.ofWord (sqrtPositiveCore fmt mantissa scale) = ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa.toNat (Int.ofNat scale.toNat - Int.ofNat (fmt.bias + fmt.fracWidth - 1)) hm))

For a nonzero mantissa below 2 ^ (fracWidth + 1) and the scale of a finite value, the kernel is Lean's logical unpacked square root of mantissa * 2 ^ (scale - (bias + fracWidth - 1)).

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordSqrt.sqrtPositive_eq {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x : Model fmt) (hfinite : x.isFinite = true) (hnonzero : x.isZero = false) (hpositive : x.signBit = false) : sqrtPositive heligible x hfinite hnonzero hpositive = NativeSmallWordFinite.sqrtPositive heligible x hfinite hnonzero hpositive

The dispatcher agrees with the shared finite kernel on every positive finite input.