One-word to two-limb Posit storage adapters

The one-word kernels occasionally continue an exact intermediate in the common UInt128 implementation. This module owns that representation boundary: format eligibility is widened from the storage word to the two-limb carrier, and a UInt64 significand is zero-extended without changing its mathematical value.

Keeping these adapters outside either rounding implementation prevents the scalar rounder from importing the two-limb arithmetic stack. The decision to cross this boundary remains local to the operation whose intermediate no longer fits one word.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordLimb.limbEligible (format : Format) (heligible : NativeWord.Eligible format) : NativeLimb.Eligible format

One-word format eligibility implies eligibility for the common two-limb carrier.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.NativeWordLimb.widen (significand : UInt64) : Numerics.FixedWord.UInt128

Zero-extend a native significand into the common two-limb carrier.