Correctness of two-word square root for normal inputs

The normal path aligns a fracWidth + 1-bit significand in a UInt256, computes a restoring integer square root with fracWidth + 1 base-four digits, and rounds from exact remainder information. sqrtNormal_refines identifies each accepted result with the public format-level square-root specification.

The kernel accepts only eligible layouts with fracWidth ≤ 124 and fracWidth + 1 ≤ bias. The first bound keeps the doubled remainder inside the two-word restoring state; the second is the hypothesis under which SqrtArithmetic.target_exponent identifies the model's target exponent with the kernel's affine exponent formula. Exceptional, subnormal, and unsupported inputs are left to the operation dispatcher. Runtime clients can import Sqrt.Runtime separately.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.sqrtNormal_refines {fmt : FloatFormat} (h : Eligible fmt) (x result : Model fmt) (hfast : sqrtNormal? x = some result) : result = Spec.sqrt x

Every accepted two-word square root agrees with the exact specification.