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

These bridges compare FloatLib square root with the Lean 4.34 logical model underlying the native floating-point types. Canonicalization forgets NaN payloads and signs while retaining all numeric bits, including the sign of zero. The model equality does not verify the external 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) : x.sqrt.canonicalizeModel = ofModel fmt (Float.Model.UnpackedFloat.sqrt fmt.toModel x.toModel)

Square root agrees on every conventional IEEE input after NaN canonicalization. The equality retains signed zeros and covers negative arguments, infinities, and both kinds of NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toFloat32Model_sqrt (x : Model FloatFormat.binary32) : x.sqrt.toFloat32Model = 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) : x.sqrt.toFloatModel = 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) : toModel (ofFloat32 x.sqrt) = (toModel (ofFloat32 x)).sqrt.canonicalizeModel

Lean 4.34 binary32 square root agrees with FloatLib square root through the existing native adapter. Only NaN signs and payloads are discarded by the representation relation.

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

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

theorem FloatLib.Floats.ExecFloat.Binary.toFloat32_sqrt (x : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toFloat32_sqrt._proof_1 toFloat32_sqrt._proof_2 toFloat32_sqrt._proof_3 toFloat32_sqrt._proof_4) : toFloat32 (sqrt x) = x.toFloat32.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 : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) toFloat_sqrt._proof_1 toFloat_sqrt._proof_2 toFloat_sqrt._proof_3 toFloat_sqrt._proof_4) : toFloat (sqrt x) = x.toFloat.sqrt

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