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 eps₃₂ 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 |fl32(x) - x| ≤ eps₃₂(x).

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.

Informal: |fl32(a+b) - (a+b)| ≤ eps₃₂(a+b).

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.

Informal: |fl32(a-b) - (a-b)| ≤ eps₃₂(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.

Informal: |fl32(a*b) - (a*b)| ≤ eps₃₂(a*b).

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.

Informal: |fl32(a/b) - (a/b)| ≤ eps₃₂(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.

Informal: |fl32(exp(x)) - exp(x)| ≤ eps₃₂(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.

Informal: |fl32(tanh(x)) - tanh(x)| ≤ eps₃₂(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.

Informal: |fl32(log(x)) - log(x)| ≤ eps₃₂(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.

Informal: |fl32(cos(x)) - cos(x)| ≤ eps₃₂(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.

Informal: |fl32(sin(x)) - sin(x)| ≤ eps₃₂(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.

Informal: |fl32(sinh(x)) - sinh(x)| ≤ eps₃₂(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.

Informal: |fl32(cosh(x)) - cosh(x)| ≤ eps₃₂(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.

Informal: |fl32(sqrt(x)) - sqrt(x)| ≤ eps₃₂(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 ℝ, we still round the result because this is a “round after every primitive” semantics.

Informal: |fl32(|x|) - |x|| ≤ eps₃₂(|x|).