Sterbenz exact subtraction

Sterbenz's lemma applies to the rounded-real grid of every fmt: two positive representable values within a factor of two have an exactly representable difference. For an IEEE descriptor, subtraction of the corresponding finite model values remains finite and decodes to that exact real difference.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_sub_eq_of_sterbenz (fmt : FloatFormat) {u v : ℝ} (hu : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) u) (hv : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) v) (hupos : 0 < u) (hvpos : 0 < v) (huv : u ≤ 2 * v) (hvu : v ≤ 2 * u) : roundAt fmt (u - v) = u - v

Sterbenz exactness for the rounded-real grid selected by fmt: two positive representable reals within a factor of two have a representable difference, so nearest-even rounding changes nothing.

Strict positivity excludes signed-zero bookkeeping; the executable theorem below handles the corresponding finite model values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_sub_eq_of_sterbenz {fmt : FloatFormat} {x y : Model fmt} (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hxpos : 0 < x.toReal) (hypos : 0 < y.toReal) (hxy : x.toReal ≤ 2 * y.toReal) (hyx : y.toReal ≤ 2 * x.toReal) : (x.sub y).toReal = x.toReal - y.toReal

Subtraction of positive finite executable values within a factor of two has no rounding error.

The Sterbenz hypotheses also bound the exact difference by one of the finite operands, so finiteness of the executable result follows rather than appearing as a separate premise.