Refinement of direct packed-pair posit multiplication

The packed multiplier forms a four-limb product and normalizes it to two limbs with a sticky bit. Its output is a valid posit code and re-encodes to the model-valued two-limb multiplication. The refinement uses exact dyadic multiplication and the shared rounding specification.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.mulCode_lt_modulus {format : Format} (heligible : NativeLimb.Eligible format) (left right : Numerics.FixedWord.UInt128) : (mulCode heligible left right).toNat < format.modulus

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

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.ofNatBits_mulCode_eq_mul {format : Format} (heligible : NativeLimb.Eligible format) (left right : Numerics.FixedWord.UInt128) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : ofNatBits (mulCode heligible left right).toNat = NativeLimbArithmetic.mul heligible (ofNatBits left.toNat) (ofNatBits right.toNat)

Direct packed multiplication re-encodes to the model-valued two-limb kernel.