Correctness of native one-word finite division

The one-word quotient kernel computes only cases whose normalized quotient and rounding evidence fit its fixed-width budget. Every IEEE descriptor stored in one word meets this budget: the sign and at least two exponent bits leave at most 61 fraction bits. The refinement relates its logarithms, restoring quotient, guard/sticky information, and packed result to the complete format-generic quotient rounder.

Under NativeSmallWord.StorageEligible, divNormal_refines_of_storage identifies every accepted result with FiniteKernel.div?. Declined inputs use the dispatcher's exact generic fallback.

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordDiv.roundNormalNativeBounds? (fmt : FloatFormat) (sign : Bool) (num den : UInt64) (exponent : ℤ) : Option (Model fmt)

The one-word quotient rounder with the format's named normal exponent bounds in place of the machine-word bias.

roundNormalNative? reads its bounds from NativeSmallWord.biasInt so that compiled code performs no Nat shift per call; this proof-facing twin is the same computation stated with ieeeMinNormalExponent, ieeeMaxNormalExponent, and bias, and roundNormalNative_eq_bounds identifies the two for every one-word format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordDiv.roundNormalNative_eq_bounds (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (sign : Bool) (num den : UInt64) (exponent : ℤ) : roundNormalNative? fmt sign num den exponent = roundNormalNativeBounds? fmt sign num den exponent

The machine-word bias rounder is the rounder with the format's named exponent bounds.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordDiv.divNormal_refines_of_storage {fmt : FloatFormat} (heligible : NativeSmallWord.StorageEligible fmt) (x y result : Model fmt) (hresult : divNormal? x y = some result) : FiniteKernel.div? x y = some result

Restoring division refines the finite kernel for every descriptor within its word capacity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordDiv.divNormal_refines {fmt : FloatFormat} (heligible : NativeSmallWord.Eligible fmt) (x y result : Model fmt) (hresult : divNormal? x y = some result) : FiniteKernel.div? x y = some result

The shared small-word capacity is sufficient for native normal division.