Correctness of multiplication backends

Every route through the multiplication dispatcher meets Spec.mul: binary32, binary64, fixed-pair, parameterized one-word, two-word, and generic implementations differ only in storage and execution strategy.

Each fast kernel is allowed to decline when its structural or finite-input preconditions fail. The proof shows that successful results are exact refinements and that every decline reaches the single generic specification-preserving path. Runtime clients can import Mul.Runtime without loading these theorems.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.MulBackend.generic_eq_spec {fmt : FloatFormat} (x y : Model fmt) : generic x y = Spec.mul x y

Compact generic multiplication preserves the public exact-dyadic operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.MulBackend.word_eq_spec {fmt : FloatFormat} (x y : Model fmt) : word x y = Spec.mul x y

The native fixed-format and parameterized one- and two-word dispatches preserve multiplication.