Refinement of direct packed-pair posit fused multiply-add

The packed FMA reads three pair-limb codes, forms the exact product plus addend, and rounds once without first constructing model wrappers. This file proves the generated code is in range and re-encodes to the already verified two-limb model operation.

That two-stage argument keeps packed field extraction and carry arithmetic out of the public Posit specification while retaining the one-rounding FMA guarantee. NaR handling follows the common packed boundary rather than a private fallback.

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

Every direct packed fused result is a valid complete posit encoding.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.ofNatBits_fmaCode_eq_fma {format : Format} (heligible : NativeLimb.Eligible format) (left right addend : Numerics.FixedWord.UInt128) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) (haddend : addend.toNat < format.modulus) : ofNatBits (fmaCode heligible left right addend) = NativeLimbArithmetic.fma heligible (ofNatBits left.toNat) (ofNatBits right.toNat) (ofNatBits addend.toNat)

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