Exact Binary32 Subtraction

Sterbenz's lemma specialized to the rounded-real binary32 configuration fexp32 = fltExp (-149) 24. Two positive representable values within a factor of two have an exactly representable difference, so rounding that difference does nothing.

Reference

• P. H. Sterbenz, Floating-Point Computation, Prentice-Hall, 1974.

theorem TorchLean.Floats.round32_sub_exact_of_sterbenz {u v : ℝ} (hu : FloatLib.Floats.Formats.Flocq.genericFormat FloatLib.Numerics.binaryRadix fexp32 u) (hv : FloatLib.Floats.Formats.Flocq.genericFormat FloatLib.Numerics.binaryRadix fexp32 v) (hupos : 0 < u) (hvpos : 0 < v) (huv : u ≤ 2 * v) (hvu : v ≤ 2 * u) : round32 (u - v) = u - v

If two positive binary32-representable reals are within a factor of two, rounding their exact difference is the identity.

theorem TorchLean.Floats.FP32.sub_exact_of_sterbenz {a b : FP32} (ha : FloatLib.Floats.Formats.Flocq.NF.IsRepresentable a) (hb : FloatLib.Floats.Formats.Flocq.NF.IsRepresentable b) (hapos : 0 < a.val) (hbpos : 0 < b.val) (hab : a.val ≤ 2 * b.val) (hba : b.val ≤ 2 * a.val) : (a - b).val = a.val - b.val

Subtraction of positive representable FP32 values within a factor of two has no rounding error.