Certified two-word normal division

The radix-2^32 loop produces the first quotient candidate, and 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 go to the generic exact-rational backend. The main theorem is divNormal_refines.

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

An eligible fraction width satisfies 64 < fracWidth ≤ 126, 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.