Native values through the shared representation bridge

Lean 4.34 exposes named NaN and infinity constants alongside the logical floating-point models introduced in Lean 4.33. We're glad Lean is making more of this model available for proofs. Here we connect those constants and the existing ofFloat / toFloat adapters to the same packed-model proofs used for arithmetic and integer conversion.

Every native value round-trips exactly. In the other direction, a FloatLib word may carry a NaN payload that Lean's model does not retain; Model.canonicalizeModel describes that change. Finite values, infinities, and both signed zeros retain their bits.

Binary32

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32 (value : Float32) : toModel (ofFloat32 value) = Formats.BinaryInterchange.Model.ofFloat32Model value.toModel

Importing a native value reads the word in its logical binary32 model.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_toFloat32_eq (value : Binary 8 23 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toModel_toFloat32_eq._proof_1 toModel_toFloat32_eq._proof_2 toModel_toFloat32_eq._proof_3 toModel_toFloat32_eq._proof_4) : value.toFloat32.toModel = (toModel value).toFloat32Model

Exporting binary32 uses the shared packed-model conversion, including NaN normalization.

theorem FloatLib.Floats.ExecFloat.Binary.isModelCanonical_ofFloat32 (value : Float32) : (toModel (ofFloat32 value)).IsModelCanonical

An imported native binary32 value already satisfies Lean's canonical-NaN invariant.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toFloat32_ofFloat32 (value : Float32) : (ofFloat32 value).toFloat32 = value

Every native binary32 value is recovered exactly after importing and exporting it.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_nan : toModel (ofFloat32 Float32.nan) = Formats.BinaryInterchange.Model.canonicalNaN Formats.BinaryInterchange.FloatFormat.binary32

Lean 4.34's binary32 NaN imports as FloatLib's canonical quiet NaN.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_inf : toModel (ofFloat32 Float32.inf) = Formats.BinaryInterchange.Model.posInf Formats.BinaryInterchange.FloatFormat.binary32

Lean 4.34's binary32 infinity imports as FloatLib's positive infinity.

Binary64

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat (value : Float) : toModel (ofFloat value) = Formats.BinaryInterchange.Model.ofFloatModel value.toModel

Importing a native value reads the word in its logical binary64 model.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_toFloat_eq (value : Binary 11 52 Formats.BinaryInterchange.FloatFormat.Encoding.ieee (Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 11) toModel_toFloat_eq._proof_1 toModel_toFloat_eq._proof_2 toModel_toFloat_eq._proof_3 toModel_toFloat_eq._proof_4) : value.toFloat.toModel = (toModel value).toFloatModel

Exporting binary64 uses the shared packed-model conversion, including NaN normalization.

theorem FloatLib.Floats.ExecFloat.Binary.isModelCanonical_ofFloat (value : Float) : (toModel (ofFloat value)).IsModelCanonical

An imported native binary64 value already satisfies Lean's canonical-NaN invariant.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toFloat_ofFloat (value : Float) : (ofFloat value).toFloat = value

Every native binary64 value is recovered exactly after importing and exporting it.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_nan : toModel (ofFloat Float.nan) = Formats.BinaryInterchange.Model.canonicalNaN Formats.BinaryInterchange.FloatFormat.binary64

Lean 4.34's binary64 NaN imports as FloatLib's canonical quiet NaN.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_inf : toModel (ofFloat Float.inf) = Formats.BinaryInterchange.Model.posInf Formats.BinaryInterchange.FloatFormat.binary64

Lean 4.34's binary64 infinity imports as FloatLib's positive infinity.