Executable direct posit candidate generation

Direct candidate generation constructs a proposed lower posit code from a normalized exact dyadic. It contains only executable field extraction and packing. The accompanying proof module records the field and range properties reused by the direct guard-and-sticky rounder.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.leadingBit (value : ℕ) : ℕ

Return the index of the leading one bit, or zero for a zero significand, using the native word primitive whenever the significand fits in UInt64.

Wider significands use exact Nat.log2, so the operation remains total at every format width.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.fractionPrefix (significand leading count : ℕ) : ℕ

Take the first count normalized fraction bits after the leading one.

leading is Nat.log2 significand. When more bits are requested than the integer significand stores, the exact dyadic expansion is padded with zeros rather than converted through Rat.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.tailPrefix (exponentField significand leading count : ℕ) : ℕ

Take the first count bits of the standard exponent/fraction tail.

The Posit Standard (2022) fixes the maximum exponent field at two bits. Tapering removes its low bits first, so a short tail keeps the most-significant exponent bits. Any remaining positions are filled by the normalized dyadic fraction.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.lowerCandidateFromFields (format : Format) (regime : ℤ) (exponentField significand leading : ℕ) : ℕ

Pack already normalized regime, exponent, and significand fields into the unsigned lower code.

Separating normalization from layout gives native-word and fixed-limb backends one common packing boundary. The function saturates above maxPos and truncates below minPos.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.lowerCandidate (format : Format) (target : Numerics.Dyadic) : ℕ

Construct the unsigned lower posit candidate directly from a positive exact dyadic.

The function is total. Zero and negative carriers return zero; magnitudes above maxPos produce the all-ones positive payload; magnitudes below minPos produce zero. The public rounder handles the standard's nonzero-underflow-to-minPos rule before consulting this candidate.