Exact Representations for Rounded Arithmetic

The error theorems for addition, multiplication, division, and square root need more than a bound: they track the grid on which an intermediate value is exactly representable. The lemmas below are the common representation layer for those developments.

theorem FloatLib.Floats.Formats.Flocq.round_toReal_exists_same_exponent {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (f : FloatRep β) : ∃ (m : ℤ), round rnd (toReal f) = toReal { mantissa := m, exponent := f.exponent }

Rounding a mantissa/exponent value can be represented using its original exponent.

If the canonical exponent is no larger than the stored exponent, the input is already generic and rounding fixes it. Otherwise the rounded canonical mantissa is shifted by an integral radix power. This is the Lean counterpart of Flocq's round_repr_same_exp.

theorem FloatLib.Floats.Formats.Flocq.toReal_add_exists_min_exponent {β : Numerics.Radix} (f g : FloatRep β) : ∃ (h : FloatRep β), toReal f + toReal g = toReal h ∧ h.exponent = min f.exponent g.exponent

The sum of two mantissa/exponent values has a representation at the smaller exponent.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLX_add_of_repr_bounds {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (f g : FloatRep β) (x y : ℝ) (hx : x = toReal f) (hy : y = toReal g) (hxf : |x + y| < bpow β (prec + f.exponent)) (hyg : |x + y| < bpow β (prec + g.exponent)) : genericFormat β (flxExp prec) (x + y)

An FLX sum is representable when it fits in prec radix digits relative to both operand representations. This is the common-grid lemma used by division and square-root residual proofs.