Native addition and subtraction

These bridges are checked against the logical floating-point model shipped with Lean 4.34. Finite inputs include both signed zeros. The result is unrestricted: cancellation, subnormal rounding, and overflow to infinity all preserve the complete packed word through the existing native adapters.

The finite-input hypotheses exclude NaNs and infinities. FloatLib preserves NaN details that Lean canonicalizes; subtraction also negates the right operand's NaN sign. These model equalities do not verify the external machine instructions used by compiled native code.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.add_eq_ofModel_add_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x y : Model fmt) (hx : x.toModel.isFinite = true) (hy : y.toModel.isFinite = true) : x.add y = ofModel fmt (Float.Model.UnpackedFloat.add fmt.toModel x.toModel y.toModel)

For finite operands, including signed zeros, dispatched addition produces precisely the word obtained by adding and packing in Lean's unpacked model. The result may overflow to infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_neg_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x : Model fmt) (hx : x.toModel.isFinite = true) : x.neg.toModel = x.toModel.neg

Negation preserves the complete finite unpacked value, including the sign of zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sub_eq_ofModel_sub_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x y : Model fmt) (hx : x.toModel.isFinite = true) (hy : y.toModel.isFinite = true) : x.sub y = ofModel fmt (Float.Model.UnpackedFloat.sub fmt.toModel x.toModel y.toModel)

For finite operands, including signed zeros, dispatched subtraction agrees with Lean's unpacked subtraction and packing. There is no restriction on the rounded result.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_add_of_isFinite (x y : Float32) (hx : x.isFinite = true) (hy : y.isFinite = true) : toModel (ofFloat32 (x + y)) = (toModel (ofFloat32 x)).add (toModel (ofFloat32 y))

Native binary32 addition commutes with the existing import adapter for all finite inputs.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_sub_of_isFinite (x y : Float32) (hx : x.isFinite = true) (hy : y.isFinite = true) : toModel (ofFloat32 (x - y)) = (toModel (ofFloat32 x)).sub (toModel (ofFloat32 y))

Native binary32 subtraction commutes with the import adapter, including signed-zero inputs.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_add_of_isFinite (x y : Float) (hx : x.isFinite = true) (hy : y.isFinite = true) : toModel (ofFloat (x + y)) = (toModel (ofFloat x)).add (toModel (ofFloat y))

Native binary64 addition commutes with the existing import adapter for all finite inputs.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_sub_of_isFinite (x y : Float) (hx : x.isFinite = true) (hy : y.isFinite = true) : toModel (ofFloat (x - y)) = (toModel (ofFloat x)).sub (toModel (ofFloat y))

Native binary64 subtraction commutes with the import adapter, including signed-zero inputs.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat32_add_of_isFinite (x y : Float32) (hx : x.isFinite = true) (hy : y.isFinite = true) : ofFloat32 (x + y) = ofFloat32 x + ofFloat32 y

Importing the native sum equals adding the imported binary32 operands with the installed certified software operation. Finite inputs may produce zero, a subnormal, or infinity.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat32_sub_of_isFinite (x y : Float32) (hx : x.isFinite = true) (hy : y.isFinite = true) : ofFloat32 (x - y) = ofFloat32 x - ofFloat32 y

Importing a native binary32 difference equals certified software subtraction of the imports.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat_add_of_isFinite (x y : Float) (hx : x.isFinite = true) (hy : y.isFinite = true) : ofFloat (x + y) = ofFloat x + ofFloat y

Importing the native sum equals adding the imported binary64 operands with the installed certified software operation, including cancellation and overflow.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat_sub_of_isFinite (x y : Float) (hx : x.isFinite = true) (hy : y.isFinite = true) : ofFloat (x - y) = ofFloat x - ofFloat y

Importing a native binary64 difference equals certified software subtraction of the imports.