Verified scale-aligned binary64 fused multiply-add

For the accepted normal inputs, shifting the addend significand by the binary64 fraction width places it at the product's scale. Their sum or difference needs at most 107 bits, so two native words hold the exact intermediate value before one nearest-even rounding.

Exact zero, deep cancellation, different scale alignments, and results outside the normal rounder's range use the generic finite kernel. Non-finite operands are handled by the outer arithmetic dispatcher.

Two-word exact arithmetic

Scale-aligned component semantics

Refinement of native product rounding

Native fast-path refinements

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaFiniteFastImpl_eq (x y z : Value) : fmaFiniteFastImpl? x y z = FiniteKernel.fma? x y z

The native aligned binary64 FMA path refines the existing exact finite kernel.