Certified two-word normal division

The radix-2^32 loop generates the first quotient candidate. A failed certificate selects the proved two-limb restoring result. The selected quotient is certified for every normalized input of an eligible layout, so this backend has no candidate-failure branch. Exceptional values, subnormal operands and results, and overflow boundaries retain the generic exact-rational backend. Start with divNormal_refines.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.precision_bounds {fmt : FloatFormat} (h : Eligible fmt) : 64 < fmt.fracWidth ∧ fmt.fracWidth ≤ 126

The precision of an eligible descriptor is within the certified division range.

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

Every accepted certified quotient agrees with the exact finite division kernel.