FP32 per-op error bounds

Proofs about numerical code should not have to expand the definition of “float32 rounding” every time they use + or exp. This file provides reusable rewrite theorems for FP32 rounding-error reasoning.

We collect those lemmas for TorchLean’s FP32 model:

• each primitive op is interpreted as “compute in ℝ, then round to the binary32 grid”, and
• the rounding step has a standard half-ULP absolute error bound.

This mirrors the standard mental model behind PyTorch/IEEE float analysis (even though our proof backend is not a bit-level model): it’s the classic “real computation + rounding error” split.

The pattern is always:

• compute the exact real result,
• apply the FP32 rounding operator,
• bound the rounding error by $\varepsilon_{32}(x)$, half an ulp at $x$; see NN/Floats/FP32/Notation.lean.

Important nuance: these are local statements about a single rounding step. Whole-network bounds typically combine these with:

• algebra/triangle-inequality steps, or
• higher-level composition lemmas in NN/Proofs/RuntimeApprox/*.

References

• IEEE Std 754-2019, "IEEE Standard for Floating-Point Arithmetic".
• D. Goldberg, "What Every Computer Scientist Should Know About Floating-Point Arithmetic", ACM Computing Surveys, 1991.
• N. J. Higham, "Accuracy and Stability of Numerical Algorithms", SIAM, 2nd ed., 2002.

This module works with a proof-friendly float32 semantics ("real operation + one rounding step"). Relating this abstraction to specific hardware/libm behavior is a separate, target-specific trust boundary handled elsewhere in TorchLean.

Per-op rounding error lemmas

theorem TorchLean.Floats.FP32.round_abs_error (x : ℝ) : |round₃₂ x - x| ≤ eps₃₂ x

Core rounding lemma for the binary32 parameters fixed by FP32.

This is the “one thing we use everywhere”: once you know an operation is defined as “round the real result”, the proof goal reduces to an instance of this lemma.

Informal: if fl32(x) denotes rounding x : ℝ to the binary32 grid, then $|\operatorname{fl}_{32}(x)-x|\le\varepsilon_{32}(x)$.

theorem TorchLean.Floats.FP32.round_relative_error_of_normal (x : ℝ) (hx : x ≠ 0) (hnormal : minNormal ≤ |x|) : ErrorBounds.relativeError x (round₃₂ x) hx ≤ neuralBpow binaryRadix (-24)

Normal binary32 rounding has relative error at most the unit roundoff $2^{-24}$.

theorem TorchLean.Floats.FP32.add_abs_error (a b : FP32) : |(a + b).val - (a.val + b.val)| ≤ eps₃₂ (a.val + b.val)

Addition: FP32 adds in ℝ and then rounds once.

This lemma isolates the rounding error introduced by that last step.

Informally, $|\operatorname{fl}_{32}(a+b)-(a+b)|\le\varepsilon_{32}(a+b)$.

theorem TorchLean.Floats.FP32.add_residual_isRepresentable (a b : FP32) (ha : NF.IsRepresentable a) (hb : NF.IsRepresentable b) : neuralGenericFormat binaryRadix fexp32 ((a + b).val - (a.val + b.val))

The exact residual left by FP32 addition is itself representable when both operands lie on the binary32 grid. This structural fact is used by error-free transformations and is stronger than the accompanying half-ULP inequality.

theorem TorchLean.Floats.FP32.sub_abs_error (a b : FP32) : |(a - b).val - (a.val - b.val)| ≤ eps₃₂ (a.val - b.val)

Subtraction: one real subtraction followed by one rounding step.

Informally, $|\operatorname{fl}_{32}(a-b)-(a-b)|\le\varepsilon_{32}(a-b)$.

theorem TorchLean.Floats.FP32.mul_abs_error (a b : FP32) : |(a * b).val - a.val * b.val| ≤ eps₃₂ (a.val * b.val)

Multiplication: one real multiplication followed by one rounding step.

Informally, $|\operatorname{fl}_{32}(ab)-ab|\le\varepsilon_{32}(ab)$.

theorem TorchLean.Floats.FP32.div_abs_error (a b : FP32) : |(a / b).val - a.val / b.val| ≤ eps₃₂ (a.val / b.val)

Division: one real division followed by one rounding step.

This does not say division is “well-conditioned”; it only isolates the rounding stage.

Informally, $\left|\operatorname{fl}_{32}(a/b)-a/b\right|\le\varepsilon_{32}(a/b)$.

Transcendentals (proof semantics)

theorem TorchLean.Floats.FP32.exp_abs_error (a : FP32) : |(MathFunctions.exp a).val - Real.exp a.val| ≤ eps₃₂ (Real.exp a.val)

In FP32, transcendental functions are specified as: apply the real function, then round.

That is not how hardware/libm is implemented, but it is exactly the right abstraction for proofs: it gives a clear mathematical meaning and a one-rounding-step error theorem.

Informally, $|\operatorname{fl}_{32}(\exp x)-\exp x|\le\varepsilon_{32}(\exp x)$, and similarly for the other functions below.

theorem TorchLean.Floats.FP32.tanh_abs_error (a : FP32) : |(MathFunctions.tanh a).val - Real.tanh a.val| ≤ eps₃₂ (Real.tanh a.val)

tanh in the proof model: real tanh followed by rounding.

Informally, $|\operatorname{fl}_{32}(\tanh x)-\tanh x|\le\varepsilon_{32}(\tanh x)$.

theorem TorchLean.Floats.FP32.log_abs_error (a : FP32) : |(MathFunctions.log a).val - Real.log a.val| ≤ eps₃₂ (Real.log a.val)

log in the proof model: real log followed by rounding.

Domain note: the inequality is about rounding error around Real.log a.val; it does not assert anything about a.val > 0.

Informally, $|\operatorname{fl}_{32}(\log x)-\log x|\le\varepsilon_{32}(\log x)$.

theorem TorchLean.Floats.FP32.cos_abs_error (a : FP32) : |(MathFunctions.cos a).val - Real.cos a.val| ≤ eps₃₂ (Real.cos a.val)

cos in the proof model: real cos followed by rounding.

Informally, $|\operatorname{fl}_{32}(\cos x)-\cos x|\le\varepsilon_{32}(\cos x)$.

theorem TorchLean.Floats.FP32.sin_abs_error (a : FP32) : |(MathFunctions.sin a).val - Real.sin a.val| ≤ eps₃₂ (Real.sin a.val)

sin in the proof model: real sin followed by rounding.

Informally, $|\operatorname{fl}_{32}(\sin x)-\sin x|\le\varepsilon_{32}(\sin x)$.

theorem TorchLean.Floats.FP32.sinh_abs_error (a : FP32) : |(MathFunctions.sinh a).val - Real.sinh a.val| ≤ eps₃₂ (Real.sinh a.val)

sinh in the proof model: real sinh followed by rounding.

Informally, $|\operatorname{fl}_{32}(\sinh x)-\sinh x|\le\varepsilon_{32}(\sinh x)$.

theorem TorchLean.Floats.FP32.cosh_abs_error (a : FP32) : |(MathFunctions.cosh a).val - Real.cosh a.val| ≤ eps₃₂ (Real.cosh a.val)

cosh in the proof model: real cosh followed by rounding.

Informally, $|\operatorname{fl}_{32}(\cosh x)-\cosh x|\le\varepsilon_{32}(\cosh x)$.

theorem TorchLean.Floats.FP32.sqrt_abs_error (a : FP32) : |(MathFunctions.sqrt a).val - √a.val| ≤ eps₃₂ √a.val

sqrt in the proof model: real sqrt followed by rounding.

Informally, $|\operatorname{fl}_{32}(\sqrt{x})-\sqrt{x}|\le\varepsilon_{32}(\sqrt{x})$.

theorem TorchLean.Floats.FP32.abs_abs_error (a : FP32) : |(MathFunctions.abs a).val - |a.val|| ≤ eps₃₂ |a.val|

abs in the proof model: real absolute value followed by rounding.

Even though $|x|$ is exact over $\mathbb R$, we still round the result because this is a “round after every primitive” semantics.

Informally, $\left|\operatorname{fl}_{32}(|x|)-|x|\right|\le\varepsilon_{32}(|x|)$.