Refinement of direct packed-pair posit square root

The packed square-root adapter returns an in-range code and agrees with the shared width-generic root-prefix kernel after decoding.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.sqrtCode_lt_modulus {format : Format} (value : Numerics.FixedWord.UInt128) : sqrtCode value < format.modulus

Every direct packed square-root result is a valid complete posit encoding.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.ofNatBits_sqrtCode_eq_sqrt {format : Format} (heligible : NativeLimb.Eligible format) (value : Numerics.FixedWord.UInt128) (hvalue : value.toNat < format.modulus) : ofNatBits (sqrtCode value) = DirectDyadicArithmetic.sqrt (ofNatBits value.toNat)

Direct packed square root re-encodes to the width-generic root-prefix kernel.