Exactness of Multiplication Errors

In the unbounded-exponent FLX format, the residual of a rounded product of two representable operands is itself representable. The rounding mode may be any valid monotone integer rounding.

theorem TorchLean.Floats.neural_generic_format_FLX_mul_bpow {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : neuralGenericFormat β (FLXExp prec) x) (e : ℤ) : neuralGenericFormat β (FLXExp prec) (x * neuralBpow β e)

Multiplication by a radix power preserves FLX representability.

theorem TorchLean.Floats.neural_mul_round_error_FLX_exists_repr {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x y : ℝ} (hx : neuralGenericFormat β (FLXExp prec) x) (hy : neuralGenericFormat β (FLXExp prec) y) (herr0 : neuralRound rnd (x * y) - x * y ≠ 0) : ∃ (f : NeuralFloat β), neuralRound rnd (x * y) - x * y = neuralToReal f ∧ neuralCexp β (FLXExp prec) (neuralRound rnd (x * y) - x * y) ≤ f.exponent ∧ f.exponent = neuralCexp β (FLXExp prec) x + neuralCexp β (FLXExp prec) y

A nonzero rounded-product residual has a representation at the sum of the operand canonical exponents. This is the exponent-carrying form needed by FLT underflow proofs.

theorem TorchLean.Floats.neural_mul_round_error_FLX {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x y : ℝ} (hx : neuralGenericFormat β (FLXExp prec) x) (hy : neuralGenericFormat β (FLXExp prec) y) : neuralGenericFormat β (FLXExp prec) (neuralRound rnd (x * y) - x * y)

The residual of a valid rounded FLX product is exactly FLX-representable.

theorem TorchLean.Floats.neural_generic_format_FLT_to_FLX {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : neuralGenericFormat β (FLTExp emin prec) x) : neuralGenericFormat β (FLXExp prec) x

Every FLT value is representable in the corresponding unbounded FLX format.

theorem TorchLean.Floats.neural_mul_round_error_FLT {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x y : ℝ} (hx : neuralGenericFormat β (FLTExp emin prec) x) (hy : neuralGenericFormat β (FLTExp emin prec) y) (hproduct : x * y ≠ 0 → neuralBpow β (emin + 2 * prec - 1) ≤ |x * y|) : neuralGenericFormat β (FLTExp emin prec) (neuralRound rnd (x * y) - x * y)

The residual of an FLT rounded product is FLT-representable when the exact product is above the underflow threshold β^(emin + 2*prec - 1).

theorem TorchLean.Floats.neural_generic_format_FLT_mul_bpow {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : neuralGenericFormat β (FLTExp emin prec) x) (e : ℤ) (hshift : emin + prec - neuralMagnitude β x ≤ e) : neuralGenericFormat β (FLTExp emin prec) (x * neuralBpow β e)

FLT multiplication by a radix power is exact when the shift stays above emin.

theorem TorchLean.Floats.neural_generic_format_FLT_mul_bpow_of_nonneg {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : neuralGenericFormat β (FLTExp emin prec) x) (e : ℤ) (he : 0 ≤ e) : neuralGenericFormat β (FLTExp emin prec) (x * neuralBpow β e)

Nonnegative radix shifts preserve every FLT-representable value.