Addition and subtraction through Lean's floating-point model

The exact dyadic addition used by FloatLib and Lean's unpacked addition align the operands at the smaller exponent before rounding once. Their agreement includes cancellation to positive zero and overflow to infinity. A descriptor must have the conventional IEEE encoding and bias. These bridges are checked against the logical floating-point model shipped with Lean 4.34.

NaN payloads require care at the native boundary: FloatLib propagates a quieted payload, whereas Lean's unpacked model has a single NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.add_eq_ofModel_add_of_toModel_finite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x y : Model fmt) (sign₁ sign₂ : Float.Model.UnpackedFloat.Sign) (mantissa₁ mantissa₂ : ℕ) (exponent₁ exponent₂ : ℤ) (hmantissa₁ : 0 < mantissa₁) (hmantissa₂ : 0 < mantissa₂) (hx : x.toModel = Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) (hy : y.toModel = Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂) : x.add y = ofModel fmt (Float.Model.UnpackedFloat.add fmt.toModel x.toModel y.toModel)

For finite nonzero operands, dispatched addition commutes with Lean's unpacked addition and packing. The result may be zero or infinity; no finiteness assumption on the sum is needed.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpacked_sub_eq_add_neg (spec : Float.Model.Format) (x y : Float.Model.UnpackedFloat) : Float.Model.UnpackedFloat.sub spec x y = Float.Model.UnpackedFloat.add spec x y.neg

Lean's unpacked subtraction is addition after exact negation, including exceptional values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sub_eq_ofModel_sub_of_toModel_finite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x y : Model fmt) (sign₁ sign₂ : Float.Model.UnpackedFloat.Sign) (mantissa₁ mantissa₂ : ℕ) (exponent₁ exponent₂ : ℤ) (hmantissa₁ : 0 < mantissa₁) (hmantissa₂ : 0 < mantissa₂) (hx : x.toModel = Float.Model.UnpackedFloat.finite sign₁ mantissa₁ exponent₁ hmantissa₁) (hy : y.toModel = Float.Model.UnpackedFloat.finite sign₂ mantissa₂ exponent₂ hmantissa₂) : x.sub y = ofModel fmt (Float.Model.UnpackedFloat.sub fmt.toModel x.toModel y.toModel)

For finite nonzero operands, dispatched subtraction commutes with Lean's unpacked subtraction and packing, including exact cancellation and overflow.