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 separate WordLimb proof module establishes the cross-carrier projection theorem used by operations with a genuine two-limb intermediate. Importing this scalar proof does not load the complete 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.