Correctness of native-word finite multiplication for generic binary32

The UInt64 multiplication kernel equals its exact-dyadic finite specification. Runtime clients can import Multiplication.Runtime without the component and rounding proofs.

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.mulFiniteWord_eq (x y : Value) : mulFiniteWord? x y = mulFinite? x y

Word-level finite multiplication equals the exact-dyadic mulFinite?.