Refinement of wide-limb division

The limb decoder supplies the exact significands and their relative scale. The format's common scale offset cancels in division. Normal significands give the ratio exponent by one proved comparison, and every other finite case uses the exact rational exponent.

The quotient rounder agrees with the reference in every rounding direction. Finite zero operands follow the same invalid-operation and signed-overflow rules. For non-finite inputs, division's value result is independent of the rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.divisionMantissa_eq {fmt : FloatFormat} (x : Value fmt) : divisionMantissa x = FiniteKernel.decodeMantissa fmt (expField x) (fraction x).toNat

The division significand is the compact finite decoder's significand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.divisionRatioExponent_eq {fmt : FloatFormat} (x y : Value fmt) : divisionRatioExponent x y (divisionMantissa x) (divisionMantissa y) = Numerics.RationalBinary.floorLog2 (divisionMantissa x) (divisionMantissa y)

The fast normal comparison and the general subnormal path give the exact ratio exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.divFinite?_refines {fmt : FloatFormat} (h : Eligible fmt) (mode : IEEERoundingMode) (x y r : Value fmt) (hr : divFinite? fmt x y mode = some r) : toModel r = (toModel x).div (toModel y) mode

Every accepted finite quotient has the exact public result in the requested rounding mode.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.div_refines {fmt : FloatFormat} (h : Eligible fmt) (mode : IEEERoundingMode) (x y : Value fmt) : toModel (div fmt x y mode) = (toModel x).div (toModel y) mode

Total wide-limb division refines the public operation in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_div {fmt : FloatFormat} (h : Eligible fmt) (x y : Value fmt) : toModel (div fmt x y) = Spec.div (toModel x) (toModel y)

Wide-limb division in its default nearest-even mode agrees with Spec.div.