Correctness of rational-free exact posit quotient rounding

The executable quotient rounder compares candidate codes by cross multiplication instead of constructing the rational quotient. This module proves the positive-code search, threshold test, ties-to-even decision, sign handling, zero, and NaR branches equal to the reference rational specification.

The comparison remains exact: multiplying dyadics preserves their integer significands and binary exponents without rational normalization. The final theorem identifies the result with exact rational division followed by standard posit rounding.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.lowerCode_eq_reference (format : Format) (numerator denominator : Numerics.Dyadic) (hdenominator : 0 < denominator.toRat) : lowerCode format numerator denominator = lowerCodeForPositive format (numerator.toRat / denominator.toRat)

Exact product comparisons follow the reference rational quotient search.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.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)

Cross-multiplied quotient rounding selects exactly the rational specification's positive code.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.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)

Rational-free positive quotient rounding refines the reference rational model rounder.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.roundSignedWith_eq_reference (format : Format) (roundMagnitude : Numerics.Dyadic → Numerics.Dyadic → Model format) (hmagnitude : ∀ (numerator denominator : Numerics.Dyadic), numerator.significand ≠ 0 → numerator.negative = false → denominator.significand ≠ 0 → denominator.negative = false → roundMagnitude numerator denominator = roundPositiveRat format (numerator.toRat / denominator.toRat)) (numerator denominator : Numerics.Dyadic) : roundSignedWith format roundMagnitude numerator denominator = if denominator.toRat = 0 then nar format else roundRat format (numerator.toRat / denominator.toRat)

Any positive-magnitude rounder that refines the rational specification yields, through the shared signed shell roundSignedWith, the complete signed quotient specification.

The two exact quotient kernels differ only in their positive-magnitude rounder, so this single proof of the exceptional cases and the four sign cases serves both.

theorem FloatLib.Floats.Formats.Posit.Model.DyadicQuotient.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)

Signed cross-multiplied quotient rounding refines exact rational division and standard rounding.