Square-root agreement with Lean's floating-point model

These theorems relate FloatLib square root to the Lean logical model underlying the native floating-point types. Canonicalization forgets NaN payloads and signs and keeps all numeric bits, including the sign of zero. The model equality does not verify the machine instructions used by compiled native operations.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.canonicalizeModel_sqrt_eq_model {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x : Model fmt) : canonicalizeModel x.sqrt = ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel x.toModel)

Square root agrees with Lean's model on every input of an IEEE format after NaN canonicalization. The equality keeps signed zeros and covers negative arguments, infinities, and both kinds of NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloat32Model_sqrt (x : Model FloatFormat.binary32) : toFloat32Model x.sqrt = x.toFloat32Model.sqrt

Exporting a binary32 square root gives the square root of the exported Lean model.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloatModel_sqrt (x : Model FloatFormat.binary64) : toFloatModel x.sqrt = x.toFloatModel.sqrt

Exporting a binary64 square root gives the square root of the exported Lean model.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_sqrt (x : Float32) : (ofFloat32 x.sqrt).toModel = Formats.BinaryInterchange.Model.canonicalizeModel (ofFloat32 x).toModel.sqrt

Lean binary32 square root agrees with FloatLib square root through the native adapter. Canonicalization discards only NaN signs and payloads.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_sqrt (x : Float) : (ofFloat x.sqrt).toModel = Formats.BinaryInterchange.Model.canonicalizeModel (ofFloat x).toModel.sqrt

Lean binary64 square root agrees with FloatLib square root through the native adapter, including signed zeros and exceptional results.

theorem FloatLib.Floats.ExecFloat.Binary.toFloat32_sqrt (x : Binary32) : toFloat32 (sqrt x) = (toFloat32 x).sqrt

Configured binary32 square root commutes with export to Lean's native Float32, for every input word. This uses the installed certified software operation.

theorem FloatLib.Floats.ExecFloat.Binary.toFloat_sqrt (x : Binary64) : toFloat (sqrt x) = (toFloat x).sqrt

Configured binary64 square root commutes with export to Lean's native Float, including signed zeros, infinities, and NaNs under Lean's canonical representation.