Refinement of direct packed-pair posit subtraction

Packed subtraction preserves the posit encoding range. Its complete result agrees with the two-limb subtraction kernel, including exceptional operands.

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

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

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

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