Exact Subtraction

The fixed-point family is an additive lattice, so subtraction is exact without a ratio restriction. This is the fixed-grid foundation for the floating-point Sterbenz theorem, where the ratio hypotheses are needed to align the operands' effective exponents.

theorem TorchLean.Floats.FIXFormat_neg {β : NeuralRadix} {emin : ℤ} {x : ℝ} (hx : FIXFormat emin x) : FIXFormat emin (-x)

Values on a fixed grid are closed under negation.

theorem TorchLean.Floats.FIXFormat_add {β : NeuralRadix} {emin : ℤ} {x y : ℝ} (hx : FIXFormat emin x) (hy : FIXFormat emin y) : FIXFormat emin (x + y)

Values on a fixed grid are closed under addition.

theorem TorchLean.Floats.FIXFormat_sub {β : NeuralRadix} {emin : ℤ} {x y : ℝ} (hx : FIXFormat emin x) (hy : FIXFormat emin y) : FIXFormat emin (x - y)

Values on a fixed grid are closed under subtraction.

theorem TorchLean.Floats.neural_generic_format_FIX_sub {β : NeuralRadix} (emin : ℤ) {x y : ℝ} (hx : neuralGenericFormat β (FIXExp emin) x) (hy : neuralGenericFormat β (FIXExp emin) y) : neuralGenericFormat β (FIXExp emin) (x - y)

Generic FIX representability is closed under exact subtraction.

theorem TorchLean.Floats.neural_generic_format_FLX_sub_of_le_two_mul {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) {x y : ℝ} (hy : 0 < y) (hyx : y ≤ x) (hx2y : x ≤ 2 * y) (hxFmt : neuralGenericFormat β (FLXExp prec) x) (hyFmt : neuralGenericFormat β (FLXExp prec) y) : neuralGenericFormat β (FLXExp prec) (x - y)

Sterbenz's lemma for the unbounded-exponent format: if two positive representable values differ by at most a factor of two, then their subtraction is exactly representable at the same precision.

The proof does not appeal to rounding. The ratio bound shows that the operands' magnitudes differ by at most one radix bin. Their integer scaled mantissas can therefore be aligned on the smaller canonical exponent, and the exact integer difference is fine enough for the result's canonical exponent.

theorem TorchLean.Floats.neural_generic_format_FLX_sterbenz {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hx2y : x ≤ 2 * y) (hy2x : y ≤ 2 * x) (hxFmt : neuralGenericFormat β (FLXExp prec) x) (hyFmt : neuralGenericFormat β (FLXExp prec) y) : neuralGenericFormat β (FLXExp prec) (x - y)

Symmetric Sterbenz lemma for FLX. If two positive representable values are within a factor of two, their exact difference is representable, whichever operand is larger.