Verified fixed-word kernels

Reusable one-, two-, and four-limb algorithms live here independently of any concrete numerical format. Runtime modules provide executable kernels; proof modules refine them to natural-number semantics. Binary floating-point and posit backends import this layer and supply their own decoding, rounding policy, and packing. Declarations use the FloatLib.Numerics.FixedWord namespace because they operate on the primitive fixed-word representations used throughout the numerical library. Their implementations and proofs are grouped here so different formats can reuse them.