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, and 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.