Correctness of direct one-word guard-and-sticky Posit rounding

candidateCarrierLawful proves that the UInt64 candidate carrier satisfies the shared carrier laws at capacity 64. The shared theorems then establish the packing and rounding refinement. The remaining proofs connect the one-word entry points, which add the zero test, the exact minimum-positive comparison, and sign restoration, to the arbitrary-width direct rounder. The one-word kernel and the two-limb kernel are therefore execution refinements of one rounding rule, selected only by exact intermediate capacity.

The WordLimb proof module proves the cross-carrier projection theorem for operations with a two-limb intermediate. Importing this scalar proof does not load the two-limb rounding proof.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.candidateCarrierLawful : GuardStickyCarrier.LawfulCandidateCarrier candidateCarrier UInt64.toNat 64

Natural-number laws of the one-word candidate carrier at capacity 64.

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

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.payloadBits_lt_of_eligible (format : Format) (heligible : NativeWord.Eligible format) : format.payloadBits < 64

Under one-word eligibility the payload is shorter than the carrier.

Positive rounding

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundPositiveCodeWord_toNat_eq_direct (format : Format) (heligible : NativeWord.Eligible format) (significand : UInt64) (exponent : ℤ) : (roundPositiveCodeWord format heligible significand exponent).toNat = DirectDyadicPacking.roundPositiveCode format { negative := false, significand := significand.toNat, exponent := exponent }

The positive one-word kernel is the shared arbitrary-width direct rounder.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundPositiveCode_eq_direct (format : Format) (heligible : NativeWord.Eligible format) (significand : UInt64) (exponent : ℤ) : roundPositiveCode format heligible significand exponent = DirectDyadicPacking.roundPositiveCode format { negative := false, significand := significand.toNat, exponent := exponent }

Natural-number positive rounding has the same direct semantics.

Signed rounding

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundCodeWord_toNat_eq_direct (format : Format) (heligible : NativeWord.Eligible format) (negative : Bool) (significand : UInt64) (exponent : ℤ) : (roundCodeWord format heligible negative significand exponent).toNat = DirectDyadicPacking.roundCode format { negative := negative, significand := significand.toNat, exponent := exponent }

The signed one-word kernel is the shared arbitrary-width direct rounder.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundCodeNat_eq_direct (format : Format) (heligible : NativeWord.Eligible format) (negative : Bool) (significand : UInt64) (exponent : ℤ) : roundCodeNat format heligible negative significand exponent = DirectDyadicPacking.roundCode format { negative := negative, significand := significand.toNat, exponent := exponent }

Complete natural-number native-field rounding has the shared direct semantics.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordRounding.GuardSticky.roundCodeNat_lt_modulus (format : Format) (heligible : NativeWord.Eligible format) (negative : Bool) (significand : UInt64) (exponent : ℤ) : roundCodeNat format heligible negative significand exponent < format.modulus

Direct one-word field rounding always returns a valid complete Posit code.