Verified scale-aligned binary64 fused multiply-add

On the exact path the addend's scale is at most 62 bits above the product's, so shifting the addend significand by that difference places it at the product's scale. Their sum or difference needs at most 116 bits, and two native words hold it exactly before one nearest-even rounding. An addend below the product, or more than 62 bits above it, is aligned with a sticky bit instead (fmaJammed?), and the jammed magnitude rounds to the same result.

Zero and subnormal operands, exact or deep cancellation, 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

Sticky alignment outside the exact window

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

Native finite binary64 FMA, with its fallback, equals the generic finite kernel.