Correctness of one-word to two-limb Posit adapters

These lemmas are needed only by operations that cross from UInt64 storage to a UInt128 intermediate. They live at that boundary so the ordinary one-word rounding proof remains independent of the complete two-limb proof stack.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordLimb.widen_toNat (significand : UInt64) : (widen significand).toNat = significand.toNat

Zero extension preserves the mathematical significand.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordLimb.roundCodeWordLow_toNat_eq_direct (format : Format) (heligible : NativeWord.Eligible format) (negative : Bool) (significand : Numerics.FixedWord.UInt128) (exponent : ℤ) : (NativeLimbRounding.GuardSticky.roundCodeWord format negative significand exponent).lo.toNat = DirectDyadicPacking.roundCode format { negative := negative, significand := significand.toNat, exponent := exponent }

Project a complete two-limb rounding result into the storage word of an eligible one-word format.

The significand may use both input limbs. Eligibility constrains only the final Posit code, so the result is represented entirely by the low output limb.