Correctness of native-word finite multiplication for generic binary32

The direct UInt64 multiplication kernel is proved equivalent to its exact-dyadic finite specification. Runtime clients can import Multiplication.Runtime without the component and rounding developments.

The significands have at most 24 bits, so their product is exact in UInt64. The proof bounds the unsigned product scale and applies the native rounder theorem for FloatFormat.binary32.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.mulFiniteImpl_eq (x y : Value) : mulFiniteImpl? x y = mulFinite? x y

The direct UInt64 finite multiply kernel equals the exact-dyadic reference operation.