Correctness of native-backed unpacked floating-point square root

The executable implementation lives in ModelSqrt.Runtime. This module proves exact agreement with Lean's logical unpacked-float operation and registers the verified compiler substitution.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeModelSqrt.sqrtCore_eq (spec : Float.Model.Format) (mantissa : ℕ) (exponent : ℤ) : sqrtCore spec mantissa exponent = Float.Model.UnpackedFloat.sqrtCore spec mantissa exponent

The native-backed core is exactly Lean's logical unpacked square-root core.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeModelSqrt.sqrt_eq (spec : Float.Model.Format) (value : Float.Model.UnpackedFloat) : sqrt spec value = Float.Model.UnpackedFloat.sqrt spec value

The native-backed operation is exactly Lean's logical unpacked floating-point square root.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeModelSqrt.unpackedSqrt_eq_sqrt : Float.Model.UnpackedFloat.sqrt = sqrt

Compile Lean's logical unpacked square root through the proved native-backed implementation.