Two-word division runtime

The first path checks a radix-2^32 quotient candidate with an independent Euclidean certificate. A rejected candidate is replaced by the fixed-word restoring result whose equality to the logical divider is proved in CertifiedDivision.Proof. The selected pair is then rounded and packed. This module exposes only the partial specialized kernel for every eligible two-word layout; the dispatcher owns the exact baseline for cases outside its normal finite range.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.divNormal? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Try certified fixed-word division for two normal operands.

Descriptor specialization follows the pattern described in Dispatch.Add.Runtime.