Correctness of exact-dyadic posit rounding

The executable posit rounder searches codes using exact dyadic comparisons, chooses between neighbors with ties-to-even, restores the sign, and packs the final model value. This module proves that the complete pipeline is equal to the simple rational specification in Rounding.Proof.

Using dyadics avoids constructing large rational numerators in the runtime, but it does not change the rounding rule. The lemmas here are the common semantic boundary for arbitrary-precision, native-word, and fixed-limb posit backends, so specialized kernels need only prove that their local comparisons agree with this rounder.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.nonnegativeDyadicAt_eq_decodeFields_of_nonzero (format : Format) (code : ℕ) (hcode : code < format.signMaskNat) (hnonzero : code ≠ 0) : nonnegativeDyadicAt format code = (ofNatBits code).decodeFields.toDyadic

A positive code below the sign mask takes the ordinary finite branch of the totalized decoder.

Native-word and fixed-limb backends use this shared fact after proving that their direct field decoder agrees with Model.decodeFields; the exceptional-value argument therefore lives in one place rather than being duplicated by every representation backend.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.nonnegativeDyadicAt_toRat (format : Format) (code : ℕ) : (nonnegativeDyadicAt format code).toRat = nonnegativeRatAt format code

Dyadic code decoding has the same rational denotation as the reference helper.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.lowerCodeForPositive_eq_reference (format : Format) (target : Numerics.Dyadic) : lowerCodeForPositive format target = Model.lowerCodeForPositive format target.toRat

The dyadic and rational lower-code searches are extensionally identical.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.lowerCodeForPositive_eq_of_bracket (format : Format) (target : Numerics.Dyadic) (candidate : ℕ) (hcandidate : candidate < format.signMaskNat) (hlower : (nonnegativeDyadicAt format candidate).isLessOrEqual target = true) (hupper : candidate + 1 < format.signMaskNat → target.isLess (nonnegativeDyadicAt format (candidate + 1)) = true) : lowerCodeForPositive format target = candidate

A locally bracketed candidate is exactly the lower code selected by bisection.

This is a property of the exact dyadic specification, not of any execution backend. Direct packers use it to prove their field constructors once, then execute without searching.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.nonnegativeDyadicAt_one_eq_fields (format : Format) : nonnegativeDyadicAt format 1 = { negative := false, significand := 1, exponent := -(4 * Int.ofNat (format.payloadBits - 1)) }

Decoding code 1 yields the closed minimum-positive dyadic fields.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.minPositive_eq_fields (format : Format) : minPositive format = { negative := false, significand := 1, exponent := -(4 * Int.ofNat (format.payloadBits - 1)) }

The smallest positive posit is a unit significand at the bottom regime scale.

This closed form is shared by every execution backend, so underflow tests do not decode the fixed encoding 1 on each arithmetic operation.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.minPositive_eq_nonnegativeDyadicAt (format : Format) : minPositive format = nonnegativeDyadicAt format 1

The executable closed form equals the standard decoding of code 1.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.minPositive_exponent_le_scale_of_not_special {format : Format} (value : Model format) (hzero : value.isZero = false) (hnar : value.isNaR = false) : (minPositive format).exponent ≤ value.scale

The smallest positive posit's exponent is a lower bound for every ordinary nonzero posit scale.

The negative-regime case uses the mandatory terminator bit: a nonzero magnitude cannot consume the complete payload as a run of leading zeros. This is the representation fact needed to align an exact product of two posits with the associated quire.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.minPositive_toRat (format : Format) : (minPositive format).toRat = minPositiveRat format

The dyadic minimum has exactly the reference minimum's rational denotation.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.roundingThreshold_toRat (format : Format) (lowerCode : ℕ) : (roundingThreshold format lowerCode).toRat = Model.roundingThreshold format lowerCode

The dyadic threshold has exactly the reference threshold's rational denotation.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.chooseNearestCode_eq (target threshold : Numerics.Dyadic) (lower upper : ℕ) : chooseNearestCode target threshold lower upper = if target.isLess threshold = true then lower else if threshold.isLess target = true then upper else if lower % 2 = 0 then lower else upper

Single-comparison nearest-even selection equals the reference two-predicate decision tree.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.chooseNearestCode_eq_lower_or_upper (target threshold : Numerics.Dyadic) (lower upper : ℕ) : chooseNearestCode target threshold lower upper = lower ∨ chooseNearestCode target threshold lower upper = upper

Nearest-even selection returns one of the two supplied neighboring codes.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.roundPositiveCode_eq_reference_of_positive (format : Format) (target : Numerics.Dyadic) (hsignificand : target.significand ≠ 0) (hnegative : target.negative = false) : roundPositiveCode format target = Model.roundPositiveCode format target.toRat

Positive dyadic rounding selects exactly the code chosen by the rational specification.

The hypotheses are the invariant established by round: zero has already been handled and the temporary magnitude has its sign cleared.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.roundPositiveCode_nonnegativeDyadicAt (format : Format) {code : ℕ} (hcode : code < format.signMaskNat) : roundPositiveCode format (nonnegativeDyadicAt format code) = code

Positive exact-dyadic rounding re-encodes every nonnegative finite posit code.

This is the dyadic counterpart of Model.roundPositiveCode_nonnegativeRatAt. Native execution backends use it to return an exactly representable direct candidate without decoding its successor or the one-bit-wider rounding boundary.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.roundPositive_eq_reference_of_positive (format : Format) (target : Numerics.Dyadic) (hsignificand : target.significand ≠ 0) (hnegative : target.negative = false) : roundPositive format target = roundPositiveRat format target.toRat

Positive dyadic model rounding refines the reference rational model rounding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.magnitude_significand (value : Numerics.Dyadic) : (magnitude value).significand = value.significand

Clearing the sign leaves the integer significand unchanged.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.magnitude_negative (value : Numerics.Dyadic) : (magnitude value).negative = false

The magnitude of a dyadic has a clear sign bit.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.magnitude_toRat (value : Numerics.Dyadic) : (magnitude value).toRat = if value.negative = true then -value.toRat else value.toRat

Clearing the sign preserves a positive value and negates a negative value.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.restoreSignCode_lt_modulus (format : Format) (negative : Bool) (positiveCode : ℕ) (hpositive : positiveCode < format.signMaskNat) : restoreSignCode format negative positiveCode < format.modulus

Direct sign restoration preserves the configured posit word width.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicRounding.ofNatBits_restoreSignCode (format : Format) (negative : Bool) (positiveCode : ℕ) (hpositive : positiveCode < format.signMaskNat) : ofNatBits (restoreSignCode format negative positiveCode) = if negative = true then (ofNatBits positiveCode).neg else ofNatBits positiveCode

Packing a sign-restored code agrees with whole-word model negation.

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

Exact-dyadic rounding returns exactly the reference rational specification.