Correctness of packed native-word Posit square root

The storage adapter decodes once, scales the exact significand into four fixed words, and runs the checked fixed-word square root, which equals the restoring loop. Its root and remainder are jammed into the common guard/sticky rounder, so the executable word path has the arbitrary-width direct square-root semantics.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSquareRoot.roundFieldsWord_toNat_eq_direct (format : Format) (heligible : NativeWord.Eligible format) (negative : Bool) (significand : UInt64) (exponent : ℤ) : (roundFieldsWord format heligible negative significand exponent).toNat = if { negative := negative, significand := significand.toNat, exponent := exponent }.isLess Numerics.Dyadic.zero = true then format.signMaskNat else DirectDyadicSquareRoot.roundCode format { negative := negative, significand := significand.toNat, exponent := exponent }

Native field rounding equals the common direct square-root domain rule.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSquareRoot.sqrtWordCodeValid_eq {format : Format} (heligible : NativeWord.Eligible format) (value : UInt64) (hvalue : value.toNat < format.modulus) : sqrtWordCodeValid heligible value hvalue = sqrtWordCode heligible value

The packed scalar adapter equals the stored-word square-root kernel.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSquareRoot.sqrtWordCodeValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (value : UInt64) (hvalue : value.toNat < format.modulus) : sqrtWordCodeValid heligible value hvalue < format.modulus

Every packed scalar square root is a complete in-range Posit encoding.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSquareRoot.sqrtWordCodeWordValid_toNat {format : Format} (heligible : NativeWord.Eligible format) (value : UInt64) (hvalue : value.toNat < format.modulus) : (sqrtWordCodeWordValid heligible value hvalue).toNat = sqrtWordCodeValid heligible value hvalue

The word-valued and natural-number views of the complete root code agree.