Correctness of direct posit field construction

These theorems connect adaptive leading-bit discovery and direct field packing to their exact natural-number specifications. Complete rounding refinement belongs to Direct.Proof; this module contains only reusable facts about the field constructor.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.leadingBit_eq_log2 (value : ℕ) : leadingBit value = value.log2

The adaptive leading-bit primitive is exactly Nat.log2.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.fractionPrefix_lt_two_pow (significand leading count : ℕ) (hlower : 2 ^ leading ≤ significand) (hupper : significand < 2 ^ (leading + 1)) : fractionPrefix significand leading count < 2 ^ count

The normalized fraction prefix fits in exactly the number of requested positions.

The hypotheses characterize leading as the index of the leading one. This formulation is independent of Nat.log2, so packed backends may reuse it after proving their own normalization invariant.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.tailPrefix_lt_two_pow (exponentField significand leading count : ℕ) (hexponent : exponentField < 4) (hlower : 2 ^ leading ≤ significand) (hupper : significand < 2 ^ (leading + 1)) : tailPrefix exponentField significand leading count < 2 ^ count

A valid two-bit exponent followed by a normalized fraction fits in count bits.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.lowerCandidateFromFields_lt_signMask (format : Format) (regime : ℤ) (exponentField significand leading : ℕ) (hexponentField : exponentField < 4) (hleading : 2 ^ leading ≤ significand) (hsignificandUpper : significand < 2 ^ (leading + 1)) : lowerCandidateFromFields format regime exponentField significand leading < format.signMaskNat

A normalized field prefix always encodes a nonnegative finite posit.

This range theorem removes a runtime candidate-bound check from specialized rounders. Its hypotheses are exactly the exponent-width and leading-bit invariants established by normalization.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.lowerCandidate_lt_signMask (format : Format) (target : Numerics.Dyadic) : lowerCandidate format target < format.signMaskNat

The direct dyadic candidate is always a nonnegative finite posit code.