Agreement with Lean's floating-point arithmetic

Model retains IEEE NaN payloads, while Lean's UnpackedFloat has a single canonical NaN. The bridges in this module therefore compare the real semantics of finite results for descriptors satisfying fmt.isIEEE = true. They connect Lean's arithmetic algorithms to the same independent roundAt specification used for Model, without identifying representation policies that deliberately differ.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_normalize_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mantissa exponent : ℤ) (zeroSign : Float.Model.UnpackedFloat.Sign) (hfinite : (ofModel fmt (Float.Model.UnpackedFloat.normalize fmt.toModel mantissa exponent zeroSign)).isFinite = true) : (ofModel fmt (Float.Model.UnpackedFloat.normalize fmt.toModel mantissa exponent zeroSign)).toReal = roundAt fmt (↑mantissa * Flocq.bpow Numerics.binaryRadix exponent)

Packing Lean's signed-integer normalizer has the independent nearest-even real semantics. The zero sign is intentionally absent from the conclusion because both signed zeros denote zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_add_finite_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign₁ sign₂ : Float.Model.UnpackedFloat.Sign) (mantissa₁ mantissa₂ : ℕ) (exponent₁ exponent₂ : ℤ) (hmantissa₁ : 0 < mantissa₁) (hmantissa₂ : 0 < mantissa₂) (hfinite : (ofModel fmt (Float.Model.UnpackedFloat.add fmt.toModel (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))).isFinite = true) : (ofModel fmt (Float.Model.UnpackedFloat.add fmt.toModel (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))).toReal = roundAt fmt (unpackedToReal (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) + unpackedToReal (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))

For finite operands and a finite result, Lean core's unpacked addition has the same independent nearest-even real semantics as Model.add.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_mul_finite_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign₁ sign₂ : Float.Model.UnpackedFloat.Sign) (mantissa₁ mantissa₂ : ℕ) (exponent₁ exponent₂ : ℤ) (hmantissa₁ : 0 < mantissa₁) (hmantissa₂ : 0 < mantissa₂) (hle : exponent₁ + exponent₂ ≤ fmt.toModel.targetExponent (Float.Model.totalExponent (mantissa₁ * mantissa₂) (exponent₁ + exponent₂))) (hfinite : (ofModel fmt (Float.Model.UnpackedFloat.mul fmt.toModel (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))).isFinite = true) : (ofModel fmt (Float.Model.UnpackedFloat.mul fmt.toModel (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))).toReal = roundAt fmt (unpackedToReal (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) * unpackedToReal (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))

For finite operands satisfying Lean core's documented roundWithAccuracy precondition, unpacked multiplication has the same independent nearest-even real semantics as Model.mul.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_div_finite_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign₁ sign₂ : Float.Model.UnpackedFloat.Sign) (mantissa₁ mantissa₂ : ℕ) (exponent₁ exponent₂ : ℤ) (hmantissa₁ : 0 < mantissa₁) (hmantissa₂ : 0 < mantissa₂) (hquotient : (Float.Model.UnpackedFloat.divCore fmt.toModel mantissa₁ exponent₁ mantissa₂ exponent₂).1 ≠ 0) (hle : (Float.Model.UnpackedFloat.divCore fmt.toModel mantissa₁ exponent₁ mantissa₂ exponent₂).2.1 ≤ fmt.toModel.targetExponent (Float.Model.totalExponent (Float.Model.UnpackedFloat.divCore fmt.toModel mantissa₁ exponent₁ mantissa₂ exponent₂).1 (Float.Model.UnpackedFloat.divCore fmt.toModel mantissa₁ exponent₁ mantissa₂ exponent₂).2.1)) (hfinite : (ofModel fmt (Float.Model.UnpackedFloat.div fmt.toModel (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))).isFinite = true) : (ofModel fmt (Float.Model.UnpackedFloat.div fmt.toModel (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))).toReal = roundAt fmt (unpackedToReal (Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) / unpackedToReal (Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂))

For finite nonzero operands satisfying Lean core's documented roundWithAccuracy precondition, unpacked division has the same independent nearest-even real semantics as Model.div.

The nonzero provisional quotient premise records that divCore produced at least one significant bit. It is the natural domain of the generic accuracy-to-rounding bridge.