Correctness of direct two-limb guard-and-sticky rounding

candidateCarrierLawful proves that the UInt128 candidate carrier satisfies the shared carrier laws at capacity 128. The shared theorems then give the packing and rounding refinement; the remaining proofs connect the two-limb entry points, which add the zero test, the exact minimum-positive comparison, and exact-width sign restoration, to the arbitrary-width direct rounder.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.candidateCarrierLawful : GuardStickyCarrier.LawfulCandidateCarrier candidateCarrier Numerics.FixedWord.UInt128.toNat 128

Natural-number laws of the two-limb candidate carrier at capacity 128.

Bit and suffix reads are exact at every width. The arithmetic laws hold under the bounds the shared rounder establishes: shifts stay below 128 positions, sums and successors fit two limbs, and masks are narrower than two limbs.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.payloadBits_lt_of_eligible (format : Format) (heligible : NativeLimb.Eligible format) : format.payloadBits < 128

Under two-limb eligibility the payload is shorter than the carrier.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.isLessMinPositive_eq (format : Format) (significand : Numerics.FixedWord.UInt128) (exponent : ℤ) : isLessMinPositive format significand exponent = { negative := false, significand := significand.toNat, exponent := exponent }.isLess (DyadicRounding.minPositive format)

The fixed-pair minimum-positive comparison is the exact dyadic comparison.

Complete carrier refinement

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

The positive two-limb kernel is the shared arbitrary-width direct rounder.

Keeping this theorem beside the kernel avoids routing the Word/Limb interoperability proof through the complete capacity-dispatch implementation.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbRounding.GuardSticky.restoreSignWord_toNat (format : Format) (heligible : NativeLimb.Eligible format) (negative : Bool) (positiveCode : Numerics.FixedWord.UInt128) (hpositive : positiveCode.toNat < format.signMaskNat) : (restoreSignWord format negative positiveCode).toNat = DyadicRounding.restoreSignCode format negative positiveCode.toNat

Two-limb sign restoration is exact-width Posit sign restoration.

The positive code must lie below the sign mask; zero is unchanged under either sign.

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

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