Correctness of direct posit quotient packing

The executable quotient path generates one destination-width normalized quotient prefix, jams the exact Euclidean remainder into its sticky bit, and feeds that stream to the shared direct Posit packer. This module proves that the result is the rounding of the exact rational quotient, with NaR for division by zero. The proof applies at every format width.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundPositiveCode_prefix_eq_reference (format : Format) (targetExponent : ℤ) (quotient remainder denominator leading : ℕ) (hleadingWidth : format.payloadBits ≤ leading) (hlower : 2 ^ leading ≤ quotient) (hupper : quotient < 2 ^ (leading + 1)) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) : DirectDyadicPacking.roundPositiveCode format { negative := false, significand := StickyPrefix.jamRemainder quotient remainder, exponent := targetExponent } = Model.roundPositiveCode format ((↑quotient + ↑remainder / ↑denominator) * 2 ^ targetExponent)

The shared direct dyadic packer rounds a normalized quotient prefix exactly as the unmaterialized rational quotient fraction.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundPositiveCode_eq_reference (format : Format) (numerator denominator : Numerics.Dyadic) (hnumeratorSignificand : numerator.significand ≠ 0) (hnumeratorNegative : numerator.negative = false) (hdenominatorSignificand : denominator.significand ≠ 0) (hdenominatorNegative : denominator.negative = false) : roundPositiveCode format numerator denominator = Model.roundPositiveCode format (numerator.toRat / denominator.toRat)

Direct positive quotient rounding refines exact rational division.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundPositiveCode_lt_signMask (format : Format) (numerator denominator : Numerics.Dyadic) : roundPositiveCode format numerator denominator < format.signMaskNat

Direct positive quotient rounding always selects a finite nonnegative code.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundPositive_eq_reference (format : Format) (numerator denominator : Numerics.Dyadic) (hnumeratorSignificand : numerator.significand ≠ 0) (hnumeratorNegative : numerator.negative = false) (hdenominatorSignificand : denominator.significand ≠ 0) (hdenominatorNegative : denominator.negative = false) : roundPositive format numerator denominator = roundPositiveRat format (numerator.toRat / denominator.toRat)

Direct positive quotient packing refines exact positive rational rounding.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.round_eq_reference (format : Format) (numerator denominator : Numerics.Dyadic) : round format numerator denominator = if denominator.toRat = 0 then nar format else roundRat format (numerator.toRat / denominator.toRat)

Direct signed quotient rounding refines exact rational division.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.round_eq_dyadicQuotient (format : Format) (numerator denominator : Numerics.Dyadic) : round format numerator denominator = DyadicQuotient.round format numerator denominator

The direct quotient kernel and the general exact quotient rounder choose the same result.

Only their positive-magnitude kernels differ, and both are certified against the same rational rounding specification.

Code-valued boundary

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundCode_eq_toNatBits (format : Format) (numerator denominator : Numerics.Dyadic) : roundCode format numerator denominator = (round format numerator denominator).toNatBits

The code-valued quotient is the encoding of the model-valued quotient.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.roundCode_lt_modulus (format : Format) (numerator denominator : Numerics.Dyadic) : roundCode format numerator denominator < format.modulus

Every quotient code fits the configured posit word.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.ofNatBits_roundCode (format : Format) (numerator denominator : Numerics.Dyadic) : ofNatBits (roundCode format numerator denominator) = round format numerator denominator

Re-encoding the quotient code recovers the model-valued quotient.