Refinement of direct packed-pair posit addition

Direct addition of packed posit pairs produces a valid encoding and agrees with the representation-independent two-limb addition kernel.

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

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

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

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