Correctness of two-limb posit packing

Direct pair packing decodes to the supplied complete encoding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.PairCode.toModel_packWord {format : Format} (width_le : format.bits ≤ 128) (word : Numerics.FixedWord.UInt128) (hword : word.toNat < format.modulus) : Code.toModel (packWord word hword) = Model.ofNatBits word.toNat

Direct carrier-native packing denotes the word's complete encoding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.PairCode.toModel_pack {format : Format} (width_le : format.bits ≤ 128) (bits : ℕ) (hbits : bits < format.modulus) : Code.toModel (pack width_le bits hbits) = Model.ofNatBits bits

Direct pair packing denotes exactly the supplied complete encoding.