Packed native-word Posit square root

The packed square-root adapter connects native posit storage to the width-generic direct kernel. A proved-valid UInt64 encoding is decoded once into native dyadic fields. A fixed-word restoring root computes the complete destination-width prefix and the common two-limb guard/sticky packer selects the Posit code. The significand, root, and remainder stay in fixed-width carriers.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSquareRoot.scaledRadicandWord (significand : UInt64) (shift : ℕ) : Numerics.FixedWord.UInt256

Scale one native significand for destination-width square-root prefix generation.

For an eligible one-word Posit, payloadBits ≤ 63; exponent parity therefore makes shift < 128. The exact product fits below bit 192 and is consumed by the 96-digit restoring kernel.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSquareRoot.roundFieldsWord (format : Format) (_heligible : NativeWord.Eligible format) (negative : Bool) (significand : UInt64) (exponent : ℤ) : UInt64

Round decoded native fields through the exact fixed-word root prefix.

@[inline]

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

Complete square-root code retained in the native storage carrier.

@[inline]

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

Natural-number view of the complete native square-root code.