Representation-independent Posit guard and sticky bits

These functions inspect the exact exponent-and-fraction tail using natural numbers only. They are the common specification refined by the one-word and two-limb execution carriers; no fixed-width storage implementation is imported here.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.tailBit (exponentField significand leading index : Nat) : Bool

Read one bit of a normalized exponent/fraction tail.

The first two positions are the Posit exponent, most-significant bit first. Later positions walk the significand below its leading one and then return exact zero padding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.tailHasNonzeroAfter (exponentField significand leading consumed : Nat) : Bool

Whether any exact exponent/fraction bit remains after consumed leading tail positions.

Before both exponent bits have been consumed, the suffix consists of the low exponent bits and the explicit fraction. Afterwards it is exactly a low-bit test on the significand.