Refinement of two-limb posit rounding

Significands that fit in 128 bits use two-limb guard/sticky rounding; larger significands use the arbitrary-width direct rounder. Both branches agree with the shared exact-dyadic rounding specification. The same refinement also proves that normalizing a four-limb product to a two-limb window with a sticky bit preserves the rounded result.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundPositiveCode_eq_direct (format : Format) (heligible : NativeLimb.Eligible format) (target : Numerics.Dyadic) : roundPositiveCode format heligible target = DirectDyadicPacking.roundPositiveCode format target

Capacity dispatch preserves the shared arbitrary-width direct positive rounder.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundCodeNat_eq_direct (format : Format) (heligible : NativeLimb.Eligible format) (value : Numerics.Dyadic) : roundCodeNat format heligible value = DirectDyadicPacking.roundCode format value

Complete two-limb rounding has the shared arbitrary-width direct semantics.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundPositiveCode_eq_dyadic (format : Format) (heligible : NativeLimb.Eligible format) (target : Numerics.Dyadic) : roundPositiveCode format heligible target = DyadicRounding.roundPositiveCode format target

Two-limb positive rounding is the shared exact-dyadic rounder.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundPositiveCode_lt_signMask (format : Format) (heligible : NativeLimb.Eligible format) (target : Numerics.Dyadic) : roundPositiveCode format heligible target < format.signMaskNat

Positive two-limb rounding always selects a code below the sign bit.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundPositive_eq_dyadic (format : Format) (heligible : NativeLimb.Eligible format) (target : Numerics.Dyadic) : roundPositive format heligible target = DyadicRounding.roundPositive format target

Packed positive rounding returns the exact-dyadic model value.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.roundCodeNat_lt_modulus (format : Format) (heligible : NativeLimb.Eligible format) (value : Numerics.Dyadic) : roundCodeNat format heligible value < format.modulus

Every two-limb rounded result is a valid complete posit encoding.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.ofNatBits_roundCodeNat (format : Format) (heligible : NativeLimb.Eligible format) (value : Numerics.Dyadic) : ofNatBits (roundCodeNat format heligible value) = round format heligible value

Re-encoding the code-only result gives the model-valued two-limb rounder.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.round_eq_dyadic (format : Format) (heligible : NativeLimb.Eligible format) (value : Numerics.Dyadic) : round format heligible value = DyadicRounding.round format value

Two-limb rounding is exactly the shared exact-dyadic rounder.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.round_eq_roundRat (format : Format) (heligible : NativeLimb.Eligible format) (value : Numerics.Dyadic) : round format heligible value = roundRat format value.toRat

Two-limb rounding therefore refines the exact rational Posit Standard semantics.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.roundPositiveCodeWord_toNat (format : Format) (heligible : NativeLimb.Eligible format) (significand : Numerics.FixedWord.UInt128) (exponent : ℤ) : (roundPositiveCodeWord format significand exponent).toNat = roundPositiveCode format heligible { negative := false, significand := significand.toNat, exponent := exponent }

The carrier-returning positive rounder denotes the shared exact positive round code.

This theorem is the boundary used by packed arithmetic: execution retains UInt128, while refinement proofs recover the same natural-number code as the general capacity-dispatched rounder.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.roundPositiveCodeWord_lt_signMask (format : Format) (heligible : NativeLimb.Eligible format) (significand : Numerics.FixedWord.UInt128) (exponent : ℤ) : (roundPositiveCodeWord format significand exponent).toNat < format.signMaskNat

Carrier-returning positive rounding always stays below the Posit sign bit.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.roundCodeWord_toNat (format : Format) (heligible : NativeLimb.Eligible format) (negative : Bool) (significand : Numerics.FixedWord.UInt128) (exponent : ℤ) : (roundCodeWord format negative significand exponent).toNat = roundCodeNat format heligible { negative := negative, significand := significand.toNat, exponent := exponent }

Signed carrier-returning rounding is the general two-limb exact round code.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.roundPositiveCode_normalizeJam128 (format : Format) (heligible : NativeLimb.Eligible format) (significand : Numerics.FixedWord.UInt256) (exponent : ℤ) : DirectDyadicPacking.roundPositiveCode format { negative := false, significand := significand.normalizeJam128.toNat, exponent := exponent + Int.ofNat significand.normalizationShift128 } = DirectDyadicPacking.roundPositiveCode format { negative := false, significand := significand.toNat, exponent := exponent }

Normalizing a four-limb significand into its jammed two-limb leading window preserves direct positive Posit rounding for every two-limb-eligible format.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.roundCodeWord_normalizeJam128_toNat (format : Format) (heligible : NativeLimb.Eligible format) (negative : Bool) (significand : Numerics.FixedWord.UInt256) (exponent : ℤ) : (roundCodeWord format negative significand.normalizeJam128 (exponent + Int.ofNat significand.normalizationShift128)).toNat = roundCodeNat format heligible { negative := negative, significand := significand.toNat, exponent := exponent }

Signed two-limb rounding of a normalized jammed four-limb significand is exactly the shared arbitrary-width result.