IEEE32Exec per-op real error bounds (finite branch)

NN.Floats.IEEEExec.Bridge.FP32Total provides refinement theorems of the form

$$ \operatorname{toReal}(\operatorname{op}_{\mathrm{exec}}(x,y)) =\operatorname{fp32Round}\!\left( \operatorname{op}_{\mathrm{real}}(\operatorname{toReal}(x),\operatorname{toReal}(y)) \right), $$

valid when the executable result stays finite (no NaN/Inf).

This file turns those equalities into the standard half-ULP absolute error bounds you want in numerical proofs:

$$ \left| \operatorname{toReal}(\operatorname{op}_{\mathrm{exec}}(x,y)) -\operatorname{op}_{\mathrm{real}}(\operatorname{toReal}(x),\operatorname{toReal}(y)) \right| \le \varepsilon_{32}\!\left( \operatorname{op}_{\mathrm{real}}(\operatorname{toReal}(x),\operatorname{toReal}(y)) \right). $$

We intentionally do not provide bounds for sin/cos here: the current executable implementation is deterministic (see NN.Floats.IEEEExec.Exec32), but it is an algorithmic approximation rather than “real trig + one rounding step”, so its real-analytic error bounds live in a separate trig-specific theory file.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round_abs_error (x : ℝ) : |fp32Round x - x| ≤ eps₃₂ x

fp32Round has the standard half-ULP absolute error bound.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round_relative_error_of_normal (x : ℝ) (hx : x ≠ 0) (hnormal : FP32.minNormal ≤ |x|) : ErrorBounds.relativeError x (fp32Round x) hx ≤ neuralBpow binaryRadix (-24)

In the normal range, executable binary32 rounding has relative error at most $2^{-24}$.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_abs_error_of_isFinite (x y : IEEE32Exec) (hfin : (x.add y).isFinite = true) : |(x.add y).toReal - (x.toReal + y.toReal)| ≤ eps₃₂ (x.toReal + y.toReal)

Addition absolute error bound for IEEE32Exec on the finite branch.

Informal: if add x y stays finite then $|\operatorname{toReal}(\operatorname{add}(x,y)) -(\operatorname{toReal}(x)+\operatorname{toReal}(y))| \le\varepsilon_{32}(\operatorname{toReal}(x)+\operatorname{toReal}(y))$.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_abs_error_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) (hfin : (x.sub y).isFinite = true) : |(x.sub y).toReal - (x.toReal - y.toReal)| ≤ eps₃₂ (x.toReal - y.toReal)

Subtraction has the standard half-ULP bound whenever the executable result is finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_abs_error_of_isFinite (x y : IEEE32Exec) (hfin : (x.mul y).isFinite = true) : |(x.mul y).toReal - x.toReal * y.toReal| ≤ eps₃₂ (x.toReal * y.toReal)

Multiplication absolute error bound for IEEE32Exec on the finite branch.

Informal: if mul x y stays finite then $|\operatorname{toReal}(\operatorname{mul}(x,y)) -\operatorname{toReal}(x)\operatorname{toReal}(y)| \le\varepsilon_{32}(\operatorname{toReal}(x)\operatorname{toReal}(y))$.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_abs_error_of_isFinite (x y : IEEE32Exec) (hfin : (x.div y).isFinite = true) : |(x.div y).toReal - x.toReal / y.toReal| ≤ eps₃₂ (x.toReal / y.toReal)

Division absolute error bound for IEEE32Exec on the finite branch.

Informal: if div x y stays finite then $\left|\operatorname{toReal}(\operatorname{div}(x,y)) -\frac{\operatorname{toReal}(x)}{\operatorname{toReal}(y)}\right| \le\varepsilon_{32}\!\left( \frac{\operatorname{toReal}(x)}{\operatorname{toReal}(y)} \right)$.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_abs_error_of_isFinite (x y z : IEEE32Exec) (hfin : (x.fma y z).isFinite = true) : |(x.fma y z).toReal - (x.toReal * y.toReal + z.toReal)| ≤ eps₃₂ (x.toReal * y.toReal + z.toReal)

FMA absolute error bound for IEEE32Exec on the finite branch.

Informal: if fma x y z stays finite then $|\operatorname{toReal}(\operatorname{fma}(x,y,z)) -(\operatorname{toReal}(x)\operatorname{toReal}(y)+\operatorname{toReal}(z))| \le\varepsilon_{32}( \operatorname{toReal}(x)\operatorname{toReal}(y)+\operatorname{toReal}(z) )$.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_abs_error_of_isFinite (x : IEEE32Exec) (hfin : x.sqrt.isFinite = true) : |x.sqrt.toReal - √x.toReal| ≤ eps₃₂ √x.toReal

Square-root absolute error bound for IEEE32Exec on the finite branch.

Informal: if sqrt x stays finite then $|\operatorname{toReal}(\operatorname{sqrt}(x))-\sqrt{\operatorname{toReal}(x)}| \le\varepsilon_{32}(\sqrt{\operatorname{toReal}(x)})$.