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. This file contains the representation lemmas shared by those developments.

theorem TorchLean.Floats.neuralRound_toReal_exists_same_exponent {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (f : NeuralFloat β) : ∃ (m : ℤ), neuralRound rnd (neuralToReal f) = neuralToReal { 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 TorchLean.Floats.neuralToReal_add_exists_min_exponent {β : NeuralRadix} (f g : NeuralFloat β) : ∃ (h : NeuralFloat β), neuralToReal f + neuralToReal g = neuralToReal h ∧ h.exponent = min f.exponent g.exponent

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

theorem TorchLean.Floats.neural_generic_format_FLX_add_of_repr_bounds {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (f g : NeuralFloat β) (x y : ℝ) (hx : x = neuralToReal f) (hy : y = neuralToReal g) (hxf : |x + y| < neuralBpow β (prec + f.exponent)) (hyg : |x + y| < neuralBpow β (prec + g.exponent)) : neuralGenericFormat β (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.